如何在 DrRacket 中的纯（无类型）lambda 演算中检查空列表？答案

【问题标题】：How to check for empty list in pure (untyped) lambda calculus in DrRacket?如何在 DrRacket 中的纯（无类型）lambda 演算中检查空列表？
【发布时间】：2017-04-30 08:21:51
【问题描述】：

我正在尝试在纯 lambda 演算中构建列表（实际上是伪装成列表的二叉树（以 [Root, [Left SubTree], [Right SubTree]] 的形式），但出于这个特定问题的目的，我们可以讨论 lambda 演算中的一般列表） .

我将在这个问题中使用 lambda 演算的一些基本定义（以 Racket 语法表示）：

(define true (lambda (x) (lambda (y) x)))
(define false (lambda (x) (lambda (y) y)))
(define if (lambda (x) (lambda (y) (lambda (z) ((x y) z)))))

; I'm using Parigot Encodings to represent numbers
(define zero (lambda (s) (lambda (z) z)))
(define one (lambda (s) (lambda (z) ((s zero) z))))
(define two (lambda (s) (lambda (z) ((s one) ((s zero) z)))))

; Here are some converter functions for debugging/printing
(define (p->int n)
   ((n (lambda(x) add1)) 0))

(define (int->p i)
   (if (zero? i)
       (lambda (f) (lambda (x) x))
       (let ((m (int->p (- i 1))))
         (lambda (f) (lambda (x) ((m f) ((f m) x)))) )))

; Building blocks for Lists. A list consists of a single element Head,
; followed by the rest of the list (Tail). Lists are thus recursively
; defined. An empty list consists of only the element 'nil'
(define mkpair (lambda (a) (lambda (b) (lambda (c) ((c a) b)))))   
(define Head (lambda (p) (p true)))
(define Tail (lambda (p) (p false)))
(define nil false)

为了对此类列表进行操作，我需要检测列表何时为空（例如，在表示为列表的二叉搜索树上进行二叉搜索时检测叶节点）。以下link 将该函数作为isempty = λl.l(λab.false)true 提供，我在 Racket 中定义如下：

(define Null? (lambda (p) (p (lambda (x) (lambda (y) false)))true))

这似乎可行，如下所示：

(p->int (((if (Null? (Head ((mkpair nil) one)))) two) one))

换句话说，上面的应用程序检查列表的头部 [nil, one] 是否为空列表（仅包含 nil），如果是，则计算结果为 two，当将其馈送到转换器函数 p->int ，产生2。一切都很好，除了 Null? 函数似乎没有评估为 false，如下面的 sn-p 所示：

(p->int (((if (Null? (Tail ((mkpair nil) one)))) two) one))

在 Racket 中也计算为 2。

有人能指出我的错误吗，我希望这是我无法检测到的语法错误！

PS：以防万一我完全走错了路，我正在尝试在 Racket 中用纯 lambda 演算实现二叉搜索树。任何指向我的最终目标的指针都将不胜感激 - 我已经列出了我采用的一种方法。

（有关我尝试模拟的功能的更多信息，请参阅this）。

【问题讨论】：

标签： list functional-programming racket lambda-calculus

【解决方案1】：

问题实际上是isempty 函数的错误转置。你应该写：

(define Null? (lambda (p) ((p (lambda (x) (lambda (y) false))) true)))

代替：

(define Null? (lambda (p) (p (lambda (x) (lambda (y) false))) true))

因为λl.l(λab.false)true应该被解释为：

λl. ((l (λab.false)) true)

而您的解释在 lambda 演算中没有对应关系。

【讨论】：