余帰納的定義

ちなみに最近のXavier Leroy（OCamlの作者）の余帰納的定義による操作的意味論はさらによさげ。まだほとんど読んでませんが、99%推測でいうと「small-step semanticsより簡潔だが、無限ループとエラーを区別できなかった」（区別するのが面倒だった）big-step semanticsにおいて、無限ループとエラーを区別できるようになった、のではないかと思います。99%想像ですが。

追記：と思ったら嘘だった。「\vdash e : \tauならば、あるvが存在してe \Downarrow v」（ただし\Downarrowは普通の評価規則を余帰納的に解釈）が成り立つのかと思ったら成り立たないらしい。Filinskiが一瞬で反例をあげたらしい。Boehm木とか考えれば当たり前なのかもしれないが、恐るべし。