### Friday, April 08, 2005

## Lambda Calculus and OCAML

I've been working my way through Types and Programming Languages (TAPL). Chapter 5 discusses the untyped lambda calculus, which is a theoretical representation of computation that predates computers.

There are a number of lambda calculus tutorials out on the web, including this one (PDF). Basically, lambda calculus lets you define functions like this:

This is a function that takes a single argument x and returns x. A function can only take a single argument, but you can nest functions to handle multiple arguments, like this:

In this case, the outermost function's return value is a function that multiplies its argument by x.So

The thing I find really interesting is that it is very easy to translate basic lambda calculus expressions into OCAML and try them out. For example, I'll start with Church Booleans.

A Church Boolean is a method of defining true and false as functions. Both functions take two arguments (using the nested notation). True returns its first argument, while false returns its second:

This translates very easily into OCAML (I am using an older form of function declaration because it matches more closely with the lambda calculus form):

You can define boolean

Each argument to this function is a boolean function like tru or fls. If a is tru, then it returns its first argument, which is b, otherwise it returns fls. If b is tru, then the result of a and b is tru, otherwise it is fls.

In a similar manner, you can define

In OCAML, these can be defined as:

You can then play around with various expressions like:

Booleans are fun, but it gets much more interesting when you get into numbers. Church numerals are formed by a combination of two functions s and z. The s function is the "successor" function and z is the zero function. The first few church numerals are defined as:

If you think of s as "1+" and z as 0, then C(0) = 0, C(1) = 1+ 0, C(2) = 1+ (1+ 0), etc.

I defined a function p1 as shorthand for adding 1, and created a print_church function to display an integer version of a Church numeral:

In this case, p1 is a partial function, the (+) operator takes two arguments, but since I only supplied 1, p1 actually returns a function that adds 1 to its argument.

Now, since I don't want to manually define each Church numeral, I defined a simple function that generates Church numerals:

If you call

It is also possible to define the addition operation. Since a Church numeral is essentially defined by adding 1 over and over starting from 0, addition can just be defined as adding 1 over and over starting from another number, like this:

That is, instead of the usual z function, let a's z function be the evaluation of b (instead of counting from 0, a is calculated by starting from b). In OCAML, this can be defined as:

If you call

Multiplication can be defined in a similar way. Instead of adding 1 every time, you add b, like this:

In OCAML, this is:

Again, using print_church, you can test the mult function. If you call

You can get a little closer to the lambda calculus notation by using only single arguments in function definitions:

There are a number of lambda calculus tutorials out on the web, including this one (PDF). Basically, lambda calculus lets you define functions like this:

**λx.x**This is a function that takes a single argument x and returns x. A function can only take a single argument, but you can nest functions to handle multiple arguments, like this:

**λx.λy.x*y**In this case, the outermost function's return value is a function that multiplies its argument by x.So

**(λx.λy.x*y) 5 3**becomes**(λy.5*y) 3**which becomes 15. This method of converting multiple arguments into nested functions is called currying.The thing I find really interesting is that it is very easy to translate basic lambda calculus expressions into OCAML and try them out. For example, I'll start with Church Booleans.

A Church Boolean is a method of defining true and false as functions. Both functions take two arguments (using the nested notation). True returns its first argument, while false returns its second:

**true = λt.λf.t**

false = λt.λf.ffalse = λt.λf.f

This translates very easily into OCAML (I am using an older form of function declaration because it matches more closely with the lambda calculus form):

Now, tru and fls are not static values, but functions. This function prints Church booleans as "true" or "false":

let tru = fun t f -> t;;

let fls = fun t f -> f;;

let print_cbool = fun b -> print_string (b "true" "false");;

You can define boolean

**and**in lambda calculus as:**and = λa.λb.a b fls**Each argument to this function is a boolean function like tru or fls. If a is tru, then it returns its first argument, which is b, otherwise it returns fls. If b is tru, then the result of a and b is tru, otherwise it is fls.

In a similar manner, you can define

**or**and**not**as:**or = λa.λb.a tru b**

not = λa.a fls trunot = λa.a fls tru

In OCAML, these can be defined as:

let andx = fun a b -> a b tru;;

let orx = fun a b -> a tru b;;

let notx = fun a -> a fls tru;;

You can then play around with various expressions like:

print_cbool (andx tru tru);;

print_cbool (andx tru fls);;

print_cbool (andx (notx fls) tru);;

Booleans are fun, but it gets much more interesting when you get into numbers. Church numerals are formed by a combination of two functions s and z. The s function is the "successor" function and z is the zero function. The first few church numerals are defined as:

**C(0) = λs.λz.z**

C(1) = λs.λz.s z

C(2) = λs.λz.s (s z)

C(3) = λs.λz.s (s (s z))C(1) = λs.λz.s z

C(2) = λs.λz.s (s z)

C(3) = λs.λz.s (s (s z))

If you think of s as "1+" and z as 0, then C(0) = 0, C(1) = 1+ 0, C(2) = 1+ (1+ 0), etc.

I defined a function p1 as shorthand for adding 1, and created a print_church function to display an integer version of a Church numeral:

let p1 = (+) 1;;

let print_church = fun c -> print_int (c p1 0);;

In this case, p1 is a partial function, the (+) operator takes two arguments, but since I only supplied 1, p1 actually returns a function that adds 1 to its argument.

Now, since I don't want to manually define each Church numeral, I defined a simple function that generates Church numerals:

let rec church = fun n s z->

if n = 0 then z

else s (church (n-1) s z);;

If you call

**print_church (church 55)**you'll see**55**.It is also possible to define the addition operation. Since a Church numeral is essentially defined by adding 1 over and over starting from 0, addition can just be defined as adding 1 over and over starting from another number, like this:

**plus=λa.λb.λs.λz.a s (b s z)**That is, instead of the usual z function, let a's z function be the evaluation of b (instead of counting from 0, a is calculated by starting from b). In OCAML, this can be defined as:

let plus = fun a b s z -> a s (b s z)

If you call

**print_church (plus (church 12) (church 34))**you should see a result of**46**.Multiplication can be defined in a similar way. Instead of adding 1 every time, you add b, like this:

**mult=λa.λb.λs.λz.a (b s) z**In OCAML, this is:

let mult = fun a b s z -> a (b s) z;

Again, using print_church, you can test the mult function. If you call

**print_church (mult (church 12) (church 34))**you should see**408**.You can get a little closer to the lambda calculus notation by using only single arguments in function definitions:

let tru = fun t -> fun f -> t;;

let fls = fun t -> fun f -> f;;