単純型付きλ計算における値呼び簡約の停止性
次の定理
大雑把には次の順番で証明にたどり着く
β簡約の種類として値呼び簡約がある（call-by-value reduction） 値呼び簡約が停止するとは無限簡約列が存在しないことを指す．
$ M \to_{cbv} M_1 \to_{cbv} \cdots は存在しない．
これらは$ \to_\betaについて示したが値呼び簡約$ \to_{cbv}でも成り立つ．
Def 1.
λ項についての型$ Aの単項述語$ Rを次のように定める
基底型$ \alphaの$ R_\alpha(M)$ \iff$ \vdash M:\alphaかつ$ Aは停止する
型$ A \to Bの$ R_{A \to B}(M)$ \iff
$ \vdash M : A \to B
$ Mは停止する
任意の$ R_{A}(N)を満たす$ Nについて$ R_B(M N)
Lem 2.
$ M \to_{cbv} M'なら，$ R_{A}(M) \iff R_A(M')
Lem 3.
型$ Aに型付けされた変数$ x
$ n \geq 0
$ R_{A_i}(N^{A_i})を満たすλ項$ M^{A_i}, 1 \leq i \leq n
このとき，
$ R_a(x^{A_1 \to \cdots A_n \to A} M_{0} \dots M_{n})
特に，$ n = 0なら$ xは単に$ R_A(x)
Lem 4.
型$ Aに型付けされたλ項$ M
$ n \geq 0
任意変数$ {x_i}^{A_i}, 1 \leq i \leq n
$ R_{A_i}(N^{A_i})を満たすλ項$ N^{A_i}, 1 \leq i \leq n
このとき，
$ R_A (M \lbrack x_1 := N_1, \cdots , x_n := N_n \rbrack )
特に，$ n=0なら$ Mは単に$ R_A(M)
Thm 3. 値呼び簡約の停止性
λ項が正しく型付けされるなら，値呼び簡約は停止する
proof:
1. λ項$ Mが型$ Aで型付けされるとする
2. Lem 4. より$ R_A(M)が成り立つ
3. Def 1. より$ Mは停止する