λ計算では自然数やデータ型をも表現できるが，プログラムが常に意味のある結果になるとは限らない(行き詰まり状態．例えば true + 1 とは？)．式を実際に評価することなしに，プログラムの振る舞いをできる限り保証したいというのは自然な動機である． 項の…