今後の注意事項

論理 半形式証明スクリプト
  • 論域が大きい場合〈large domain of discourse〉を考える。
  • 複アロー構成と多アロー構成、そのときのパラメータとしてのコレクションモナド
  • コレクションモナドの一種としてのバンチモナド
  • 型コンテキストと指標は同一概念であること。
  • 命題コンテキストはフィイバー方向の型コンテキスト
  • ベース方向とファイバー方向の“切れ目”を変えること。
  • バンチの分配法則
  • 色々な多圏様構造と色々なシーケント計算
  • リーズニング・プログラミング： メタリーズニングは Apply, Comp, Prod があるCCC（かな？）
  • 導出を対象として、リーズニングを射とするCCC（かな？）での計算がリーズニング・プログラミング

計算の構造

論理 半形式証明スクリプト 多義語 セミナー

構文論：

基本概念 別名
ラベル 名前, 変数, 不定元, 定数, 識別子
シング n-射, もの, 実体, 具体物
割り当て 束縛, 代入, 関連付け〈association〉
リテラル 定数, 名前, 記号
コネクティブ 演算{子}?記号
コンビネーション 項, 式, 図式

※ 論理のリテラルは、原子論理式〈アトム〉またはその否定。コンビネーションは順列組み合わせとは無関係。

構文論の基本概念であるが、シングは意味領域の対象物〈semantic object〉。ラベル、リテラル、コネクティブ、コンビネーションは構文領域の対象物〈syntactic object〉。

  1. コンビネーションは構文解析できて、構文木を作れる。
  2. 構文木の末端は、ラベル（リテラル含む）、末端以外はコネクティブ
  3. 文法範疇〈構文範疇〉は、また別に定義される。
  4. シングに束縛された状態のラベルがリテラル。未束縛のラベルは変数。定数は、自由変数かリテラルか意味不明なので使用禁止が吉。定数関数はまた意味が違う（練習：定数関数を定義せよ）
  5. 定数／変数は、運用方針（気持ち）と状態に関する形容詞〈述語〉。リテラルもラベルの状態。
  6. ラベルの状態は、(1)未束縛、(2)シングに束縛（リテラル）、(3)コンビネーションに束縛 の三状態だが、リテラルはコンビネーションなので、リテラルに束縛は (2) と (3) の区別が難しい。ここはややこしいが、構文論としては「リテラル≠シング」と考えて区別する。「山田」は山田ではない。
  7. ラベルの集合があり、すべてのラベルに束縛〈割り当て〉があるとき、束縛セットと呼ぶ。単一束縛と束縛セットは区別する。
  8. プロファイル束縛セット、シング束縛セット、コンビネーション束縛セットをそれぞれ、指標、モデル、構成手続きと呼ぶ。
  9. プロファイル束縛セット〈指標〉をスキーマ、型宣言セット、型コンテキスト、コンテキストとも呼ぶ。
  10. シング束縛セット〈モデル〉をハードインスタンス、値環境、ハード環境、ハード実装とも呼ぶ。
  11. コンビネーション束縛セット〈手続き〉をソフトインスタンス、項環境、ソフト環境、ソフト実装とも呼ぶ。
  12. ハード{インスタンス | 実装}とソフト{インスタンス | 実装}は区別すべき。ソフト実装が、すべてリテラルで与えられていてもソフト。ハードにするにはリテラルの評価が必要。
  13. コンビネーションを評価〈式を計算〉するには、評価環境が必要。評価環境がハード環境〈モデル〉のときはすぐに評価できるが、ソフト環境のときが問題。
  14. 評価環境がソフト環境〈手続き〉のときは、先にソフト環境を評価してハード環境〈モデル〉を作る必要がある。この手順は再帰的に行われる。
  15. 評価の再帰的なプロセスはツリーで表現できるので、評価ツリー〈evaluation tree〉と呼ぼう。
  16. コンビネーションの評価〈式の計算〉は、評価ツリーのtop-down構築〈tree building〉と、評価ツリーのbottom-up具体化の2フェーズからなる。top-down building phase と bottom-up concretization phase
  17. 具体化〈concretization〉とは、ハード環境〈モデル〉による評価のこと。

こうしてみると、同義語で騙されている面が大きい。

  1. プロファイル束縛セット＝指標＝スキーマ＝型コンテキスト、カリー／ハワード／ランベック・フレームワークでは 命題＝型 だから、指標 ＝ 型コンテキスト ＝ 命題コンテキスト in (命題と導出の圏)
  2. シング束縛セット＝モデル＝値環境＝ハード環境＝ハード実装、手続き＝項環境＝ソフト環境 とは違う。が、リテラル束縛セットはシング束縛セットと区別しにくい。
  3. コンビネーション束縛セット＝手続き＝項環境＝ソフト環境＝ソフト実装。コンビネーションの評価によりモデル＝ハード実装に具体化できる。

素朴な用語法では：

  1. リテラル＝数表記〈numeral〉、数字〈digit character〉は数表記〈数表示〉とは違う。
  2. シング＝数〈number〉
  3. コンビネーション＝式
  4. 評価＝計算

知識ベースの構造

論理 半形式証明スクリプト 多義語
  • リテラルは、シングの束縛〈割り当て | 結びつき〉を持つ名前〈ラベル〉
  • 宣言文は名前〈ラベル〉へのプロファイルの割り当て
  • ソフト定義文は名前〈ラベル〉へのコンビネーション〈項〉の割り当て、マクロ・ラベルを生成する。
  • ハード定義文は名前〈ラベル〉へのシング〈項〉の割り当て、リテラルを生成する。
  • 宣言文のバンチを指標と呼ぶ。型コンテキスト、タイピング・コンテキストともいう。
  • ソフト定義文のバンチを構成手続きと呼ぶ。ソフト環境ともいう
  • ハード定義文のバンチをモデルと呼ぶ。ハード環境ともいう

知識ベースには次のものが含まれる。

  1. 型リテラル Nat, Bool, Real, 1 など
  2. 型構成子コネクティブ ×, [,] など
  3. 値リテラル〈型付き値定数〉 0, 1, true など
  4. 関数リテラル＝値構成子コネクティブ +, *, ^ など
  5. 述語リテラル（関数リテラルの特殊ケース） =, ≦ など
  6. 述語コネクティブ＝論理コネクティブ ∧, ∨, ￢ など
  7. 保証リテラル 公理論理式と |- で書く
  8. プリミティブ導出リテラル MP など
  9. プリミティブ・リーズニング・リテラル ConjIntro, LCurry など
  10. プリミティブ・メタリーズニング・リテラル APPLY, COMP, PROD など

グルーピング／組織化の手法として

  1. 指標デビジョン
  2. モデル・デビジョン
  3. 手続き・デビジョン
  4. 一般デビジョン

$`\mathscr{K}`$ が知識ベースなら、構文ベースのハイパードクトリン／インスティチューションを生成するので、それを $`\mathscr{K}^*`$ と書く。問題は、$`\mathscr{K}^*`$ の構造と意味論。

意味論と構文論の整理

論理 半形式証明スクリプト 多義語

名前とラベルは同義語。束縛と割り当ては同義語。広義のタイピングとプロファイリングは同義。束縛にはハード束縛とソフト束縛がある（後述）。

  • 束縛される前のラベルは変数
  • ハード束縛された後のラベルはリテラル

束縛の種類：

  • ハード束縛： 名前〈変数〉にシングまたはリテラルを束縛する。
  • ソフト束縛： 名前〈変数〉にコンビネーション〈項〉を束縛する。

コンテキストが曖昧語なので、次のように形容詞を付ける。

  • 変数タイピング・コンテキスト
  • 変数ハード束縛コンテキスト
  • 変数ソフト束縛コンテキスト

環境という言葉を使う場合は：

  • 変数タイピング・コンテキスト＝変数プロファイリング・コンテキスト＝コンテキスト＝指標
  • 変数ハード束縛コンテキスト＝ハード環境＝リテラル定義＝モデル＝インスタンス
  • 変数ソフト束縛コンテキスト＝ソフト環境＝マクロ定義＝構成手続き

変数の種別は次のとおり。TF は types and functions、PD は propositions and derivations。

変数の種別 シング
型変数 0-mor in TF
値変数 1-mor in TF from 1
関数変数 1-mor in TF
述語変数 1-mor in TF to B
型バンチ変数 0-mor in PolyArr(TF)
多関数変数 1-mor in PolyArr(TF)
論理式変数 0-mor in PD
論理バンチ変数 0-mor in PolyArr(PD)
導出変数 1-mor in PD
多導出変数 1-mor in PolyArr(PD)
保証変数 1-mor in PD from T
リーズニング変数 1-optor on PolyArr(PD)

コンテキスト＝指標 があれば、項〈コンビネーション〉のプロファイリング〈タイピング | 型つけ〉が出来る。

次の言葉づかいと同義語を理解・認識する必要がある。同義語の認識〈同定〉、多義語の解決でクリアになる。

  1. 圏の対象を「型」と呼ぶことがある。
  2. 型つけ＝タイピング＝型推論 である。行為〈アクション | プロセス〉としての型つけは、変数・項を対象物として遂行〈アクト | パフォーム〉される。
  3. タイピング＝プロファイリング である。
  4. 値＝ポイント＝ポインティング射 である。
  5. 広義の型コンテキスト＝プロファイリング・コンテキスト＝指標 である。
  6. 指標＝スキーマ である。
  7. 型定義は、型ラベルに型リテラルの割り当てか、型ラベルに型項の割り当てか、スキーマか、曖昧。
  1. 項の評価には環境が必要である。環境はソフト環境とハード環境がある。
  2. ソフト環境〈構成手続き | 多関数・多導出〉による項の評価をマクロ展開／テンプレート展開と呼ぶ。
  3. ハード環境〈モデル | タプル〉による項の評価を具体化と呼ぶ。
  4. マクロ展開も具体化も、展開、置換、代入と呼ぶ。
  5. したがって、展開と置換と代入は同義語であり、いずれも曖昧語である。（曖昧語としての同義語、同義な曖昧語）

計算システムの構文

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

記述すべきモノを対象物〈objectum | オブジェクタム〉と呼ぶ。対象物の種別は意味範疇、文法内の品詞は構文範疇。次の意味範疇に属する対象物を扱う。

  1. 関数： 圏 $`\mathcal{TF}`$ の1-射、f∈Map(X, Y)
  2. 値・個体・データ ： 圏 $`\mathcal{TF}`$ のポインティング1-射、a∈Map(1, X), a∈X
  3. 型 ： 圏 $`\mathcal{TF}`$ の0-射、X∈Type
  4. 真偽値 ： 集合 $`{\bf B}`$ の要素、t∈Bool
  5. 述語 ： $`{\bf B}`$ を余域とする関数であり、圏 $`\mathcal{PD}`$ の0-射、p∈Map(X, B), p∈|PD|
  6. 論理式 ： 圏 $`\mathcal{PD}`$ を意味領域とする構文的対象物、F∈Formula[X]
  7. バンチ ： アトムの集合と区切り記号の集合から構成されるツリー構造 b∈Bunch[A, D]
  8. 導出 ： 圏 $`\mathcal{PD}`$ の1-射、p:P → Q in PD

△はオーバーロード・コンフリクト。？は好ましくない用法。？？は名前がない。

関数

  • 変数： 関数変数＝△関数
  • リテラル： 関数リテラル＝関数{記号 | 名}＝△関数
  • コネクティブ： 関数コネクティブ＝{汎関数 | 作用素}{記号 | 名}＝△{汎関数 | 作用素}
  • 項： 関数項＝△関数
  • 閉じた項の意味： 関数
  • 開いた項の意味： 汎関数

値・個体・データ

  • 変数： 個体変数＝？変数
  • リテラル： 個体リテラル＝個体定数＝？定数
  • コネクティブ： 個体コネクティブ＝関数リテラル
  • 項：個体項＝関数値項
  • 閉じた項の意味： 個体
  • 開いた項の意味： 関数

型

  • 変数： 型変数＝型パラメータ
  • リテラル： 型{名 | 記号}＝△型
  • コネクティブ： 型コネクティブ＝型演算{名 | 記号}＝型構成子{名 | 記号}＝△型構成子
  • 項： 型項＝△型
  • 閉じた項の意味： 型
  • 開いた項の意味： 型構成子

真偽値

  • 変数： 真偽値変数＝？命題変数
  • リテラル： 真偽値リテラル＝？論理定数＝？命題定数
  • コネクティブ： 真偽値コネクティブ＝？論理コネクティブ＝？論理記号
  • 項： 真偽値項＝ブール項＝？命題＝？論理式
  • 閉じた項の意味： 真偽値
  • 開いた項の意味： 真理関数＝ブール関数〈Boolean function〉

述語

  • 変数： 述語変数＝？命題変数
  • リテラル： 述語リテラル＝述語{記号 | 名}＝△述語
  • コネクティブ： 述語コネクティブ＝？論理コネクティブ＝？論理記号
  • 項： 述語項＝論理式＝△述語
  • 閉じた項の意味： 述語
  • 開いた項の意味： ？？

論理式

  • 変数： 論理式変数＝？命題変数
  • リテラル： 論理式リテラル＝論理式（自分がリテラル）
  • コネクティブ： 論理式コネクティブ＝？論理コネクティブ＝？論理記号
  • 項： 論理式の論理式〈入れ子の論理式〉
  • 閉じた項の意味： 論理式
  • 開いた項の意味： ？？

バンチ

  • 変数： バンチ変数（大文字ギリシャ文字）
  • リテラル： バンチリテラル＝バンチ（自分がリテラル）
  • コネクティブ： バンチコネクティブ＝バンチリーズニング{名 | 記号}
  • 項： バンチのバンチ〈入れ子のバンチ〉
  • 閉じた項の意味： バンチ
  • 開いた項の意味： バンチ構成子

導出

  • 変数： 導出変数＝導出ラベル
  • リテラル： 導出リテラル
  • コネクティブ： 導出コネクティブ＝リーズニング{名 | 記号}
  • 項： 導出項
  • 閉じた項の意味： 導出
  • 開いた項の意味： リーズニング

バンチ計算システム

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

バンチ計算システムの構成素：

  1. 項
  2. バンチ
  3. 書き換え規則
  4. 書き換えアクション
  5. 書き換え系列〈sequence〉

説明：

  1. 項は構文的コンビネーション
    1. ツリー構造
    2. リーフは型付き変数または型付きリテラル、型は圏の対象
    3. リーフ以外のノードはコネクティブ
    4. 文法範疇があってもよい。
  2. バンチは項の構文木
    1. ツリー構造
    2. リーフは項
    3. リーフ以外のノードは区切り記号〈コネクティブ〉
  3. 書き換え規則は、個々の書き換えアクションのもとになるパターン
    1. 仮パラメータを持つかもしれない。
    2. 適用可能性条件が付くかもしれない。
  4. 書き換えアクション
    1. 書き換え規則の仮パラメータに実パラメータを代入して得られる。
    2. 書き換え規則の名前、実パラメータ、適用ロケーションからなる。
    3. 書き換えの対象となるバンチの一部をリデックス〈redex〉、書き換えの結果をリダクテッド〈reducted | contractum〉と呼ぶ。オペランドとリザルトがいいかも。
    4. 実際の書き換えに使える。書き換え系列に出現する。
  5. 書き換え系列
    1. バンチと書き換えアクションが交互に現れる系列。

項の文法とバンチの文法は類似、ときにまったく同じだが、項とバンチは区別する。項 ←→ バンチ の相互変換は、濃縮・希釈〈concentration dilution〉または折りたたみ・展開〈contraction expansion〉で行う。

バンチ書き換えと項書き換えは区別される。

ちなみに文法は次から構成される。

  1. 語彙〈終端記号の集合〉
  2. 文法範疇〈非終端記号の集合〉
  3. 書き換え規則＝生成規則
  4. 開始記号

文法はオートマトンと密接に関係する。

バンチ書き換えシステム＝バンチ計算システム、項書き換えシステム＝項計算システムは階層的に配置される。複数の計算システムの構造物・組織体を、計算システム連合〈federation of {calculation | calculating} systems〉と呼ぶ。現実の計算システムは連合を形成している。

演繹システムからリーズニングシステムへ

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

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

知識ベースは、ライブラリや組織化・配布形態であるパッケージ／モジュールと考える。知識ベースに対する操作は：

  1. 合併する。
  2. 分割する。
  3. キーとなる名前をリネームする。
  4. 知識ベース自体の名前をリネームする。
  5. 知識ベースにアイテムを追加する。
  6. 知識ベースからアイテムを削除する。
  7. その一部をまとめて指標やデビジョンを作る。
  8. 組織構造を変更する。
  9. アイテムを検索する。

これに関して次の疑問が出てくる。

  • アイテムとは何か？
  • 名付けられる対象と名付け方式は？
  • 組織構造とは何か？

文法も問題になる。

  • 構文木は、リーフをアトムと呼ぶ。例えば、論理式のアトム＝原子論理式＝述語呼び出し、算術式のアトム＝原子算術式＝数値リテラル、バンチのアトム＝原子バンチ＝論理式。
  • 構文木のリーフ以外のノードの付けられた“値”がコネクティブ。論理式のコネクティブ＝命題コネクティブ。算術式のコネクティブ＝算術演算子＝数値コネクティブ。バンチのコネクティブ＝論理式コネクティブ ←アリャリャ！

文法は、アトム変数とコネクティブを提供する。アトム変数への代入で“構文的に定数な”構文木が得られる。バインダーでバインドすることによって“構文的に閉じた”構文木が得られる。自由変数／束縛変数という概念は普遍的で、どの文法でも使える。

  • 型項文法： アトム変数は型変数。リテラルは型固有名。
  • 関数項文法： アトム変数は個体変数〈{object | individual} variable〉。リテラルは個体リテラル。
  • 命題文法： アトム変数は述語変数。（「命題変数」は真偽値変数）リテラルは固有述語記号。
  • 論理バンチ文法： アトム変数は論理式変数。リテラルは固有論理式記号（例、T、⊥）。コネクティブは区切り記号。区切り記号は $`{^\lor,}`$ など。
  • 導出項文法： アトム変数は導出変数〈ラベル〉。リテラルは固有導出記号（例：!_P）コネクティブは結合、ペアリングなど。
  • リーズニング項文法： アトム変数はリーズニング変数〈ラベル〉。リテラルは固有リーズニング{記号 | 名}。コネクティブは結合、積、ペアリングなど。

書き換え＝置換

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

広義の項書き換え系について考えている。書き換えと置換〈substitution〉は区別しなくていいだろう。とりあえず、3種類の書き換え＝置換がある。

  1. 関数項置換： 変数／リテラルをリーフとし、関数記号をノードとする構文木において、部分木（リーフノードも、ツリー全体も含む）を、他の木で置き換える。
  2. 命題項置換： 原子論理式〈アトム〉をリーフとし、論理記号をノードとする構文木において、部分木（リーフノードも、ツリー全体も含む）を、他の木で置き換える。
  3. バンチ置換： 論理式をリーフとし、構造構成子記号をノードとする構文木において、部分木（リーフノードも、ツリー全体も含む）を、他の木で置き換える。

関数項置換、命題項置換、バンチ置換の上に、導出の書き換え＝リーズニング、リーズニングの書き換え＝メタリーズニング が構成される。

置換のなかで可逆・双方向なものを、等値置換（関数項のとき）、同値置換（命題項／バンチのとき）と呼ぶ。

purescriptのインストールで問題

その他ソフトウェア 記録

NPMでインストールできて簡単、と思ったら PowerShell から実行できない。.bin という拡張子のファイルを実行しようとして、データ扱いされる。cmd.exe では実行できる。Webで調べた解決策は：

  • 環境変数 PATHEXT に .BIN を追加する。

自作のコマンドレット Set-util_Path を使った。

シーケント計算の再解釈の障害

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

「命題」の曖昧性

  1. 真偽値
  2. 述語
  3. 論理式
  4. （個体変数に関して）閉じた論理式

ところが、「論理式」が曖昧。

  1. テンプレート述語項構文木（リーフが穴、ノードが述語コネクティブ）
  2. テンプレート述語項構文木＋述語コンテキスト
  3. 評価値である述語

型理論のときも、型の意味が

  1. テンプレート型項構文木（リーフが穴、ノードが型コネクティブ）
  2. テンプレート型項構文木＋型コンテキスト
  3. 評価値である型
  4. 型そのもの（圏の対象）
  5. 型リテラル
  6. 型変数

一般に、次のものが混同される。

  1. モノそのもの〈シング〉
  2. モノを表すリテラル
  3. モノを代入できる型付き変数
  4. モノに対するコネクティブをノードとするテンプレートツリー構造
  5. 項 ＝ テンプレートツリー構造＋コンテキスト
  6. 項の評価値

対策： 次の概念を導入する。

  1. XXXを代入できる変数＝XXX変数 例：真偽値変数、述語変数、整数変数、ベクトル変数
  2. XXXを成分とするタプル〈部分ラベル付きリスト〉＝XXXコンテキスト 例：真偽値コンテキスト、述語コンテキスト
  3. XXXに作用するオペレーターを表すリテラル＝XXXコネクティブ 例：述語コネクティブ、実数コネクティブ、述語テンプレート・コネクティブ、型コンテキスト・コネクティブ
  4. XXXを表すテンプレートツリー＋XXXコンテキスト＝XXX項

シーケント計算の再解釈 4

メタリーズニングの種類：

  1. ApplyReasoning : reas, deriv ≡> deriv
  2. ComposeReasoning : reas, reas ≡> reas
  3. ProductReasoning : reas, reas ≡> reas

リーズニング 導出のマージ：

  1. MergeConj : conj → conj, con → conj ⇒ conj → conj
  2. MergeDisj : conj → disj, con → disj ⇒ conj → disj
  3. MergeConjLDist : conj → prop, con → disj ⇒ conj → disj
  4. MergeConjRDist : conj → disj, con → prop ⇒ conj → disj
  5. MergeDisjLDist : conj → prop, con → conj ⇒ conj → conj
  6. MergeDisjRDist : conj → conj, con → prop ⇒ conj → conj

リーズニング 導出の結合：

  1. Comp : conj → xxx, xxx → xxx ⇒ conj → xxx カット
  2. PostComp : conj → xxx ⇒ conj → xxx 知識ベース使用
  3. PreComp : conj → xxx ⇒ conj → xxx 知識ベース使用

リーズニング 導出のカリー化：

  1. 右カリー化
  2. 左カリー化

導出 族の濃縮

  1. 連言族の濃縮
  2. 選言族の濃縮

導出 命題の希釈

  1. 連言命題の希釈
  2. 選言命題の希釈

導出 型環境の外移動

まとめ
  1. リーズニング 導出のマージ モノイド積
  2. リーズニング 導出の結合 結合
  3. リーズニング 導出のカリー化 指数
  4. 導出 型環境の外移動
  5. 導出 族の濃縮
  6. 導出 命題の希釈

シーケント計算の再解釈 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} }
\newcommand{\conc}{\mathop{\#} }
\newcommand{\Subst}[1]{ \begin{bmatrix} #1 \end{bmatrix} }
%`$

次のオペレーターを考える。$`\alpha, \beta\in \mrm{TypeCtx}`$

  • $`\Dia_\alpha^\beta : \mrm{Prop}[\alpha]\to \mrm{Prop}[\alpha\conc\beta]`$
  • $`\forall_\alpha^\beta : \mrm{Prop}[\alpha\conc\beta]\to \mrm{Prop}[\alpha]`$
  • $`\exists_\alpha^\beta : \mrm{Prop}[\alpha\conc\beta]\to \mrm{Prop}[\alpha]`$

命題レベルの左右カリー化。$`\Gamma, \Delta \in \mrm{PropCtx}, Q\in \mrm{Prop}`$

  • $`\LLambda_{\Gamma, Q}^\Delta: \mrm{MultiDeriv}(\Delta\conc\Gamma, Q) \to \mrm{MultiDeriv}(\Gamma, [\Delta\triangleright Q])`$
  • $`\RLambda_{\Gamma, Q}^\Delta: \mrm{MultiDeriv}(\Gamma\conc\Delta, Q) \to \mrm{MultiDeriv}(\Gamma, [Q \triangleleft \Delta])`$

関数レベルの左右カリー化。$`\alpha, \beta \in \mrm{TypeCtx}, Y\in \mrm{Type}`$

  • $`\Llambda_{\alpha, Y}^\beta: \mrm{MultiFunc}(\beta\conc\alpha, Y) \to \mrm{MultiFunc}(\alpha, [\beta \triangleright Y])`$
  • $`\Rlambda_{\alpha, Y}^\beta: \mrm{MultiFunc}(\alpha\conc\beta) \to \mrm{MultiFunc}(\alpha, [Y\triangleleft \beta])`$

多関数 $`f:\alpha \to \beta`$ による置換

  • $`f^*: \mrm{Prop}[\beta] \to \mrm{Prop}[\alpha]`$
  • $`f^* Q = Q\Subst{f}`$

これに加えて：

  1. 連言の濃縮・希釈 バンチ演算
  2. 選言の濃縮・希釈 バンチ演算
  3. 全称命題の濃縮・希釈 拡大バンチ演算
  4. 存在命題の濃縮・希釈 拡大バンチ演算
  5. 同値置換 プレポスト結合 知識ベース使用 バンチ演算
  6. 各種のマージ 導出への演算
  7. ド・モルガン双対移動 導出への演算
  8. プレ結合 知識ベース使用 導出への演算
  9. ポスト結合 知識ベース使用 導出への演算
  10. カット

シーケント計算の再解釈 2

論理 半形式証明スクリプト
ド・モルガン双対

ド・モルガン双対をリスト〈バンチ〉に対して定義する。双対化演算は、

  • *(A1, ..., An) = (￢A1| ...| ￢An)
  • *(,) = (|)
  • *(A1| ...| An) = (￢A1, ..., ￢An)
  • *(|) = (,)
  • ** = id

と定義する。推論規則は

￢ 左
(Γ → Δ| Φ) ⇒ (*Φ, Γ → Δ)

￢ 右
(Ψ, Γ → Δ) ⇒ (Γ → Δ| *Ψ)

特別な場合として

￢ 左
(Γ → Φ) ⇒ (*Φ, Γ → (|))

￢ 右
(Ψ → Δ) ⇒ ((,) → Δ| *Ψ)
∧ 右 と ∨ 左 と限量子

まず、そのまま書く。

∧ 右
(Γ → Δ| A And, Π → Λ| B) ⇒ (Γ, Π ⇒Δ| Λ| A∧B)

∨ 左
(A, Γ → Δ And, B, Π → Λ) ⇒ (A∨B, Γ, Π → Δ| Λ)

構造規則を使って、Γ, Π を新たに Γ、Δ| Λ 新たに Δ と置いて：

∧ 右
(Γ → Δ| A And, Γ → Δ| B) ⇒ (Γ ⇒Δ| A∧B)

∨ 左
(A, Γ → Δ And, B, Γ → Δ) ⇒ (A∨B, Γ → Δ)

限量子

∀ 右
(Γ → Δ| A(a) ) ⇒ (Γ ⇒Δ| ∀x.A(x))

∨ 左
(A(a), Γ → Δ) ⇒ (∃x.A(x), Γ → Δ)

Σ とΠ を使うと：

Π 右
(Γ → Δ| A(i) ) ⇒ (Γ ⇒Δ| Πi.A(x))

Σ 左
(A(i), Γ → Δ) ⇒ (Σi.A(x), Γ → Δ)
⊃ 左

→ と ⇒ を使ってしまったので、含意を ⊃ にする。

⊃ 左
(Γ → Δ, A And, B,Π → Λ) ⇒ (A⊃B, Γ, Π → Δ, Π)

これは、マージとド・モルガン双対で解釈するのがいいかな。

マージ
(Γ → Δ, A And, B,Π → Λ) ⇒ (B, Γ, Π → Δ, Π, A)

ド・モルガン双対
(B, Γ, Π → Δ, Π, A) ⇒ (￢A, B, Γ, Π → Δ, Π)

連言濃縮
(￢A, B, Γ, Π → Δ, Π) ⇒ (￢A∧B, Γ, Π → Δ, Π)

同値置換 ￢A∧B ≡ A⊃B
(￢A∧B, Γ, Π → Δ, Π) (A⊃B, Γ, Π → Δ, Π)
リーズニング
  1. 連言の濃縮・希釈 バンチ演算
  2. 選言の濃縮・希釈 バンチ演算
  3. 全称命題の濃縮・希釈 拡大バンチ演算
  4. 存在命題の濃縮・希釈 拡大バンチ演算
  5. マージ バンチ演算
  6. ド・モルガン双対移動
  7. プレ結合 知識ベース使用
  8. ポスト結合 知識ベース使用
  9. 同値置換 プレポスト結合 知識ベース使用
  10. カリー化

シーケント計算の再解釈 1

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

シーケント計算をリーズニング構成の計算と考える。できるだけ少ないリーズニングで計算をしたい。

リーズニングを少なくするには、プリミティブな導出を揃える。

∧-モノイド構造 ∨-モノイド構造
![A] Θ[A]
Δ[A] ∇[A]
π1[A, B] ι1[A, B]
π2[A, B] ι2[A, B]
X[A, B] X[A, B]
A∧￢A → ⊥ T → A∨￢A

カット以外の構造規則はすべて、PreComp, PostComp で実現できる。

  1. A-増 左： PreComp[![A]]
  2. A-増 右： PostComp[Θ[A]]
  3. A-減 左： PreComp[Δ[A]]
  4. A-減 右： PostComp[∇[A]]
  5. (A, B)-換 左： PreComp[X[A, B]]
  6. (A, B)-換 右： PostComp[X[A, B]]

論理規則：

  1. ∧ 左1 ： PreComp[π1[A, B]]
  2. ∧ 左2 ： PreComp[π2[A, B]]
  3. ∨ 左1 ： PostComp[ι1[A, B]]
  4. ∨ 左2 ： PostComp[ι2[A, B]]

残るのは、

  1. ∧ 右、∀ 右
  2. ∨ 左、∃ 左
  3. → 左

知識ベースと半形式性

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

知識ベースには、次のようなものが入っている。

  1. 型の宣言・定義
  2. 関数の宣言・定義
  3. 命題の宣言・定義
  4. 導出の宣言・定義
  5. リーズニングの宣言・定義
  6. メタリーズニングの宣言・定義
  7. それらを組織化する構造ファセット

知識ベースを背景にして、新しい型／関数／導出／リーズニングを構成する行為が広義の計算。

このとき、半形式的記述の特徴は：

  1. あいまい検索： 知識ベースの特定のアイテム（宣言、定義、指標など）を検索する際に、曖昧指定でもなんとかなる。表記のゆれ（漢字かひらがなか、大文字小文字、人名表記、助詞のあるなし、etc.）や常識的な別名は許容される。また、文脈も考慮される -- 「オイラーの定理」が何を意味するか？ とか。
  2. パターンマッチング〈ユニフィケーション〉： 書き換えアクションの適用可能性〈applicability〉の判定にパターンマッチングが使われる。
  3. 暗黙の了解： パラメータを明示的に指定しなくても推測する。
  4. 後回しと前方参照： 一部の計算・証明を後回しにして、名前だけ付けておくことが出来る。
  5. 先行名付け： まだ定義してないものに名前を付ける。名付けの正当性証明の義務が発生する。