リテラルは、シングの束縛〈割り当て | 結びつき〉を持つ名前〈ラベル〉 宣言文は名前〈ラベル〉へのプロファイルの割り当て ソフト定義文は名前〈ラベル〉へのコンビネーション〈項〉の割り当て、マクロ・ラベルを生成する。 ハード定義文は名前〈ラベル〉…

名前とラベルは同義語。束縛と割り当ては同義語。広義のタイピングとプロファイリングは同義。束縛にはハード束縛とソフト束縛がある（後述）。 束縛される前のラベルは変数 ハード束縛された後のラベルはリテラル 束縛の種類： ハード束縛： 名前〈変数〉に…

記述すべきモノを対象物〈objectum | オブジェクタム〉と呼ぶ。対象物の種別は意味範疇、文法内の品詞は構文範疇。次の意味範疇に属する対象物を扱う。 関数： 圏 $`\mathcal{TF}`$ の1-射、f∈Map(X, Y) 値・個体・データ ： 圏 $`\mathcal{TF}`$ のポインテ…

バンチ計算システムの構成素： 項 バンチ 書き換え規則 書き換えアクション 書き換え系列〈sequence〉 説明： 項は構文的コンビネーション ツリー構造 リーフは型付き変数または型付きリテラル、型は圏の対象 リーフ以外のノードはコネクティブ 文法範疇があ…

演繹システムの議論で、知識ベースの管理やダイナミズムの考慮が決定的に欠けていたと思う。知識ベースを $`\mathscr{K}, \mathscr{L}`$ などで表し、常に考慮する。知識ベースは、ハイパードクトリンやインスティチューションの生成系だと考える。生成され…

広義の項書き換え系について考えている。書き換えと置換〈substitution〉は区別しなくていいだろう。とりあえず、3種類の書き換え＝置換がある。 関数項置換： 変数／リテラルをリーフとし、関数記号をノードとする構文木において、部分木（リーフノードも、…

「命題」の曖昧性 真偽値 述語 論理式 （個体変数に関して）閉じた論理式 ところが、「論理式」が曖昧。 テンプレート述語項構文木（リーフが穴、ノードが述語コネクティブ） テンプレート述語項構文木＋述語コンテキスト 評価値である述語 型理論のときも、…

$`\newcommand{\LLambda}{\mathrm{L}\Lambda} \newcommand{\Llambda}{\mathrm{L}\lambda} \newcommand{\RLambda}{\mathrm{R}\Lambda} \newcommand{\Rlambda}{\mathrm{R}\lambda} \newcommand{\Dia}{\diamondsuit} \newcommand{\mrm}[1]{\mathrm{#1} } \newco…

ド・モルガン双対 ド・モルガン双対をリスト〈バンチ〉に対して定義する。双対化演算は、 *(A1, ..., An) = (￢A1| ...| ￢An) *(,) = (|) *(A1| ...| An) = (￢A1, ..., ￢An) *(|) = (,) ** = id と定義する。推論規則は ￢ 左 (Γ → Δ| Φ) ⇒ (*Φ, Γ → Δ) …

シーケント計算をリーズニング構成の計算と考える。できるだけ少ないリーズニングで計算をしたい。リーズニングを少なくするには、プリミティブな導出を揃える。 ∧-モノイド構造 ∨-モノイド構造 ![A] Θ[A] Δ[A] ∇[A] π1[A, B] ι1[A, B] π2[A, B] ι2[A, B] X[…

知識ベースには、次のようなものが入っている。 型の宣言・定義 関数の宣言・定義 命題の宣言・定義 導出の宣言・定義 リーズニングの宣言・定義 メタリーズニングの宣言・定義 それらを組織化する構造ファセット 知識ベースを背景にして、新しい型／関数／…

とある論文で使っていた用語法： シーケントの左辺 ＝ antecedent〈前件〉 シーケントの右辺 ＝ succedent〈後件〉 イニシャルシーケント ＝ 公理シーケント シーケントの推論規則用語： 上式 ＝ premises〈仮定〉 下式 ＝ conclusion〈結論〉 前件、後件、…

保証〈warranty〉 ： derivation T → A 反駁〈refutation〉 ： derivation A → ⊥ 証拠〈witness〉 ： 存在記号導入に使う要素、項 事例〈instance〉 ： 全称記号消去に使う要素、項 存在スタート条件〈existential starting condition〉 ： 存在記号消去に伴…

対象物： 型 関数 値〈データ | ポイント〉 特別な関数 汎関数〈メタ関数〉 命題（真偽値、述語、論理式） 導出 保証 特別な導出 リーズニング〈メタ導出〉 カリー／ハワード／ランベック対応 型 命題 関数 導出 値 保証 汎関数 リーズニング 項： 型項（多…

動詞 DoSomething 名詞 Something 短縮 construct construction cons calculate calculation calc derive derivation deriv reason reasoning reas Begin Something WeHave A And, B Using Something X params WeHave A' And, B' Using Something Y params .…

$`\newcommand{\Sep}{\mathrel{\|} } \newcommand{\Subst}[2]{ {\scriptsize \begin{bmatrix} #1\\ #2 \end{bmatrix} } } %`$$`\quad \alpha \Sep \varphi: \Gamma \to B`$ここで： 型コンテキストはギリシャ文字小文字 命題コンテキストはギリシャ大文字 命…

palette CCC { parameter wire X, Y, Z node left-eval[X, Y] : (X, X⇒Y) → (Y) node decomp-prod[X, Y] : (X×Y) → (X, Y) node swap[X, Y] : (X, Y) → (Y, X) action LeftCurry[X, Y, Z] :: ((X, Y) → (Z)) ~~→ ((Y) → (X⇒Y)) // ...省略... parameter node…

描画モデルは、描画エージェント（一人、ペインター、画師、絵師）、キャンバス（入れ子可能）、パレット（複数可能）からなる。 唯一のカレントキャンバスを持つ。 唯一のカレントフォーカスポイントを持つ。それは、カレントキャンバス上の点。 カレントフ…

型・関数 命題・導出 0-射 型 0-射 命題 0-オペレータ 積 0-オペレータ 連言 0-オペレータ 指数 0-オペレータ 含意 0-射 指数型 0-射 含意命題 1-射 関数 1-射 導出 1-射 データ 1-射 保証〈ワランティー〉 1-射 入射〈余射影〉 1-射 証拠 1-射 射影〈成分〉…

少し追記。 型コンテキストを型判断と呼ぶ用語法は採用しない。 型シーケント $`\Gamma \vdash M:\sigma`$ を型判断〈typing judgement〉と呼ぶのは許容しよう。 型判断の意味はセマンティック・デカルト閉圏の射になる。特に集合圏では単なる写像。型コンテ…

まず、次は同義語扱いしたほうがいい。 変数の型宣言 型コンテキスト 0-指標 ポイント1-射だけの1-指標 構造体定義 レコード定義 テーブルスキーマ 例えば、 variable x, y : Real, c : Color type-context {x:Real, y:Real, c:Color} 0-signature _ { 0-mor…

型の圏（複圏、多圏もある）と命題の圏（複圏、多圏もある）との関係。カリー／ハワード／ランベック対応（むしろ、カリー／ハワード／ランベック・フレームワーク）があるので似てる。抽象化すれば同じになる。が、型コンテキストの圏の対象の上に命題の圏…

MEDL（Mathematical Entity Description Lang.）とDIDL（Drawing Instruction and Description Lang.）について。DIDLはある程度は汎用の絵図記述言語。だが、直接的な目的は証明記述。「証明」は曖昧語なので、テクニカルタームとしては導出〈derivation〉…

MP導出の図を向きを変える。 スタックとリストの関係と等式の証明 計算図 リーズニング図 紙芝居方式リーズニング図リーズニング図の同値変形 分岐合流紙芝居方式リーズニング図 線形証明とグラフ証明図とツリー証明図連言リストと宣言リスト、α, β は論域。…

演繹システム - (新) 檜山正幸のキマイラ飼育記 メモ編 演繹システム (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 演繹システム (3) - (新) 檜山正幸のキマイラ飼育記 メモ編 $`\newcommand{\derive}{ \vdash }% \newcommand{\deduce}{ \mathop{\|\!-} }% \…

Title: A Taste of Categorical Logic — Tutorial Notes Authors: Lars Birkedal (birkedal@cs.au.dk), Aleš Bizjak (abizjak@cs.au.dk) Date: July 10, 2017 URL: https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf これは良いチュート…

https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の P.3 の11個の規則 IDENTITY WEAKENING CONTRACTION EXCHANGE MULTI-COMPOSITION （もとは無名） PAIRING PROJ-1 PROJ-2 ABS APP UNIT（むしろTERMINALだろうが） 使う文は以下。確…

面積問題への対策（あるいは無策） (A21) - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2019-01-08 意味不明な言葉達 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2018-11-15 お絵描き証明の例 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2016-02-24 $`\v…

CoqでもLeanでもPropを使うが、Prepの正体は何でもよくて、デカルト閉半環圏（の対象集合）であればよい。自然数上に定義された述語 p は p: Nat → Prop だが、その実体が次のいずれでも、さらに他の何かでもいい。$`\quad p:{\bf N} \to {\bf B} \text{ in …

ストリング図の描画指令〈instruction〉と記述〈description〉のための言語 Drawing Instruction Description Language 目的は違うが名前が似ているもの： https://www.ijcai.org/Proceedings/03/Papers/069.pdf LADDER (LAnguage to Describe Drawing, disp…