Как применять правила исчисления лямбда в Racket?

Question

Я пытаюсь проверить некоторые функции лямбда-исчисления, которые я написал с помощью Racket, но не очень повезло с тестовыми окнами. Например дано определение

; successor function 
(define my_succ (λ (one) 
       (λ (two) 
        (λ (three) 
        (two ((one two) three)))))) 

Я пытаюсь применить его к 1 2 3, ожидая преемника 2 быть 3, делая

(((my_succ 1) 2) 3) 

логики в том, что, поскольку my_succ это функция, которая принимает один аргумент и передает его другой функции, которая принимает один аргумент, который передает его третьей функции, которая принимает один аргумент. Но я получаю

application: not a procedure; 
expected a procedure that can be applied to arguments 
    given: 1 
    arguments.: 

Я пробовал Google и нашел много кода для правил, но примеров применения этих правил нет. Как я могу вызвать вышеупомянутую функцию-преемник, чтобы проверить его?

Answer 1

Вы смешиваете две совершенно разные вещи: лямбда-термины и функции в Racket.

1. рэкета вы можете иметь анонимные функции, которые могут быть записаны в Й нотации (например (λ(x) (+ x 1)), который возвращает правопреемник целого, так что ((λ(x) (+ x 1)) 1) возвращает 2)
2. в Pure Lambda Calculus у вас есть только термины лямбды , которые записываются в аналогичной записи и могут быть интерпретированы как функции.

Во втором домене, не натуральные числа, как 0, 1, 2, ..., но у вас есть термины только лямбда, и представлять числа в качестве таковых. Например, если вы используете так называемый Church numerals, вы представляете (в техническом плане закодировать) число 0 с термином лямбда λf.λx.x, 1 с λf.λx.f x, 2 с λf.λx.f (f x) и так далее.

Таким образом, функция successor (для чисел, представленной в этой кодировке) соответствует термину, который, в Ракетка нотации, является функцией, которую вы написали, но вы не можете применить его к номерам, как 0, 1 и т.д., но только с другими лямбда-выражений, то есть вы могли бы написать что-то вроде этого:

(define zero (λ(f) (λ (x) x))) ; this correspond to λf.λx.x 

(successor zero) 

в результате в ракетка является процедура (она будет напечатана как: #<procedure>), но если вы пытаетесь проверить, что ваш результат правильно, сравнивая его с функциональным кодированием 1, вы найдете что-то странное. В самом деле:

(equal? (successor zero) (λ(f) (λ(x) (f x)))) 

производит #f, так как если сравнивать две процедуры в Ракетка вы получаете всегда ложно (например, (equal? (λ(x)x) (λ(x)x)) производит #f), если не сравнивать «идентичны» (в смысле «той же ячейке памяти») Значение ((equal? zero zero) дает #t). Это связано с тем, что для правильного сравнения двух функций вы должны сравнивать бесконечные множества пар (вход, выход)!

Другая возможность будет представлять лямбда-термины, как какое-то структуру в рэкете, так что вы можете представить Чёрч, а также «нормальное» условие лямбды, и определить функцию apply (или лучше reduce) преформу лямбды-сокращение ,