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))
跟你一样总和。所以现在我有非递归版本。但是我不能在这里使用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