Lambda-Calculus and Combinators: An Introduction
Hindley & Seldin より
形式$(\lambda x.M)N$は、演算子$(\lambda x.M)$に引数$N$が適用されること表している。
$(\lambda x.M)N$は、計算され、$M$内の$x$を$N$に置き換えられ、$[N/x]M$へと簡単化することができる。
定義1.24（βコントラクト、β簡約）
$$(\lambda x.M)N$$の形式はリデックス(redex)とよばれ、それに対応する項$$[N/x]M$$は、コントラクタム(contractum)と呼ばれる。
項$P$が$(\lambda x.M)N$の形式を含んでおり、$[N/x]M$によって置き換えられ、その結果が$P'$となる場合、$P$が$P'$にβコントラクトしたと言われ、$$P\quad \triangleright_{1\beta}\quad P'$$と書かれる。
$P$が有限（あるいは零）回のβコントラクトされ、束縛変数が変更され、項$Q$に変更された場合は、$P$は$Q$へβ簡約したと呼ばれ、$$P\quad \triangleright_\beta\quad Q$$と書かれる。
例1.25
(a) $(\lambda x.x(xy))N\quad\triangleright_{1\beta}\quad N(Ny)$
(b) $(\lambda x.y)N\quad\triangleright_{1\beta}\quad y$
(c) $(\lambda x.(\lambda y.yx)z)v
\quad\triangleright_{1\beta}\quad[v/x]((\lambda y.yx)z)
\quad\equiv\quad((\lambda y.yv)z)$
$\quad\triangleright_{1\beta}\quad [z/y](yv)
\quad\equiv\quad yz$
(d) $(\lambda x.xx)(\lambda x.xx)
\quad\triangleright_{1\beta}\quad[(\lambda x.xx)/x](xx)
\quad\equiv\quad(\lambda x.xx)(\lambda x.xx)$
$\quad\triangleright_{1\beta}\quad[(\lambda x.xx)/x](xx)
\quad\equiv\quad(\lambda x.xx)(\lambda x.xx)$
$\quad\cdots\quad$等
(e) $(\lambda x.xxy)(\lambda x.xxy)
\quad\triangleright_{1\beta}\quad[(\lambda x.xxy)/x](xx)
\quad\equiv\quad(\lambda x.xxy)(\lambda x.xxy)y$
$\quad\triangleright_{1\beta}\quad[(\lambda x.xxy)/x](xxy)y
\quad\equiv\quad(\lambda x.xxy)(\lambda x.xxy)yy$
$\quad\cdots\quad$等
例1.25(d)のように、簡単化プロセスは常に簡単化するわけでない。
更に悪い場合は、(e)の場合、更に複雑になっていくことがある。
これらの例が示すように、簡単化プロセスは常に終了するわけでなく、リデックスを含まない項に到達した時に終了する。
定義1.26
βリデックスを含まない項$Q$はβ標準形と呼ばれる。
項$P$がβ標準形の項$Q$にβ簡約すれば、項$Q$は$P$のβ標準形と呼ばれる。
例1.27
(a) 1/25(c)において、$zv$は$(\lambda x.(\lambda y.yx)z)v$のβ標準形である。
(b) $L\equiv(\lambda x.xxy)(\lambda x.xxy)$と置くと、1.25(e)によって、
$L\ \triangleright_{1\beta}\ Ly
\ \triangleright_{1\beta}\ Lyy
\ \triangleright_{1\beta}\ \cdots$
この列は無限に続くので、$L$はβ簡約され得ず、$L$はβ標準形を持たない。
(c) 上記の$L$を使って、$P\equiv(\lambda u.v)L$とおく。すると、$P$は（少なくと）2つの異なるやり方で簡約することができる。
(i) $P\ \equiv\ (\lambda u.v)L
\ \triangleright_{1\beta}\ [L/u]v\ \equiv\ v$
(ii) $P\ \triangleright_{1\beta}\ (\lambda u.v)(Ly)$
$\quad\triangleright_{1\beta}\ (\lambda u.v)(Lyy)$
$\quad\cdots$等
そのため$P$は標準形$v$を持つが、無限の簡約も持っている。
(d) 例1.25(d)の項$(\lambda x.xx)(\lambda x.xx)$は、普通$\Omega$と呼ばれる。標準形を持たず。実際、常に自分自身に簡約されるので、標準形に簡約されることはない。しかし、$\Omega$は、どんな異なる項にも簡約され得ないのという意味で「最小」である。
練習問題1.28
次の項をβ標準形に簡約せよ。
(a) $(\lambda x.xy)(\lambda u.vuu)
\ \triangleright_{1\beta}\ (\lambda u.vuu)y
\ \triangleright_{1\beta}\ vyy$
(b) $(\lambda xy.yx)uv
\ \triangleright_{1\beta}\ vu$
(c) $\lambda x.x(x(yz))x)(\lambda u.uv)$
$\quad\triangleright_{1\beta}\quad (\lambda u.uv)((\lambda u.uv)(yz))(\lambda u.uv)$
$\quad\triangleright_{1\beta}\quad(\lambda u.uv)(yzv)(\lambda u.uv)$
$\quad\triangleright_{1\beta}\quad(yzv)v(\lambda u.uv)$
$\quad\triangleright_{1\beta}\quad yzvv(\lambda u.uv)$
(d) $(\lambda x.xxy)(\lambda y.yz)$
$\quad\triangleright_{1\beta}\quad(\lambda y.yz)(\lambda y.yz)y$
$\quad\triangleright_{1\beta}\quad(\lambda y.yz)zy$
$\quad\triangleright_{1\beta}\quad zzy$
(e) $(\lambda xy.xxy)(\lambda u.uyx)$
$\quad\equiv_\alpha\quad(\lambda vw.vww)(\lambda u.uyx)$ 第2項の$y,x$が自由変数なので、α変換した
$\quad\triangleright_{1\beta}\quad\lambda w.(\lambda u.uyx)ww$
$\quad\triangleright_{1\beta}\quad\lambda w.(wyx)w$
$\quad\equiv\quad\lambda w.wyxw$
(f) $(\lambda xyz.xz(yz))
(\underline{(\lambda xy.yx)u})
(\underline{(\lambda xy.yx)v})w$
$\quad\triangleright_\beta\quad(\lambda xyz.xz(yz))(\lambda y.yu)(\lambda y.yv)w$ ２つのコントラクトによって
$\quad\triangleright_\beta\quad
\underline{(\lambda y.yu)w}
(\underline{(\lambda y.yv)w})$ ３つのコントラクトによって
$\quad\triangleright_\beta\quad wu(wv)$ 2つのコントラクトによって