簡約と型付けについて私が知っている二、三の事柄（試験投稿）

$\lambda$計算では、$\beta$簡約（以下、「簡約」）という仕組みにより計算を表現する。
$M{\to }_{\beta }N$という簡約があり、$M$が$\tau$という型により正しく型付けられているなら、簡約結果である$N$も同じ$\tau$によって型付けられている。これを主部簡約定理 subject reduction theorem という。
この定理の証明には以下の補題が有用である。

型付けの代入補題

$\lambda$項$M$が$\gamma$により型付けられていてかつ$M$内に$x$が自由出現しているとする。さらに、$N$が$\delta$により型づけられているとする。このとき、$\lambda$項$M[N\leftarrow x]$は型$\gamma$により型づけられている。

正規化可能性

型のない$\lambda$計算では、$xx$のように$\beta$正規形（以下、「正規形」）を持たない$\lambda$項が存在した。
しかし、型付$\lambda$計算では、強正規化定理 strong normalizability という性質が成り立つ。

弱正規化可能性

正しく型のついた$\lambda$項$M$に対して正規形$M_n$に至る簡約列
$$M{\to }_{\beta }{M}_1{\to }_{\beta }{M}_2{\to }_{\beta }\cdots {\to }_{\beta }{M}_n$$
が存在するとき、$M$は弱正規化可能であるという。

この性質が述べるところは、適切な簡約戦略の採用により正規形に到達できるが、不適切な採用では正規形に到達できない場合もあるということである。

強正規化可能性

正しく型のついた$\lambda$項$M$に対して、$M$から始まる無限簡約列
$$M{\to }_{\beta }{M}_1{\to }_{\beta }{M}_2{\to }_{\beta }\dots$$
が存在しないとき、$M$は強正規化可能であるという。

単純型付$\lambda$計算は強正規化可能性を持つことが知られており、強正規化可能であれば弱正規化可能であることが知られている。