演繹システムのパート分類（モジュラー／レイヤード設計・実装のため）： 分野固有パート 論理パート（分野によらない共通パート） 分野固有パートは： 個体レベル 型レベル 論理パート 命題レベル 推論レベル システムが単ソート〈single{- | }sort{ed}?〉…

まず、同義語のまとめ。 指標⊆仕様＝セオリー＝プレゼンテーション＝コンピュータッド＝ポリグラフ＝グラフ＝箙 モデル＝構造＝代数＝加群＝表現 基本構図は： A ∈0 n-AlgD(τ, A) これの文脈は、 τ ∈0 n-Thy D ∈0 (n+1)-Thy A ∈0 (n+1)-AlgD'(τ', A') 文脈内…

用語ごとのリンク集： 母数: まともな定義がない - 檜山正幸のキマイラ飼育記 メモ編 母数 - 檜山正幸のキマイラ飼育記 メモ編 やっぱり用語記号が分からない - 檜山正幸のキマイラ飼育記 メモ編 定数と汎関数とパラメータ（母数） - 檜山正幸のキマイラ飼育…

ほぼワースト順 確率変数 分布、分布する 従う 母集団 試行、試行する サンプリング〈標本調査〉する 離散（形容詞） 例文（例文はもっと欲しい） xを確率変数として、xの関数f(x)をxにより積分すると、f(x)の期待値が得られる。 t値とは、t分布に従って分布…

代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 の続きで、ローヴェル・セオリーを可能とするフレームワークについて。ローヴェル・セオリーローヴェル・セオリーの導入・説明では、有限集合の圏FinSetの骨格として、基数（それ自身集…

内容： 代数的定義形式 代数的定義形式の同義語群 アンビエント 定義形式のアンカリング 単位対象と格上げ 値k-射と定義形式の格上げ モデルとモデルの圏 TBD：ローヴェル・フレームワーク TBD：族と抽象と脱抽象 代数的定義形式n-圏と関連する圏論的実体〈c…

rator - 檜山正幸のキマイラ飼育記 メモ編の続き。交換律 commutative law のratorは、associat-ive → associat-or に倣うなら commutat-ive → commutat-or だが、commutatorは使えない。苦し紛れでcommutorにする。transforのような造語もあるし。https://a…

とりあえず表。説明はその下。 関手オートマトン 可達性 可識性 圏論 相対分離性 相対余分離性 部分圏 余反映的部分圏 反映的部分圏 エルブラン構成 単純エルブラン構成 二重双対エルブラン構成 分離性は圏に分離対象（separator）または分離対象族（family …

数量の感覚 - 檜山正幸のキマイラ飼育記 メモ編 の件：ここにまとめておく。足していく（つもり）。 日常的な数量の色々 体重 身長 クラスや会社や組織の人数 価格 移動の距離 移動の時間 ペットボトルの容量 ビルの高さ 部屋やフロアの広さ 荷物の重さ 株価…

「これはひどい」としか言いようがない。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]他の参考記事： 「ならば」記号の部分 - 檜山正幸のキマイラ飼育記 メモ編 論理の用語、日本語-英語 - 檜山正幸のキマイラ飼育記 メモ編…

ここにまとめることにする。追加情報は追記していく。配布に付いているPDF文書、同梱文書と呼ぶことにする。略称はファイルのベース名。 タイトル ページ数 略称 Programming and Proving in Isabelle/HOL 63 prog-prove A Proof Assistant for Higher-Order…

インストールと「誰も書かない」シリーズ1から5： WindowsへのCoqのインストール - 檜山正幸のキマイラ飼育記 誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記 業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2） - 檜山正幸…

主に2015年10月と11月、12月少し（昨日・今日とか）でブログに出現した表を集めてみる。全部一度に眺めると、なにか思いつくかもしれない、と期待して。まとめる作業がイイカゲンだから、順不同で網羅的かどうかも分からない。 豊饒プロ関手は豊饒な世界を提…

なんらかの意味でオートマトンの圏があるとき、次の操作がある。 オートマトンの最小化、最適化、正規化などと呼ばれる操作 「観測可能な振る舞い」という概念があり、オートマトンにその観測可能な振る舞いを対応させる操作 指定された振る舞いを実際に行う…

ネタバレ。『ダークナイト ライジング（The Dark Knight Rises）』（2012年）を一人で観に行った。子供たちは興味ない。実際、（うちの）子供たちが喜ぶような映画じゃないな。最近のバットマン（クリストファー・ノーラン監督の三部作）はシリアスで暗い。…

時間も空間も何もかも離散的な状況で考える。可算無限は認めたいが、面倒なら全部有限でいい、という前提。時間発展の生成子（time evolution generator）は、正方行列Aで与えられているとする。境界（入出力）とかあるけど、とりあえずはAだけに注目。 FA(k…

「式を計算（評価）して値を求める」-- という構造を一般化するハナシ。とりとめもない。 計算とは（ここでは）、計算関手:図式の圏→値の圏。値の圏は、事実上「行列の圏」。図式とは、図 and/or 式、つまり、graph, diagram, term, expression, formulaなど…

毎度毎度、、、 さまざまな「ならば」達も参照。構文 項 term 基礎項＝閉じた項 ground term = closed term 論理式 formula 閉じた論理式＝文 closed formula = sentence 命題論理式 propositional formula 言明 statement 素論理式＝原子論理式 prime formu…

やっぱり、カウフマンブラケットはねじれ付き無向絡み目に対して定義するのが自然だな。ねじれ（ひねり）はねじれ乗数（twist factor）に表現される。輪っこもねじれもスカラー乗法になるのは不思議な気もするが、スプライシング（交差の解消）とヤンキング…

もう少しチャントまとまったら書こうと思っていたが、とりあえず叩き台。●不動点等式／不等式／帰納法 a・a* + 1 = a* [不動点等式; the fixed point equation] a・a* + 1 ≦ a* [不動点不等式; the fixed point enequation] a・x + b ≦ x ⇒ a*・b≦x [不動点…

まずはAb圏の定義から： hom-setがアーベル群 射の結合は双線形 零対象を持つことは仮定しない（零射は存在する）。 次に加法圏： Ab圏である。 零対象を持つ。 双積を持つ。 Ab圏をプレ加法圏（preadditive category）とも呼ぶ。対応する「半」概念。 加法…

ケリー双対については、http://d.hatena.ne.jp/m-hiyama-memo/20070331 に書いてある。直進圏は http://d.hatena.ne.jp/m-hiyama-memo/20070426/1177562726、軸的圏は http://d.hatena.ne.jp/m-hiyama-memo/20070329/1175144493 。 種類 左双対 右双対 左＝…

対称モノイド閉圏があり、モノイド積による関手の随伴により内部ホムを定義して、自己豊饒化されている状況を考える。モノイド積を×、内部ホム（ホム積）を[-, -]で書くとする。デカルト閉圏やコンパクト閉圏で成立している同型と、それに類似の算術公式をま…

区別／使い分けがわからない - 檜山正幸のキマイラ飼育記 メモ編にて： ハミルトンの原理と最小作用の原理って同じようだが？ 準備： s = s(t)（t = t0からt1）を運動のパラメータ表示とする（配位空間を動く）。(s, s')（s' = ds/dt）は相空間上での軌道（…

Exotic Semirings - 檜山正幸のキマイラ飼育記 メモ編にある表を再掲。 台集合 加法 乗法 名称 N∪{+∞} min + tropical半環 N∪{-∞} max + polar半環 N∪{+∞} min max fuzzy半環 R∪{+∞} min + optimization代数 R∪{-∞} max + schedule代数 fuzzy半環を除いて、…

組み合わせ幾何学的な簡約・変形を移動（move）と呼ぶ習慣がある。で、いろいろな移動をまとめてみる。中心になるのは、ライデマイスター（Reidemeister）移動I, II, IIIである。カウフマン（Kauffman）はジグザグ等式を移動0として追加している。アルチン（…

ソフトウェア的な技法 圏論的な解釈 論理計算 ラムダ計算 具体的なモデル ソフトウェア的な技法としては、とりあえずはコンベンションと動的（実行時）演算ライブラリだけを準備して、徒手空拳でも使えることをアピールしよう。もちろん、コンテナ（自動的な…

まとめになってないし、裏を取ってないけど、とりあえずバラバラと書いておく。後で確認してリンクとか付けよう。人名はできるだけ片仮名書きするが、発音が見当もつかないのは原綴。[追記]人物リンク集 - 檜山正幸のキマイラ飼育記 メモ編参照。[/追記]トゥ…

道具が十分揃った、とは全然言えないけど、当初の目的であったXMLへのアタックを再開しよう。そう思った理由は：理由その1：インラインテーブル問題昔（20世紀だな）設定したいくつかの問題のなかでも難問だと思っていた「インラインテーブル問題」、ふと思…

なんか、思惑とは違った展開だな -- 別にいいけど。状況をまとめておく。まず、ElgotオペレータとConwayオペレータは、本質的に同じことがわかった。Elgotオペレータが余デカルト（な対称モノイド）圏、Conwayオペレータがデカルト圏に作用するもので、お互…