How to apply lambda calculus rules in Racket?

Question

I am trying to test some of the lambda calculus functions that I wrote using Racket but not having much luck with the testcases. For example given a definition

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

I am trying to apply it to 1 2 3, expecting the successor of 2 to be 3 by doing

(((my_succ 1) 2) 3)

logic being that since my_succ is a function that takes one arg and passes it to another function that takes one arg which passes it to the third function that takes one arg. But I get

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

I tried Googling and found a lot of code for the rules, but no examples of application of these rules. How should I call the above successor function in order to test it?

Answer 1

You are mixing two completely different things: lambda terms and functions in Racket.

1. In Racket you can have anonymous functions, that can be written in the λ notation (like (λ(x) (+ x 1)) that returns the successor of an integer, so that ((λ(x) (+ x 1)) 1) returns 2),
2. in Pure Lambda Calculus you have only lambda terms, that are written with in a similar notation, and that can be interpreted as functions.

In the second domain, you do not have natural numbers like 0, 1, 2, ..., but you have only lambda terms, and represent numbers as such. For instance, if you use the so-called Church numerals, you represent (in technical term encode) the number 0 with the lambda term λf.λx.x, 1 with λf.λx.f x, 2 with λf.λx.f (f x) and so on.

So, the function successor (for numbers represented with this encoding) correspond to a term which, in Racket notation, is the function that you have written, but you cannot apply it to numbers like 0, 1, etc., but only to other lambda expressions, that is you could write something like this:

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

(successor zero)

The result in Racket is a procedure (it will be printed as: #<procedure>), but if you try to test that your result is correct, comparing it with the functional encoding of 1, you will find something strange. In fact:

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

produces #f, since if you compare two procedures in Racket you obtain always false (e.g. (equal? (λ(x)x) (λ(x)x)) produces #f), unless you compare the “identical” (in the sense of “same memory cell”) value ((equal? zero zero) gives #t). This is due to the fact that, for comparing correctly two functions, you should compare infinite sets of couples (input, output)!

Another possibility would be representing lambda terms as some kind of structure in Racket, so you can represent Church numerals, as well as "normal" lambda terms, and define a function apply (or better reduce) the perform lambda-reduction.