functional-programming - 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

将扩展为(在每一行，粗体表达式被展开或缩小):

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

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

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

翻译为:

sum := λl. l plus 0

这将扩展为

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