$\begin{array} & \mbox{(a) } xyz(yx) \\ ≡ \Big(((xy)z)(yx)\Big) \\ \\ \mbox{(b) } λx.uxy \\ ≡ \Big(λx.((ux)y)\Big) \\ \\ \mbox{(c) } λu.u(λx.y) \\ ≡ \Big(λu.(u(λx.y))\Big) \\ \\ \mbox{(d) } (λu.vuu)zy \\ ≡ \Big(\Big((λu.((vu)u))z\Big)y\Big) \\ \\ \mbox{(e) } ux(yz)(λv.vy) \\ ≡ \Big(((ux)(yz))(λv.(vy))\Big) \\ \\ \mbox{(f) } (λxyz.xz(yz))uvw \\ ≡ \Big(\Big(\Big(\Big(λx.(λy.(λz.((xz)(yz))))\Big)u\Big)v\Big)w\Big) \\ \\ \end{array}$

$\begin{array} & \mbox{(a) 以下の λ-termの xy に下線を付ける} \\ λxy.xy \\ ≡ (λx.(λy.(\underline{xy}))) \\ \\ \mbox{(b) uv に下線を付ける} \\ x(uv)(λu.v(uv))uv \\ ≡ ((((x(\underline{uv}))(λu.(v(\underline{uv}))))u)v) \\ \\ \mbox{(c) 以下の λ-term に λu.u が存在するかどうか} \\ λu.u \\ ≡ (λu.u), \\ λu.uv \\ ≡ (λu.(uv)) \mbox{これには λu.u は存在しない} \end{array}$

$\begin{array} & \mbox{(a) } [(uv)/x](λy.x(λw.vwx)) \\ ≡ λy.(uv)(λw.vw(uv)) \\ \\ \mbox{(b) } [(λy.xy)/x](λy.x(λx.x)) \\ ≡ λy.(λy.xy)(λx.x) \\ \\ \mbox{(c) } [(λy.vy)/x](y(λv.xv)) \\ ≡ y[(λy.vy)/x](λv.xv) \\ ≡ y(λz.[(λy.vy)/x][z/v]xv) \\ ≡ y(λz.(λy.vy)z) \\ ;; \mbox{解答では、 z ≠ x,y,v。ただ、Definition 1.12 から} \\ ;; z \notin FV((λy.vy)(xv)) \mbox{ を満たすもので良いので } z \notin \{x, v\}\\ \\ \mbox{(c)別解 } [(λy.vy)/x](y(λv.xv)) \\ ≡ y[(λy.vy)/x](λv.xv) \\ ≡ y(λy.[(λy.vy)/x][y/v]xv) \\ ≡ y(λy.(λy.vy)y) \\ ;; \mbox{z の替わりに y と置いた場合でも満たしているのがわかる} \\ \\ \mbox{(d) } [(uv)/x](λx.zy) \\ ≡ λx.zy \\ \end{array}$