Как реализовать «EQ» LISP в исчислении лямбда?

Question

Я изучаю лямбда-исчисление в эти дни и нашел это очень красивым и интересным, но я не узнал, как реализовать примитив EQ LISP, который судит, совпадают ли два символа.

Я нашел много материалов для реализации целочисленной арифметики (используя церковные номера) и логической логики, но не смог найти решение для EQ. Я надеюсь, что EQ как это работает (то же из LISP):

(EQ x x) --> True 
(EQ x y) --> False 
(EQ (x y) (x y)) --> False // return true only for simple symbols, not structures 

Любая помощь.

---

Update:

Я не против того, чтобы обернуть символы в некоторых контекстах, например:

(EQ (lambda u . u symbol x) (lambda u . u symbol x)) --> True 
(EQ (lambda u . u symbol x) (lambda u . u symbol y)) --> False 

---

Я нашел возможное решение:

Если мы икт символы в конечном множестве, например, Symbols = {A, B, C}, то мы можем определить EQ так:

A = λ A B C. A 
B = λ A B C. B 
C = λ A B C. C 
EQ = λ x y. ChurchEQ (x 1 2 3) (y 1 2 3) // Here 1, 2, 3 should be replaced by Church Numbers 

Я проверил эту коду в качестве переводчика, и он работает.

Но остается одна проблема: Сам EQ не может быть размещен в Symbols.

Answer 1

Невозможно определить общий понятие равенства для произвольных членов в исчислении лямбда. В зависимости от реализации EQ либо определяется как синтаксическое равенство (возможно, до α-эквивалентности), либо равенство указателя, которое должно быть определено в реализации вашего интерпретатора, а не в самом языке.

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

T = λ x y. x 
F = λ x y. y 
not = λ p. p F T 
xor = λ p q. p (q F T) q 
equ = λ p q. not (xor p q)