How to write the equals predicate in Racket (or Scheme) using just lambda expressions

Question

I can see how to write cons, cdr, car and other expressions in Racket using only lambda expressions (from SICP):

(define (cons x y)
  (lambda (m) (m x y)))

(define (car z)
  (z (lambda (p q) p)))

(define (cdr z)
  (z (lambda (p q) q)))

Is there a way to write the equals predicate the same way?

I want to be able to compare defined expressions, which include numbers, but also compare arbitrary expressions which are not numbers.

I guess I am interested in developing mathematics from a minimal set of symbols. From what I can understand, it will not be the same as developing math from Set Theory because the basics of Set Theory use the "is an element of" symbol and the null set symbol as its only non-logical symbols. If I understand correctly, the Lambda Calculus uses the "function" symbol (lambda) as its only necessary non-logical symbol. But, everything can be built from there. Is this correct?

Answer 1

Equivalence without equivalence functions or operators can use pattern matching and mapping. This is a sample and the regular expression matching emits #t when the first part of strings match. "co" matches "cool" but not the reverse. The matches here are only string and number. Lists could easily be added. I think there might be a lambda/match function that will work like a regular lambda function that also does matching.

(define/match (equ? a b)
  [( (? number? a) (? number? b) )
     (case (- a b) [(0) #t] [else #f])]
  [( (? string? a) (? string? b) ) 
     (if (regexp-match? (regexp-quote a) b) #t #f)])

Answer 2

Equality of numbers can be done. I found this blog that had this and more:

(define (zero  f) (λ (x) x))
(define (succ  n) (λ (f) (λ (x) (f ((n f) x)))))
(define one   (succ zero))
(define two   (succ one)) ; continue to define all numbers
(define (add a b) ((b succ) a))

;; here we use you definition of cons, car, cdr
(define (pred n) 
  (cdr ((n (λ (p) 
             (cons (succ (car p)) (car p)))) 
        (cons zero zero))))

(define (if c a b) (c a b))
(define (true a b) a)
(define (false a b) b)
(define (zero? n) ((n (λ (x) false)) true))
(define (sub a b) ((b pred) a))
(define (mult a b) ((a (λ (x) (add x b))) zero))

;; here is numeric compare
(define (= a b) (zero? (sub a b)))

(print-boolean (= (add two two) (mult two two))) ; ==> true    
(print (add two two)) ; ==> 4

These are the print functions. These only gives you a more natural look for the values that really are just fine the way they are when passed to these, but just a little cryptic.

(define (print n) ((n (λ (n) (+ n 1))) 0))
(define (print-boolean n) (n 'true 'false))

Answer 3

I don't think that this can be done, in general -- in particular, because the function needs to deal with the type of both of its parameters, which can't be done with just a lambda.

Really, the answer is "it depends." Here, SCIP is implementing the lambda calculus in Racket. Lambda calculus lists are different beasts than Racket lists -- they're closures, rather than a datatype. cons, car and cdr, as defined here, are not compatible with the vanilla Racket language. If you want to use the lambda calculus, you're forced to implement all of it in your language. In particular, you need to build Church numerals to put inside your lists and then define equality on them by following your favorite CS textbook. `

You can't get the generalized equal? predicate, because this deals with much higher level constructs. Even if we restrict ourselves, equality soon becomes undecidable.

Answer 4

cons, car, and cdr are a close-knit set of functions, very much isolated from the rest of the language; you can implement them however you want with no real impact on anything else.

But = is a much more far-reaching function, whose implementation depends on the implementation of everything else in the language: you can't just rewrite it in isolation. Lambda calculus is Turing complete, so of course it is possible to implement = with just lambdas, but you have to structure the entirety of the language around it.

One example implementation would involve requiring that each scheme-level value (assuming here that we're implementing scheme in terms of lambdas) is represented at the interpreter level as a cons, whose car is a number representing its type and whose cdr is a value of some sort. Then = could compare the types, and make some comparison of the values if the types match.

But now you have to dive into how you even represent numbers: okay, fine, Church numerals. And how do you compare those for equality, in order to implement =? All of this is possible, but it's a much more involved problem than reimplementing cons, car, and cdr.