並行簡約と完全展開

並行簡約 $\Rightarrow$ を次の規則で帰納的に定める。

1. $x\Rightarrow x$。
2. $M\Rightarrow M'$ ならば $\lambda x.M\Rightarrow\lambda x.M'$。
3. $M\Rightarrow M'$、$N\Rightarrow N'$ ならば $MN\Rightarrow M'N'$。
4. $M\Rightarrow M'$、$N\Rightarrow N'$ ならば $(\lambda x.M)N\Rightarrow M'[x:=N']$。

項 $M$ の完全展開 $M^{*}$ を、$x^{*}\equiv x$、$(\lambda x.M)^{*}\equiv\lambda x.M^{*}$、$((\lambda x.M)N)^{*}\equiv M^{*}[x:=N^{*}]$、$M$ が抽象でないとき $(MN)^{*}\equiv M^{*}N^{*}$ で定める。