β変換ともいう

仮引数を実引数に置き換える操作

簡約過程を列にしたものがβ変換列

複数回のβ簡約は\xrightarrow{\ast}_\betaとか\twoheadrightarrowとかと表記される

文献によって異なる

前者を使っていこうかな

簡約基(\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 p.54

「β簡約」という言葉は使われていないが多分同じ意味

β簡約の評価戦略の種類