続・意味不明な言葉達 対策
絵を中心に考えるしかないだろう。
で、絵のノードだが、誤解を招きそうな気がしてきた。ノード → スパイダーと改名したほうがいいかも知れない。グラフ理論の頂点とは違って、むしろ近傍部分グラフみたいなものだから。
スパイダーは脚を持つ。脚の付け根をピンと呼び、「ピン付きノード＋ワイヤー」と考えることもある。ピンの代わりにジャック（穴、凹）があり、ワイヤー側にプラグ（凸）があると考えてもいい。ワイヤーラベルは、ピン／ジャック／プラグのラベルになる。物理的、器具的な比喩は、繋がればなんだっていい
スパイダーが、「定理、推論、証明、推論規則、論理的公理、分野固有の公理」などに対応する。スパイダーに関する性質として：
- ラベルあり ←→ ラベルなし
- 組み込み ←→ ユーザー定義
- 総称 ←→ 具体的
- 絶対（入力自明） ←→ 相対（入力が自明でない）
- 定義／記述 ←→ 呼び出し／使用
などがある。
暫定的にスパイダーを推論〈inference〉と呼ぶことにして：
- ラベル付き推論 ←→ ラベルなし推論
- 組み込み推論 ←→ ユーザー定義推論
- 総称推論 ←→ 具体的推論
- 推論の定義／記述 ←→ 推論の呼び出し／使用
これらの説明で、次の用語が有効かも知れない。
- 基本〈アトミック | プリミティブ〉スパイダーとクラスタースパイダー
- 単一スパイダーと図〈フィガー | ピクチャー | ダイアグラム〉
- 命題変数、項変数、個体変数〈個体変項〉、個体式 ＝ 項、命題式 ＝ 論理式
以上の設定で、おおよその対応は：
- アトミックではないスチル絵図 → 証明
- スチル方式〈NK方式〉における定理ボディ → 証明
- 総称で入力が自明でないスパイダー → 推論規則
- 総称で入力が自明なスパイダー → 論理的公理
- 分野固有の公理は、総称ではないスパイダーで表現される。
それと、別な大きな問題は：
- システム内ラベルとメタ変数の区別がしにくい。
- 特にシステム内ラベルを表現するメタ変数が登場すると非常に厄介。
図示での問題は、
- ムービーが分岐してるときのマルチフレームと、単一フレームに合流されたときの違いが明確ではない。なぜなら、フレームを区切る記号がないから。
- 2本のワイヤー／ケーブルのあいだの中間領域が連言的か選言的かが分からない。中間領域を明示する習慣がないから。
ウワーッ、、、、、問題だらけだーーー！！
