lambda演算中列表元素的总和和列表的长度

Question

我正在尝试在 lambda 演算中创建用于计算列表元素总和和列表长度的函数。
列表示例：a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))
sum a 应返回 6，len a 应返回 3。

我写了递归版本：

len = λl.if (empty l) 0 (plus 1 (len (tail l)))
sum = λl.if (empty l) 0 (plus (head l) (sum (tail l)))

if、empty、plus、tail 是其他 lamda 函数。

然后我用定点组合器做了一些技巧：

len = λl.if (empty l) 0 (plus 1 (len (tail l))) 
len = λfl.if (empty l) 0 (plus 1 (f (tail l))) len
len = Y λfl.if (empty l) 0 (plus 1 (f (tail l)))

在哪里Y = λf.(λx.f(x x))(λx.f(x x))
sum 也一样。所以现在我有非递归版本。但我无法在这里使用 beta 缩减获得 beta 范式。
我想知道这些函数是否存在 beta 范式以及它们的样子。

Answer 1

考虑到列表是由它自己的迭代器编码的，这些可以更容易地实现：

a := [1, 2, 3] = λcn.c 1 (c 2 (c 3 n))

表示列表是两个参数的函数：一个用于cons 节点，一个用于nil 构造函数的末尾。

因此，您可以通过以下方式实现length：

• 忽略存储在cons 节点中的值并返回+1
• 将nil 替换为0

翻译成：

length := λl. l (λ_. plus 1) 0

这将扩展为（在每一行，粗体表达式正在展开或缩小）：

length a
(λl. l (λ_. plus 1) 0) a
(λl. l (λ_. plus 1) 0) (λcn.c 1 (c 2 (c 3 n)))
(λcn. c 1 (c 2 (c 3 n))) (λ_. plus 1) 0
(λn. (λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))) 0
(λ_. plus 1) 1 ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))
(plus 1) ((λ_. plus 1) 2 ((λ_. plus 1) 3 0))
(plus 1) ((plus 1) ((λ_. plus 1) 3 0))
(plus 1) ((plus 1) ((plus 1) 0))
(plus 1) ((plus 1) 1)
(plus 1) 2
= 3

同样，您可以通过以下方式实现sum：

• 使用+ 将存储在cons 中的值与评估尾部的结果结合起来
• 将nil 替换为0

翻译成：

sum := λl. l plus 0

这将扩展为

sum a
(λl. l plus 0) a
(λl. l plus 0) (λcn.c 1 (c 2 (c 3 n)))
(λcn. c 1 (c 2 (c 3 n))) plus 0
(λn. plus 1 (plus 2 (plus 3 n))) 0
plus 1 (plus 2 (plus 3 0))
plus 1 (plus 2 3)
plus 1 5
= 6