如何解决通过显示所有 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
是什么。
就是这样。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。