MEDL（Mathematical Entity Description Lang.）とDIDL（Drawing Instruction and Description Lang.）について。
DIDLはある程度は汎用の絵図記述言語。だが、直接的な目的は証明記述。「証明」は曖昧語なので、テクニカルタームとしては導出〈derivation〉を使う。「推論」もテクニカルタームとしては使わない。
「項」はテキスト記号表現〈テキスト・コンビネーション〉の意味で使う。項の種類は：
- 型項
- 関数項（定数項含む）
- 命題項＝論理式
- 導出項（＝証明項、使わない）
ここでの「定数項」はプロファイルが 1 → A の形の関数項のこと。ちなみに定数の意味は：
- 自由変数、束縛されてない変数
- 域が生成対象〈generator object〉である射
- 終対象／生成対象を経由する射
- 置換〈代入〉を許されない記号、リテラル、コネクティブなど
登場する圏類似構造
- 型の圏 ≒ 集合圏
- 型の複圏 ≒ 集合の複圏
- 型コンテキストの圏 ： 対象は型コンテキストで、射は割り当て系〈system of assignment〉。射を置換〈substitution〉とは言わない。対象を型判断とは言わない。
- 命題の複圏： 対象は命題で、複射は導出
- 命題の多圏： 対象は命題で、多射は導出系〈system of derivations〉
型の圏、型の複圏は、型コンテキストの圏に埋め込める。型の多圏と型コンテキストの圏は、変数がある点で違う。
型コンテキストの圏の対象ごとに、そのコンテキスト上の命題の多圏が載る。インスティチューションまたはハイパードクトリン。型コンテキストの圏の射である割り当て系により置換または翻訳と呼ぶ引き戻し多関手が定義される。演繹システムの“規則”としては、引き戻し反変多関手（インスティチューションでは反変共変が逆になる）を SUBSTITUTION と呼ぶ。以下の“規則”はすべて SUBSTITUTION の特殊ケースとなる。
- PROP-WEAKENING
- PROP-COTRACTION
- PROP-EXCHANGE
- PROP-FUNCTION-TERM-SUBSTITUTION （狭義の SUBSTITUTION）
共通構造とカリー／ハワード／ランベック対応
型の圏と命題の圏は共通構造を持っている。
- どちらもデカルト閉圏である。
- したがって、モノイド積、単位終対象〈終対象対象〉、終射、カリー化／アンカリー化、ペアリング、射影〈破棄射〉、対角〈コピー射〉を持つ。
- 複圏または多圏のオペレータ（命題ではリーズニング）として次がある。IDENTITY, GRAFTING, MULTI-COMPOSITIO, WEAKENING, CONTRACTION, EXCHANGE。
- 型の圏がパイ型をサポートすると、∀限量子と同じ議論ができる。
- 型の圏も命題の圏もパイ構成を持つなら、λΠ-計算が出来る。圏の種別〈ドクトリン〉はCCCΠ〈Cartesian Closed Category with Π〉
- SUBSTITUTION = TRANSLATION によって、インスティチューションまたはハイパードクトリン的な構造を導入できる。
- 命題の圏は、CCCなだけではなくて直和を持ち、デカルト閉半環圏になる。
- 命題の圏は、Π構造と双対なΣ構造も持つ。
- 型の圏と命題の圏は共通構造が多いので、同じ計算メカニズムが使える。
- 型の圏のなかに真偽値対象があれば、命題の圏を構成できる。この場合、命題を関数と思える。
用語法
- 型コンテキストを単にコンテキストということがある。
- 型コンテキストを型判断、または判断と呼ぶことがある。
- 割り当て系を判断と呼ぶことがある。
- 割り当て系を置換〈substitution〉と呼ぶことがある。
- 割り当て系の成分〈tuple component〉＝割り当て を判断と呼ぶことがある。
- 割り当て系の成分〈tuple component〉＝割り当て を置換と呼ぶことがある。
- 型コンテキストと指標が混同されることがある。型コンテキストを無法則指標とみなすことがある。
- 関数項による割り当てと、導出が混同されることがある。アビタである複圏が違う。
- 導出と導出のプロファイル〈シーケント〉が混同されることがある。
- 関数項を項と呼び、それ以外の項を項とは呼ばないことがある。
- 命題項は論理式と呼ぶ。
- 導出項を証明{項 | オブジェクト}と呼ぶことがある。
- 導出または導出項を推論と呼ぶことがある。特に基本導出{項}?を推論と呼ぶ傾向がある。
- 導出に作用するオペレータであるリーズニング、特に基本リーズニングを推論と呼ぶことがある。
- リーズニングが含めたコンステレーション図のバエズ／ドーラン・ツリーを証明と呼ぶことがある。
- ここでの置換は、項に作用する置換オペレータ〈置換リーズニング | 置換アクション | 置換コマンド〉である。
- 置換オペレータは関手なので、導出にも作用する。
- 置換オペレータ〈翻訳オペレータ〉＝置換関手〈翻訳関手〉の随伴により限量子〈量化子〉関手が定義される。
- 限量子関手の一部は限量子オペレータ。つまり、限量子リーズニング。
