計算の構造

構文論:

基本概念 別名
ラベル 名前, 変数, 不定元, 定数, 識別子
シング 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. 評価=計算