圏論的論理のチュートリアル

muses 半形式証明スクリプト 論理 課題

これは良いチュートリアルのように思えるが、「ゴッチャにした記述」が気になる。

typing rule として次の3つがある。

  1. （構文的）項の構成規則と対応するプロファイルの決定規則： プロファイルの決定規則に注目して typing rule と呼んでいるようだ。
  2. （意味論的）シング（意味的存在物）の構成規則とシングのアビタ決定規則： とある構成に関してアビタが閉じていることが背景にある。
  3. 文法の生成規則と構文範疇の決定規則： 構文的な構成で記号表現〈項 | 式〉の作り方と、構文範疇の計算法

文法がらみは {syntax | syntactic{al}?} {formation | forming} rule のこと。構文範疇と型は違うが、しばしば混同される。p.4 の Figure 2 を typing rule と呼ぶのは酷すぎる。これは、論理式の文法生成規則。論理式が表すシングがPropと呼ばれるアビタに棲んでいる。

それに対して、p.3 Figure 1 は、デカル閉圏をアビタ（セマンティック背景圏）とする項〈式 | テキスト・コンビネーション〉の構成規則になっている。タイピング〈プロファイリング〉は構成に付随するオマケ的位置付け。セマンティクスを伴う項構成規則でプロファイルも計算可能な規則。

同義語
  • 関数 ＝ オペレーション ＝ 射 ＝ 1-射
  • 型 ＝ ソート ＝ 対象 ＝ 0-射
  • 関数名 ＝ 関数定数 ＝ オペレーション記号 ＝ 射ラベル ＝ 1-ラベル
  • 型名 ＝ 型定数 ＝ ソート記号 ＝ 対象ラベル ＝ 0-ラベル
  • しばしば 関数 ＝ 関数名、型 ＝ 型名
  • 基本型 ＝ 生成0-射
  • 基本関数 ＝ 生成1-射

例によって、次は同義。

  • {base | primitive | atomic | prime | built-in | simple} {type | sort | object} {symbol | name | constant}? = generating 0-morphism label
  • {base | primitive | atomic | prime | built-in | simple} {function | operation | morphism} {symbol | name | constant}? = generating 1-morphism label
項の構成規則

素材は：

  1. 生成0-射 1
  2. 生成1-射 I, X, Δ, !, π^1, π^2

オペレータは

  1. 直積 0-オペレータ（1-オペレータは無し）
  2. 指数〈ベキ乗 | 累乗 | 指数〉 0-オペレータ（1-オペレータは無し）
  3. ペアリング
  4. カリー化
  5. 反カリー化

詳細は DIDLで規則記述 - (新) 檜山正幸のキマイラ飼育記 メモ編

シーケント

当該チュートリアルのいい点は、シーケントの定義が明確な点だろう。シーケントは次の形に書かれる。

$`\quad \Gamma \mid \Xi \vdash \psi`$

Γは型コンテキストで、圏論的な指標になる。x:σ は x:1 → σ とみなすので、1-mor宣言がならぶことになる。型コンテキストとは限らない一般の指標をとってもいい。Γはセオリーを決めると言ってもいい。

Ξ は、論域が共通な命題〈論理式〉のリストで、

$`\quad \Xi = (\varphi_1, \cdots, \varphi_n)`$

したがって、シーケントの一部を抜き出すと、

$`\quad (\varphi_1, \cdots, \varphi_n) \vdash \psi`$

これは、命題の圏のプロファイル。シーケント全体としては、Γが定義する命題の圏のなかのプロファイルを意味する。そのプロファイルを持つ射 F が導出（通常「証明」とも呼ばれる）。X は論域。

$`\quad F : (\varphi_1, \cdots, \varphi_n) \to \psi \text{ on } X \text{ in }\mathrm{Prop}[\Gamma]`$

「シーケントが証明できる」とは、そのシーケント＝プロファイルを持つ導出が構成可能であること。

檜山の課題

p.40に自然演繹の規則が書いてある。これをチャンと圏論的・絵算的に書き換えて、最終的にDIDLで書く。