通过显示所有 Beta 减少来表明术语“cons”有效

问题描述

我是函数式编程的新手。

因此术语 cons 将一个元素附加到列表的前面。哪里

cons ≜ λx:λl:λc:λn: c x (l c n)

对于示例函数调用，我应该如何证明 cons 使用 Beta 减少正确工作？例如将 cons 3 [2,1] 减少到 [3,2,1]？

是否有类似 lambda 演算中算术运算的公式？与算术运算（即加法或乘法）相比，我对如何处理这个问题有点困惑。

谢谢。

解决方法

cons ≜ λx:λl:λc:λn: c x (l c n) 表示

cons x l c n =
   c x (l c n)

（在功能/应用/组合符号中）。所以

cons 3 [2,1] c n = 
 = c 3 ([2,1] c n)

如果不只是 [2,1] 的快捷表示法，那么 cons 2 [1] 是什么，以便我们继续

 = c 3 (cons 2 [1] c n)
 = c 3 (c    2 ([1] c n))
 = c 3 (c    2 (cons 1 [] c n))
 = c 3 (c    2 (c    1 ([] c n)))

所以没有从 cons 3 [2,1] 减少到 [3,2,1]； [3,1] 是 cons 3 [2,1]。 [2,1] 是 cons 2 [1]，[1] 是 cons 1 []。

列表 cons x xs，当提供 c 和 n 参数时，将变成 c x (xs c n)，{{1} }， 轮到时;所以任何列表的元素都在 xs 的应用链中相互重叠使用。

c 应该变成什么？它没有任何内容可以通过 [] c n 应用程序——这些应用程序将应用于列表的元素，而 c 没有。所以唯一合理的做法（我相信你已经给出了这个定义）是把 [] 变成只是 [] c n：

n

无论 cons 3 [2,1] c n = = c 3 (c 2 (c 1 ([] c n))) = c 3 (c 2 (c 1 n )) 和 c 是什么。

就是这样。