行き詰まり状態
項が
正規形
であるが値ではない時、その項は「行き詰まり状態」であるという
これが
実行時エラー
に相当する
無意味な状態
例えば色々導出を進めていったら
$ \mathrm{succ}\,\mathrm{false}
にたどり着いちゃった
$ \mathrm{succ}
は引数に自然数しか取らないので、これは明らかにおかしい
操作的意味論
的に、これ以上何の操作もできない、詰み
これを静的に防ぐために
型システム
などを利用する
参考
TaPL
3章