教堂数字的取幂定义为：
expt ≡ λmnsz.nmsz
但是在幂不是 0 或 1 的情况下，我无法评估它。考虑这个例子：
expt C3 C2 ≡ [λmnsz.nmsz](λsz.s^3 z) (λsz.s^2 z)
在哪里
λsz.s^2 z = λsz.s(sz)
和Cn 代表教会数字n
代入 m 和 n，我得到：
λsz. (λsz.s^2 z)(λsz. s^3 z)sz
λsz. (λsz.s^2 z)(s^3 z)
λsz. (s^3)^2 z
事实上，
λsz. (s^m)^n z = s^(m*n) z
最后一条语句简化为
C6 ≡ λsz. s^6 z
但expt C3 C2 应该评估为 C9。
那么我哪里做错了？
【问题讨论】：
标签： lambda-calculus
这是错误的：
λsz. (λsz.s^2 z)(λsz. s^3 z)sz
λsz. (λsz.s^2 z)(s^3 z)
λsz. (s^3)^2 z
您不能将 (λsz.s^3 z) 应用于 sz。您必须将 (λsz.s^2 z) 应用于 (λsz.s^3 z)，因为评估是从左到右的。
λsz. (λsz.s^2 z) (λsz. s^3 z) sz
λsz. (λz.(λsz. s^3 z)^2 z) sz
λsz. (λz.(λsz. s^3 z)((λsz. s^3 z) z)) sz
λsz. (λz.(λsx. s^3 x)((λsy. s^3 y) z)) sz
λsz. (λz.(λsx. s^3 x) (λy. z^3 y)) sz
λsz. (λz.(λx. (λy. z^3 y)^3 x)) sz
λsz. (λz.(λx. (λy. z^3 y)((λy. z^3 y) ((λy. z^3 y) x)))) sz
λsz. (λz.(λx. (λy. z^3 y)((λy. z^3 y) (z^3 x)))) sz
λsz. (λz.(λx. (λy. z^3 y)(z^3 (z^3 x)))) sz
λsz. (λz.(λx. (λy. z^3 y)(z^6 x))) sz
λsz. (λz.(λx. (z^3 (z^6 x)))) sz
λsz. (λz.(λx. (z^9 x))) sz
λsz. (λx. (s^9 x)) z
λsz. (s^9 z)
【讨论】：