定義のメカニズム
データ型と型シノニム - 檜山正幸のキマイラ飼育記 メモ編 で、コンプリヘンションとコンビネーションと言ったが、
- コンプリヘンション（了解）
- コンストラクション（構成）
にする。定義を、
- 了解〈コンプリヘンション〉による定義
- 構成〈コンストラクション〉による定義
に分ける。了解による定義には、それを支える了解方式〈コンプリヘンション・スキーマ〉が必要。構成のときは、構成方法を表すコンストラクタが必要。別名：
定義が付値のことなのか、着項のことなのかが曖昧で、通常は、「着項すれば付値される」を暗黙の前提にしている。
- 了解による定義では、了解方式を記述項を書けば、それが付値を意味する。構文的に正しい記述項（構成項とは違う）は自動的に付値を保証して、その背景は了解方式である。
- 構成による定義では、名前に構文的に正しい構成項を着項する。しかし、着項により付値は保証されない。構成項の要求指標〈requiremtn signature〉が付値されてないといけない。付値された要求指標とは、要求指標上のモデルに他ならない。つまり、付値可能条件は、構成項の要求モデル〈requirement model = requirement signatureのmodel〉が指定されていること。
- 要求モデルのなかで、要求項は評価されるが、評価には評価用の射が必要で、それは要求モデル・要求項より次元が上がったモデルが必要。その評価モデルは、通常はシステムでbuiltinに提供される。
「定義」に関連したことで、特殊な次元で特殊な事象が起きることがある。
次元0だ（0-射だけ考える）と、区分け＝プロファイリングになる。特殊事情だ。圏を指定すると、その圏が有界（有限なnでのn-圏）だとすると、(n + 1)-射は、n-射の等号になる。つまり、(n + 1)-ホムセットが単元集合になる。ホムセットが単元だということは、プロファイリングすると付値が保証される。
- 0次元では、区分けがプロファイリングを保証する。
- (n + 1)次元では、プロファイリングが付値を保証する。
圏がn-等式的とは、(n + 1)-射が、n-射の恒等に限ること。通常の圏は、1-等式的だとして扱っていると思う。証明の圏がやっかいのは、1-等式的ではないことである。
圏の議論を単純化するためにワイヤーフレームを取るが、もとの圏とワイヤーフレーム圏、さらにはワイヤーフレームの骨格（＝リンデンバウム／タルスキー圏）がゴッチャになっていて、どこの何を指しているのかが不明になっている。
StandardMLでfunctorを使っているのは、代入子が共変でリダクト関手を誘導するから、代入子とリダクト関手を同一視してもいいだろう、ということだが、これをやっていると、そのうち何がなんだか分からなくなる。「クワってプロフする」のがとても大事。
