計算の構造

構文論：

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

構文論の基本概念であるが、シングは意味領域の対象物〈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. 評価＝計算