次は同義
- $`\text{we define example of type }T \text{ named }e`$
- $`\text{we define pointing function } e \text{ returns type }T`$
example〈事例 | 具体例〉は pointing function に展開されるが、of は語順を変えてしまう。of は戻り値型を先に記述して、名前を後に記述する形式を強制する。語順以外は、「of type ＝ returns type」。returns は、「returns 変数名 :∈ 型」を許すが、「of 変数名 :∈ 型」は許さない。
of は名前を後ろに移動するので、named で名前であることを明示。無名なら unnamed とする。「unnamed ＝ named _」。
問題は $`\text{example of type }T`$ の $`T`$ が何であるか？ $`\text{set } S`$ と $`\text{type }T`$ で、$`T`$ は型項で $`S`$ は集合項 ということになる。
- 集合項は、一回の解釈で直接的に ZFC の集合を denote する。
- 型項は、最初の解釈で構文的な展開処理がされる。それにより型のスキーマが得られる。つまり、型項は 型スキーマを denote する。型スキーマに外延化操作が施されてZFC集合が得られる。
- 外延化操作〈extensionalization〉は、名前を消すものと残すものがある。入れ子に対して再帰的に適用される。
型スキーマをZFC集合に外延化するには、事例作成〈examplify〉をときに無限に実行する必要がある。事例作成でできた事例達をすべて寄せ集めたZFC集合が型スキーマの外延化。
集合項〈set term〉は、型理論的内包から作ったZFC的集合を直接 denote できる。一方で、型項に集合項をどうやって入れるか？ は問題である。型定数、特に基本型定数とは何であるか？ 複合型定数とは何であるか？
型理論は、集合論と比べて、内包と外延の分離が難しい。外延に内包がへばりついている。内包情報を持った外延を扱う必要がある。それはファイブレーションかも知れない。
いずれにしても、記述言語〈DL〉において、型項と集合項の関係は大きな問題だ。
