在λ演算中,(λ x. λ y. λ s. λ z. x s (y s z)) 用于将两个 Church 数加起来。如何解释这个过程?是否有关于函数式编程的λ演算的好资源?非常感谢您的帮助。
实际上λ f1. λ f2. λ s. λ z. (f1 s (f2 s z)) 计算加法,因为它有效地将(f2 s z)即f2代表的数字替换到(f1 s z)中的“零”的位置。
例如:我们取f2为二进制的ssz。f1是一:s z。将最后一个z
替换为f2,您会得到sss z,即三的扩展形式。
这需要黑板和手势讲解,抱歉。
true = \a,b.a false = \a,b.b
n = \f,x.f(f(....(f x)...))
有 f 函数的 n 次出现。
现在,如果您想从 x 开始迭代函数 f n + m 次,则必须先迭代 n 次,即 (n f x),然后从前一个结果开始迭代 m 次,即
m f (n f x)
m (n f) x
以构造函数和相应的消除器(所谓的Bohm-Berarducci编码)更正式地解释了数据类型的先前编码。