lambda 演算中的加法证明

Question

不明白add(m, n) = m + n证明中的这个转变：(λmn.λsz.m, s, (n, s, z)) = (λs.λz.sm(z) ) , s, (λs.λz.sn(z))

解释转换的逻辑（可能是 b 约简或某些定义的使用，例如 n = λs.λz.s^n(z) ）。

Answer 1

好的，我找到了解释。

[在此处输入图像描述][1] [1]：https://i.sstatic.net/nuV6J36P.png

add(m, n) = (λm.λn.λf.λx.m(f)(n(f)(x)))(m)(n) = λf.λx.m(f)(n(f) )(x)) = λf.λx.f^m(f^n(x)) = λf.λx.f^(m+n)(x) = m + n