Caty用語の整理

従来からのCaty用語も整理。

TYPEを型（の意味）全体の集合、Mを計算モデル圏とする。

• コマンド -- プロファイルと実行ボディの組。名前を持つか持たないかは理論上は重要ではない。
• プロファイル -- 同一の型変数スコープ内に置かれた2つの型項のタプル
• ネイティブコマンド -- 実行ボディがネイティブ言語で書かれたコマンド
• スクリプト -- CatyScript言語の式
• スクリプトコマンド -- 実行ボディがスクリプトであるコマンド
• 総称型 -- 型パラメータを持つ型。nパラメータの総称型の意味は、TYPEⁿ⊃→|M| という写像。
• 総称プロファイル -- 型パラメータを持つプロファイル。nパラメータの総称プロファイルの意味は、TYPEⁿ⊃→|M|×|M| という写像。
• 総称コマンド -- 型パラメータを持つコマンド。nパラメータの総称コマンドの意味は、TYPEⁿ⊃→M という写像。
• 総称スクリプト -- 型パラメータを持つスクリプト。式内に総称コマンドを含む。プロファイルが指定されないと意味が定義できない。
• 型制約 -- TYPEⁿの部分集合を定義する論理式
• カインド制約 -- 型制約の一種で、ある構文的制限を持った論理式で定義される1パラメータの型述語
• カインド -- カインド制約、またはカインド制約が定義するTYPEの部分集合
• （Catyの）型具体化 -- 総称型、総称プロファイル、総称コマンド、総称スクリプトの型パラメータへの具体型の割り当て
• 総称整合性条件 -- 総称型、総称プロファイル、総称コマンド、総称スクリプトの型パラメータ領域TYPEⁿに関する条件で、n型パラメータの型関数（広義）の定義域を特徴付ける型制約。
• 整合的な型具体化 -- 総称型、総称プロファイル、総称コマンド、総称スクリプトの型具体化で、総称整合性条件を満たすもの。

ついでに(?)、総称コマンドの例

1. pass<X> :: X-> X
2. pr-1<X, Y> :: [X, Y] -> X
3. pr-2<X, Y> :: [X, Y] -> Y
4. in-1<X, Y> :: X -> (@1 X | @2 Y)
5. in-2<X, Y> :: Y -> (@1 X | @2 Y)
6. diag<X> :: X -> [X, X]
7. cons<X> :: [list<X>, X] -> list<X>
8. car<X> :: list<X> -> X throws EmptyList
9. cdr<X> :: list<X> -> list<X> throws EmptyList

2型パラメータ、1型パラメータのpassは次のように定義される。

• pass/<2> = Λ<X, Y: X⊆Y>(X->Y).λx:X.x
• pass/<1> = Λ<X>(X->X).λx:X.x