How to implement `EQ` of LISP in lambda calculus?

Question

I'm learning lambda calculus these days and found it very beautiful and interesting, but I haven't found out how to implement the EQ primitive of LISP, which judges if two symbols are the same.

I have found many materials for implementing integer arithmetic (using Church Numbers) and boolean logic, but failed to find a solution for EQ. I hope EQ works like this(the same of LISP):

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

Any help.

---

Update:

I do not mind to wrap symbols into some contexts, for example:

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

---

I've found a possible solution:

If we restrict symbols in a finite set, e.g., Symbols = {A, B, C}, then we can define an EQ like this:

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

I have tested these code in an interpreter, and it works.

But one problem remains: The EQ itself can't be placed into Symbols.

Answer 1

There is no way to define a general notion of equality for arbitrary terms in the lambda calculus. Depending on the implementation EQ is either defined as syntactic equality (perhaps up to α-equivalence) or pointer equality which have to be defined in the implementation of your interpreter and not in the language itself.

That said, there are many cases of specific lambda expressions ( i.e. church numerals, church booleans ) where there is a well-defined decision procedure for determining equality which of course be encoded in the lambda calculus, just like it can be encoded in any language. For example for booleans:

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)