色々な対応関係

セミナー セオリー論

暫定案、後で修正。

日本語だと複数形がないので、複数形の代わりに「ナントカセット」とする。

セオリー論 プログラミング 論理 ストリング図
指標 インターフェイス 推論規則セット スパイダーセット〈アイコンパレット〉
ソート 型 命題 ワイヤー（のラベル）
オペレーション サブルーチン 定理 名前付きストリング図
基本オペレーション 組み込みサブルーチン 公理 スパイダー
オペレーション宣言 サブルーチンプロトタイプ 定理宣言 -
オペレーションボディ サブルーチンボディ 定理の証明 名前付きストリング図のストリング図
リファクタリング 証明の書き換え ストリング図の書き換え
構文モナド プログラミング言語 論理言語 描画法
クライスリ射 ライブラリ セオリー ストリング図キット
クライスリ結合 ライブラリのマクロ展開 セオリーの定理展開 ストリング図の展開
モデル マシン、エンジン モデル

別な対応表

プログラミング 論理
ユーザー、プログラマ 証明者〈prover〉
プログラミング 証明行為〈proving〉
テキストプログラミング言語 テキスト論理言語
グラフィカルプログラミング言語 グラフィカル論理言語
インターフェイス 指標〈シグネチャ〉
型 論理式〈命題〉
？ シーケント〈プロファイル〉
宣言〈プロトタイプ ｜ シグネチャ〉 宣言（借用）
サブルーチン定義 定理
サブルーチン定義ヘッド 定理ヘッド（借用）
サブルーチン定義ボディ 定理ボディ（借用）
プログラムコード 証明{図}?
呼び出し数 呼び出し数（借用）＝ノード数
ライブラリ セオリー
組み込みサブルーチン 公理／推論規則
引数型 仮定
戻り値型 結論
ランタイムエンジン／ハードウェア モデル
コンパイル／トランスパイル トランスパイル（借用）

必要な用語：

  • 絶対証明： 仮定が空な証明
  • 絶対シーケント： 右片側シーケント、絶対証明のシーケント〈プロファイル〉
  • 単純証明＝基本証明： ノード数が1の証明{図}? 公理、推論規則と同一視できる。
  • 絶対単純証明＝絶対基本証明： 論理式リストと同一視できる。もちろん、公理、推論規則と同一視できる。
  • {コンパクト}?カリー化： コンパクト論理におけるカリー化コンビネータ
  • 絶対化： 与えられた証明図を絶対証明図にするリーズニング、演繹定理から（カリー化の繰り返しで）出来る。

非形式「証明」の解釈：

  1. 証明図〈proof {figure | diagram}〉
  2. 証拠式〈witness expression〉
  3. リーズニング図 （証明図とリーズニング図の区別は出来てない）
  4. 定理の証明部（構成素名、役割名）
  5. 証明行為〈proving〉

非形式「定理」の解釈：

  1. 指標内の宣言
  2. ヘッド付き証明〈headed proof〉
  3. ヘッド付き証明のヘッド
  4. セオリー〈ライブラリ〉のインスタンス

非形式「公理」の解釈：

  1. 指標内の宣言
  2. ヘッド付き証明〈headed proof〉、ただし証明は単純証明
  3. ヘッド付き証明のヘッド、ただし証明は単純証明
  4. セオリー〈ライブラリ〉のインスタンス

公理証明、推論規則、基本証明、単純証明 が同義語、公理命題と公理絶対証明〈絶対推論規則 | 絶対基本証明 | 絶対単純証明〉は同一視可能。たくさんの同義語、ほんとは違うが習慣的に同一視することが混乱と誤解をまねく。