各種のオペレーターの呼び名

なんかもう、ひたすら単語の選択と（必要なら）造語をしている。いいかげんウンザリはしている。

全般的に、用語法において、関数と関数を表す式と関数値の区別が付いてない／付けてないことが分かる。これは普遍的（どこでも見いだせる）な現象だ。関数まわり混同現象と呼ぼう。

値＼引数	個体-引数	型-引数	命題-引数	推論-引数	リーズニング-引数
個体-値	関数,個体族	例：選択関数	例：ヒルベルトε	-	-
型-値	型族	型構成子, 総称型	例：コンテキスト領域	-	-
命題-値	命題関数, 命題族	型総称命題	結合子,命題構成子	例：プロファイル	-
推論-値	推論族	型総称推論	命題総称推論, 推論規則	リーズニング,推論構成子	例：プロファイル
リーズニング-値	リーズニング族	型総称リーズニング	命題総称リーズニング	推論総称リーズニング, リーズニング規則	リーズニング構成子

• ※ 「XXXの族」は、「XXXのリスト」、「コンテキストボックス内XXXの集まり」の概念を含む。
• ※ 型構成子と総称型は、演算子と式の違いがある。関数まわり混同現象がある。
• ※ 型総称命題の型パラメータは、コンテキストと限量子に現れる。
• ※ 命題のコンテキスト領域は、命題がコンテキスト付き〈コンテキスト内に置かれている〉ときだけ。ただし、どんなwell-suited〈ウェルスーテド〉な命題もなんらかのコンテキストに置かれていると考えてもよい。
• ※ 推論のプロファイルは、正確には命題のリストのペアである。
• ※ リーズニングのプロファイルは、正確には推論のリストのペアである。

無引数の場合：

	無引数演算子記号	値の種別
個体-値	個体定数	個体の型
型-値	型定数, 型名	型のカインド
命題-値	述語定数	述語の域型
推論-値	推論{規則}名	推論のプロファイル
リーズニング-値	リーズニング{規則}名	リーズニングのプロファイル

• ※ 述語定数は命題引数を持たないが、個体引数を持っている。個体引数も持たないときは論理定数、命題定数。
• ※ 推論規則は、命題引数〈命題総称のパラメータ〉は持つ。推論引数は持たないので、推論構成子ではない。
• ※ 推論のプロファイルは、（総称かも知れない）命題リストのペアである。
• ※ リーズニングのプロファイルは、（総称かも知れない）推論リストのペアである。

様々なオペレーターとその名前（固有名詞）、仮引数、実引数、引数種別、戻り値種別 を明確に書く記法が必要だが、ないのだな。はぁーー（溜息）。例によって、

• {引数 | 変数 | パラメータ | インデックス}
• {引数 | 変数 | パラメータ | インデックス}{の}?{型 | 変域 | 域 | 領域 | ドメイン | 集合}

の同犠牲問題もあるし。

ついでに、式の呼び方：

値＼変数	個体-変数	型-変数	命題-変数	推論-変数	リーズニング-変数
個体-値	項	-	-	-	-
型-値	型族式	{型}?総称型式	-	-	-
命題-値	命題関数式	型総称論理式	命題総称論理式	-	-
推論-値	推論族式	型総称推論式	命題総称推論式	推論総称リーズニング式	-
リーズニング-値	リーズニング族式	型総称リーズニング式	命題総称リーズニング式	推論総称リーズニング式	リーズニング総称リーズニング式

• ※ たいていの命題〈論理式〉は、命題関数式になっている。
• ※ たいていの推論{式 | 表現}は、推論族式＝“命題関数式のリストのペア”になっている。
• ※ 型式は「ケイシキ」ではなくてカタシキ。
• ※ 総称パラメータは、{テンプレート | パターン}{変数 | パラメータ | 引数} または プレースホルダー とも呼ばれる。

代入、具体化の言い回しも：

• 個体変数に個体式〈項〉を{個体 | 値}代入、{個体 | 値}変数を{個体 | 値}具体化
• 型変数に型式を型代入、型変数を型具体化
• 命題変数に命題式〈論理式〉を命題代入、命題変数を命題具体化
• 推論変数に推論式〈リッチシーケント〉を推論代入、推論変数を推論具体化
• リーズニング変数にリーズニング式をリーズニング代入、リーズニング変数をリーズニング具体化

名前のルール、名前集合〈name set | set of names〉と式集合〈expression set | set of expressions〉：

種別	システム内の変数	変数を表すメタ変数	メタ変数の変域
個体	x, y	同じ	IndivVar
型	なし	X, Y	TypeConst
命題	A, B, P, Q	同じ	PropVar
推論	F, G	同じ	InferVar
推論のラベル	なし	f, g	InferLabel
命題のリスト	なし	Γ, Δ	PropList
リーズニング	なし	ξ, η	ReasExpr
コンテキスト	なし	α, β	Context