構文領域と意味領域

思い付いたことを順不同にダダーっと箇条書きにする。後で整理する。まだごった煮。

先に意味領域：

1. 集合の集合がある。小さい具象圏の対象集合 ＝ Type ＝ |Sem|
2. 0, 1 はType内にある。0, 1∈Type
3. 型がAの個体〈individual〉とは、1からのAへの射のこと。
4. 関数はSemの射。個体は射の一種。
5. Semはデカルト閉圏。
6. Semは直和も持っている。
7. 圏Semは、コンテキスト領域〈議論の領域〉と代入（の意味である関数）の圏。
8. 構文領域〈semantic realm〉が決まれば、個体変数を使ってコンテキストを作れる。コンテキストは、Sem上のファイバーリング構造を持つ。
9. {個体}?定数記号、{個体間}?関数記号とその意味が決まれば、代入の意味も決まる。
10. 集合（＝コンテキスト領域）XごとにPow(X)を付ければハイパードクトリンになる。
11. 代入の意味である関数からなるSemの部分圏と、その上のPowハイパードクトリン（もとのハイパードクトリンの部分ハイパードクトリン）ができる。
12. 述語{定数}?記号〈関係{定数}?記号〉の意味が定まれば、論理記号の意味は固定だから、論理式の意味が決まる。
13. リスト（連言的リストと選言的リスト）の意味も決まる。意味＝真理集合＝一般化された真偽値は、リストの場合も、コンテキスト領域XのPow(X)の要素。
14. リストは、集合 1..n = {1, .., n} をインデックスとするインデックス族〈indexed family of popositions〉に連言マーカー、選言マーカーが付いたもの。
15. リスト（連言的リストと選言的リスト）の一般化として、連言的インデックス族と選言的インデックス族を考えることが出来る。
16. インデックスセットがXである連言的命題族は、連言的Xコンテキスト内に置かれた命題の集まり。インデックスセットがXである選言的命題族は、選言的Xコンテキスト内に置かれた命題の集まり。
17. コンテキスト領域という概念は、それ自体は意味側の単なる集合だが、構文側と意味側を繋ぐ役割を果たす。
18. 連言的Xインデックス付き命題〈論理式〉族と選言的Xインデックス付き命題〈論理式〉族に対する意味は集合論的に真理集合として定義できる。
19. そして、真理集合の包含関係として、シーケントの二値的真偽が定義できる。
20. シーケントの二値的でない真偽値＝真理集合も定義はできる。
21. シーケントの真偽値（二値または集合値）とは、推論の真偽値だから、さらにリーズニング（推論に対する推論 ＝ 2-推論）の真偽値も定義できる。

そうか、次元（次数）でいいのか：

1. 0-推論 ＝ 命題
2. 1-推論 ＝ 推論〈証明〉
3. 2-推論 ＝ リーズニング

次に構文領域：

1. 型： 型定数記号、型変数記号、型オペレーター記号（型値）がある。型定数記号の意味は決まっている。
2. 型： 型を表す形式的型表現が決まる。形式的型表現に名前を付けると名前付き型コンビネータができる。型コンビネータは型パラメータを持てる。型パラメータのソートはTypeである。
3. 個体： 個体定数記号、個体変数記号、個体オペレーター記号（個体値）＝関数記号 がある。個体定数記号の意味は意味領域の個体＝射として決まっている。
4. 個体： 個体を表す形式的個体表現が決まる（項）。形式的個体表現に名前を付けると名前付き個体コンビネータ（ユーザー定義関数）ができる。個体コンビネータは個体パラメータを持てる。個体パラメータのソートは型（意味は集合）である。
5. 個体変数記号と型定数記号によりコンテキストを構文的に定義できる。
6. 命題： 命題定数記号、命題変数記号、命題オペレーター記号（命題値）がある。命題定数記号の意味は決まっている。
7. 命題： 命題を表す形式的命題表現（それが論理式）が決まる。形式的命題表現に名前を付けると名前付き命題コンビネータができる。命題コンビネータは命題パラメータを持てる。命題パラメータのソートはProp[α]である。αはコンテキスト。
8. 推論： 推論定数記号、推論変数記号、推論オペレーター記号（推論値）がある。推論定数記号の意味は決まっている。
9. 推論： 推論を表す形式的推論表現（推論式、推件式）が決まる。形式的推論表現に名前を付けると名前付き推論コンビネータができる。推論コンビネータは推論パラメータを持てる。推論パラメータのソートは推論のプロファイルである。

構文領域にある集合：

1. TypeConstSymb, TypeVarSymb, TypeOperSymb, UserTypeOperSymb, TypeExpr, TypeSortExpr = {Type}
2. IndivConstSymb, IndivVarSymb, IndivOperSymb, UserIndivOperSymb, IndivExpr, IndivSortExpr = TypeExpr
3. PropConstSymb, PropVarSymb, PropOperSymb, UserPropOperSymb, PropExpr, PropSortExpr = TypeExpr
4. InferConstSymb, InferVarSymb, InferOperSymb, UserInferOperSymb, InferExpr, InferSortExpr = PropProfileExpr

	Const	Var	Oper	UserOper	Expr	Sort
型	型名	型変数	型構成子	型構成子	型式	型のカインド
個体	定数	変数	関数	関数	項	個体の余域型
命題	述語記号	命題変数	結合子	命題構成子	論理式	命題の域型
推論	推論定数	推論変数	リーズナー	タクティク	推論式	推論プロファイル

述語記号と総称性がうまく説明できてない。
コンテキスト＝インデックスセットも説明が必要だ。項変数は要らないのか？ 次が別に必要。

• 個体変数を持った命題 ＝ 命題関数 ＝ インデックス付き命題族
• 命題変数を持った推論 ＝ 総称的推論 ＝ 推論規則
• 個体変数を持った型 ＝ インデックス付き型族

有限	任意
インデックス i	自由変数 x
インデックスセット 1..n	コンテキスト領域 X
リスト (i∈1..n … )	コンテキスト付き論理式 (x∈X …)
リストからの成分 A[k]	ボックスからの具体化 A[a]
同一成分リスト	自由変数を持たない論理式が入ったボックス
n複製Δn	Xコンテキスト水増しΔX

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

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

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

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

• ※ 「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

アニメムービー用語

1. マルチスクリーンムービー
2. ムービーフィルム
3. フレーム（のコンテンツ）
4. 絵コンテ〈ストーリーボード〉
5. {絵コンテの{コマ | シート} | {ストーリー}?シート}
6. シーン
7. {アクション}?コマンド
8. スクリプト（ActionScriptは固有名詞）
9. スクリプトのユーザー定義関数
10. オープニングフレーム
11. エンディングフレーム

アニメムービー	論理
ムービーフィルム	{フル}?リーズニング図
フレーム（のコンテンツ）	推論図
絵コンテ	(LK証明図の集まり)
シート	(LK証明図＝)推論シート
シーン	部分リーズニング図
コマンド	基本リーズニング
スクリプト	リーズニング式
ユーザー定義関数	リーズニングタクティク
オープニングフレーム	開始推論図
エンディングフレーム	終了推論図
-	推論図のプロファイル

ダメな言葉と矢印のまとめ

	名詞	動詞能動態	形容詞-済み	形容詞-可能
証明	×	×	○ 推論は-	○ 推論は-、命題は-
推論	○	△ 仮定が結論を-	×	×
リーズニング	○	○ 上式が下式を-	○ 推論は-	○ 推論は-

言い方の候補：

• Γ infers Δ
• Γ concludes Δ
• Γ derives Δ
• Γ entailes Δ
• ξ reasons η
• ξ conclues η
• ξ entailes η

動詞の能動態のときは、主語が何であるかが難しい。仮定が結論を推論するのか？ それとも、私が仮定から推論を推論するのか？ 主語「私」は違うな、私だとすると「その推論（名詞）を正しいと確信している」のが私だ。

ついでに矢印：

• ⇒ 含意、前件、後件
• → 推論（シーケント）、左辺＝仮定、右辺＝結論
• ▷ リーズニング、上式、下式、{開}?始式、終{了}?式
• リーズニングでは、前フレーム、次フレーム、オープニングフレーム、エンディングフレームも使う。

縦方向	横方向
なし	⇒
---	→
===	▷

証明と呼ばれるかも知れないモノ

推論を次のように規定する。

1. 推論には必ずプロファイルがある。
2. プロファイルは仮定命題リストと結論命題リストからなる。
3. 推論はラベル付きのときもあれば、ラベル無しのときもある。
4. 推論は組み込みのときもあれば、ユーザー定義のときもある。
5. 組み込み推論は、必ずラベルを持つ。
6. 組み込み推論は、ラベルとプロファイルだけで定義される。
7. ユーザー定義の推論は、組み込み推論から初めてリーズナーを適用して作る複合推論である。
8. ユーザー定義の推論を推論ライブラリに編成してよい。

リーズニングも同様に規定できる。

で、証明と呼ばれる可能性があるモノ。

1. 推論{図}? ＝ 証明{図}?
2. 組み込みではない推論{図}? ＝ 証明{図}?
3. リーズニング{図}? ＝ 証明{図}?
4. リーズニングのストーリーシート ＝ 証明{図}?
5. 組み込みではないリーズニング ＝ 証明{図}?
6. 組み込みではないリーズニングのストーリーシート ＝ 証明{図}?
7. ラベル付き登録済み推論図またはラベル付き登録済みリーズニング図のボディ

これなんで、定理も同じだけのバラエティがある。まともなコミュニケーションが出来るわけがない。

次を事前に定義する。

1. 推論{図}? ＝ スパイダー ＝ ノード・ワイヤー図
2. 組み込み vs. ユーザー定義
3. リーズニング{図}?
4. {ストーリー | {絵}?コンテの}シート ＝ 注釈付き累積推論図