語彙と構文、文法用語、意味論用語 - (保存用) 檜山正幸のキマイラ飼育記メモ編

構文的な対象〈テキスト〉が、

整形式〈well-formed〉 -- 文法に則っている。
解釈可能、可解釈〈interpritable〉 -- 値を（超越的には）求めることが出来る。有意〈significant | meaningful〉と同じ。
型つけ可能〈typable〉 -- 型を割り当て可能
型つけられている〈typed〉 -- 型を割り当て済み
相対解釈可能〈relatively interpritable〉 -- 環境〈文脈〉のなかで解釈可能
妥当、真 -- 論理式であり、解釈可能であり、値が真となる。

型理論は、解釈可能性を一意型つけ可能性で置き換える技術。型割り当て＝タイピングが終わっていれば（型つき）ならば、解釈可能性を保証する。

解釈可能性は、有意性と同じで有値性と言ってもよい（そんな言葉はないが）。あるいは評価可能性〈evaluable〉。このときの有値性は、超越的に考えている。計算的（実効的、構成的）に考えているわけではない。

超越的：超越機械により、真偽判断が可能である。
計算的：理想機械により、真偽判断が可能である。

超越機械と理想機械の計算力は決定的に違う。「決定的に」の意味は：

理想機械で実行できる計算は、超越機械で実行できる。
超越機械で実行できる計算で、理想機械では実行できないものがある。

実在機械と理想機械のあいだには、ここまで決定的な断絶はない。

それはそうと、文法用語：

定数 -- 計算なしに値に評価可能
変数 -- 単なる名前、束縛（割り当て）により環境を構成する
関数名 -- 環境があれば、評価可能。関数名も変数。
述語名 -- 環境があれば、評価可能。述語名は関数名の一種。
項 -- 環境により評価可能。定数または関数呼び出し式。
論理式 -- 環境により評価可能。論理式は項の一種。

これが通常の常識的な文法（構文ルール）。ラムダ構文を入れると、

関数名の置換体〈replacement〉として、関数項が使える。
述語名の置換体として、述語{関数}?項が使える。

ラムダ構文付きで考えると、項はラムダ項であり、その一部に関数項〈関数抽象〉がある。重要なことは、項に自由変数があることで、自由変数の値は環境からもらう。よって、自由変数が残った項を環境無しで評価することはできない。できないことは出来ない。

以上のことから、構文レベルで次を入れるべき：

ラムダ抽象〈関数抽象〉、ラムダ束縛
全称限量子〈量化子 | 限定作用素〉、全称束縛
存在限量子、存在束縛

ボトム定数（⊥_A）も入れたほうがいいのかな？ボトム定数を入れれば、標準解釈はSetではなくて、PtSet^nonsになる。ただし、PtSet^nonsは直和が作れない。直和を作りたいなら、非空相対集合の圏RleSetに拡張する必要がある。すると、多変数関数の引数評価戦略が影響してくる。ムー。論理OR"∨"の解釈に影響する。

ここらへんも、超越機械と理想機械の違いだな。理想機械では、∨と∃について、実行の打ち切りが起きる。超越機械では打ち切りの必要はない（打ち切ってもコストは変わらないので）。理想機械では、∀を確認できるはずはないので、否定命題の反例を探しにいく。結局、真な∀命題は直接確認はできない。