“Lambda-Calculus and Combinators: An Introduction”メモ(その4)
Excercise A1.3
$S$ は β-redex であり、あらかじめ β-reduction をしておくもの。
$\begin{array} &
P^\prime & ≡ & (λx.S)v, \mbox{ where } S ≡ (λyv.uvy)x \\
S & ≡ & (λy.(λv.uvy))x \\
& \rhd_{1\beta} & [x/y]λv.uvy \\
& ≡ & λv.uvx \\
P & ≡ & (λx.(λv.uvx))v \\
& \rhd_{1\beta} & [v/x](λv.uvx) \\
& ≡ & λy.[v/x][y/v]uvx \\
& ≡ & λy.[v/x]uyx \\
& ≡ & λy.uyv \\
\end{array}$
$S$ をそのまま $P^\prime$ へ代入するもの。
$\begin{array} &
P^\prime & ≡ & (λx.(λyv.uvy)x)v \\
& \rhd_{1\beta} & [v/x](λyv.uvy)x \\
& ≡ & (λyv.uvy)v \\
& ≡ & (λy.(λv.uvy))v \\
& \rhd_{1\beta} & [v/y](λv.uvy) \\
& ≡ & λx.[v/y][x/v]uvy \\
& ≡ & λx.[v/y]uxy \\
& ≡ & λx.uxv \\
\end{array}$