続・証明とリーズニング

コンテキストの階層は、外から内に向かって：

1. ライブラリコンテキスト＝知識ベース
2. ワーキングコンテキスト＝ステージコンテキスト
3. 判断コンテキスト または 問題コンテキスト

コンテキスト＝混合コンテキストには次のものが格納される。情報の重複がある。自動導出は、関数定義／定理定義からの導出。

型宇宙	命題宇宙
関数定義	定理定義
ラベルの結果型宣言	ラベルの結果命題宣言
（上に同じ）型の要素変数宣言	（上に同じ）命題の証拠変数宣言
関数名のプロファイル宣言（自動導出）	定理名のシーケント宣言
計算項の結果型宣言（自動導出）	証明項の結果命題宣言（自動導出）
関数名への計算項割り当て（自動導出）	定理名への証明項割り当て（自動導出）
定義的等式 ≡（自動導出）	定義的同値式 ≡（自動導出）
関数名からボディへの書き換え規則（β変換）	定理名からボディへの書き換え規則（β変換）

関数定義 (f := t) : Γ |- A から次が導出される。

1. f: Γ |- A 関数名のプロファイル宣言
2. t : A 計算項の結果型宣言
3. f := t 関数名への計算項割り当て
4. f ≡ t 定義的等式
5. f ~→ t, f a ~→ t[a/x] 関数名からボディへの書き換え規則（β変換）

関数名のプロファイル宣言は次のようにパッキング〈レイフィケーション〉される。

• f: Γ |- A プロファイル宣言
• f^ : |- Γ→A 右辺は依存アロー型のプロファイル宣言
• f^ : Γ→A 項の結果型宣言

パッキング〈レイフィケーション〉の結果は、コンテキスト項目〈フィールド〉になれるので、コンテキスト拡張に使える。

用語法：

• (結果＝戻り値)＠型宇宙、(結果＝結論)＠命題宇宙

注意：

カリー／ハワード／ランベック対応を使うときは、形容詞に「圏論的」「型理論的」「集合論的」「論理的」などを使うほうが安全。例：型理論的アロー型、論理的含意命題、圏論的指数対象。