Как проверить пустой список в чистом (нетипизированном) лямбда-исчислении в DrRacket?

Question

Я пытаюсь создать списки в чистом лямбда-исчислении (фактически Двоичные деревья маскируются как списки (в форме [Root, [Left SubTree], [Right SubTree]]), но для целей этого конкретного вопроса мы можем поговорить об общих списках в лямбда-исчислении).

Некоторые основные определения лямбда-исчисления (выраженный в синтаксисе Ракетка), я буду использовать в этом вопросе:

(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, который я определил в Ракетка следующим образом:

(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, как видно ниже фрагменте кода:

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

Который также оценивает в 2 в рэкет.

Может кто-то указать мне на мою ошибку, которая, я надеюсь, является чем-то синтаксическим, что я не могу обнаружить!

PS: На всякий случай я полностью подхожу к этому неправильно, я пытаюсь реализовать двоичное дерево поиска в чистом исчислении лямбда в Racket. Любые указатели на мою конечную цель были бы очень благодарны - я перечислил один из подходов, которые я принял.

(Для некоторого дополнительного чтения о функции, которую я пытаюсь имитировать, см. this).

Answer 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) 

в то время как ваша интерпретация не имеет соответствия в лямбда-исчислении.