計算では、簡約(以下、「簡約」)という仕組みにより計算を表現する。
という簡約があり、がという型により正しく型付けられているなら、簡約結果であるも同じによって型付けられている。これを主部簡約定理 subject reduction theorem という。
この定理の証明には以下の補題が有用である。
型付けの代入補題
項がにより型付けられていてかつ内にが自由出現しているとする。さらに、がにより型づけられているとする。このとき、項は型により型づけられている。
正規化可能性
型のない計算では、のように正規形(以下、「正規形」)を持たない項が存在した。
しかし、型付計算では、強正規化定理 strong normalizability という性質が成り立つ。
弱正規化可能性
正しく型のついた項に対して正規形に至る簡約列
が存在するとき、は弱正規化可能であるという。
この性質が述べるところは、適切な簡約戦略の採用により正規形に到達できるが、不適切な採用では正規形に到達できない場合もあるということである。
強正規化可能性
正しく型のついた項に対して、から始まる無限簡約列
が存在しないとき、は強正規化可能であるという。
単純型付計算は強正規化可能性を持つことが知られており、強正規化可能であれば弱正規化可能であることが知られている。