β簡約
β-conversion
仮引数を実引数に置き換える操作
複数回のβ簡約は$ \xrightarrow{\ast}_\betaとか$ \twoheadrightarrowとかと表記される
文献によって異なる
前者を使っていこうかなmrsekut.icon
簡約基$ (\lambda x.t_{12})(t_2)を以下のように書き換える操作のこと
$ (\lambda x.t_{12})t_2 \to [x \mapsto t_2]t_{12} .
このとき$ (\lambda x.t_{12})t_2 のことをβ基という $ (\lambda x.N)Mの形のもの
単純に、$ t_{12}の中の束縛変数$ xに$ t_2を適用したもの
代入の厳密な定義
ref TaPL.icon p.54
「β簡約」という言葉は使われていないが多分同じ意味