Lambda Calculus: build a function that takes more arguments with each iteration

Question

I'm trying to build a function that takes a given number of arguments and always return the same value.

This is a part of an homework. There is a hint provided:

The "k-way T" is a function that takes k arguments and always returns T. A "0-way T" is just T.

Where k is provided as Church Numeral and T is the lambda expression for True (\x.\y.x).

The complete task is to provide an lambda expression that computes an k-way OR function. Where the number of 'boolean' arguments is provided before the 'boolean' arguments. e.g:

((OR 3) F T F)

But for now I'm trying to create that takes k arguments and returns always T. The k is provided as first argument.

((TRUE 2) T F) == T

So basically I wan't to create a function that has one more argument for each church numeral 'iteration'.

But somehow I'm completely stuck.

Can I do that with only an church numeral? Or do I need recursion (Y-Combinator)?

In general: Are there any good tools (e.g for visualization) that support the creation of lambda expressions.

I'm really astonished about the power of the lambda calculus and I really want to learn it. But I don't know how...

Thanks in advance

Anton Trunov Anton Trunov · Accepted Answer · 2016-04-29T06:59:25

I'll show how to implement the TRUE function. Since k is not fixed, you need a fixed-point combinator (Y would do, but it's not the only fixed-point combinator). First of all a couple words about the notation I've used below: iszero (takes a Church numeral, checks if it is Church zero and returns a Church boolean), T (the Church-encoded true boolean value), pred (the predecessor function for Church numerals), and Y (a fixed-point combinator).

let TRUE = Y (λr. λn. (iszero n) T (λx. (r (pred n))))

Notice that let is not part of lambda calculus syntax, it's metasyntax to introduce a name (for us).

This works as follows: Y sort of converts the r argument into "self" -- when a function calls r it calls itself. To illustrate this, I'm going to rewrite the above into recursive form (warning: it's for illustrative purposes only, lambda calculus does not allow this; since all the functions are anonymous you can't call them using their names -- there is just no way for this):

let TRUE = λn. (iszero n) T (λx. (TRUE (pred n)))

I've stripped off the λr. part and replaced r by TRUE (again, please do not do this in your homework, it is not valid lambda calculus).

And this definition is easier to understand: if TRUE is called like this TRUE 0 it just returns T, otherwise it returns a function of one argument which wraps around a function of (n - 1) arguments, essentially representing a function of n arguments.

As for your question on tools: one way would be to use Scheme/Racket -- it would help checking your "lambda calculus code" runs as it should. For example, here is an implementation of TRUE in Racket:

(define (Y f)
  ((lambda (x) (x x))
   (lambda (x) (lambda (a) ((f (x x)) a)))))

(define TRUE
  (Y (lambda (r)
       (lambda (n)
         (if (zero? n)
             #t
             (lambda (x) (r (sub1 n))))))))

;; tests
> (TRUE 0)
#t
> ((TRUE 1) #f)
#t
> (((TRUE 2) #f) #f)
#t
> ((((((TRUE 5) #f) #f) #f) #f) #f)
#t

I ought to add that I used here built-in booleans, integers, if-expression, sub1, zero? instead of Church-encoded ones. Otherwise it would make this example much bigger (or incomplete).

Lambda Calculus: build a function that takes more arguments with each iteration

2 Answers