数学 › 数理論理学と型理論 › 単純型付きラムダ計算とカリー＝ハワード対応

還元可能性の 3 条件

補題 3.3（「単純型付きラムダ計算とカリー＝ハワード対応」§3）・ ✓公理まで証明済み

すべての型 $A$ について次が成り立つ。

(CR1) $M\in\mathrm{Red}_A$ ならば $M$ は SN。
(CR2) $M\in\mathrm{Red}_A$ かつ $M\to_\beta M'$ ならば $M'\in\mathrm{Red}_A$ 。
(CR3) $M$ が中立で、 $M$ の 1 ステップ簡約先がすべて $\mathrm{Red}_A$ に属するならば、 $M\in\mathrm{Red}_A$ 。

とくに (CR3) から、変数はすべての $\mathrm{Red}_A$ に属する（変数は中立で、簡約先をもたない）。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

前提をたどる証明が使う定理・定義

証明は Rikai の他の定理を参照していません（定義と論理だけで示されています）。

これを使っている定理証明で参照している 1 件

強正規化定理✓定理 3.1・単純型付きラムダ計算とカリー＝ハワード対応

関連するノック 2 問