Activity Sequence: Untyped Lambda Calculus

The untyped lambda calculus is a Turing-complete language. It only provides three constructs: function abstraction, function application, and variables. It has no constructs to represent numbers, logical values, or arithmetic or logical operators. It only has functions. Nothing else.

Church Booleans

If we want to represent Boolean values, we thus need to somehow represent them as functions. We can do that by encoding them as Church Booleans. A Church Boolean is a curried function of two arguments: the first argument specifies what to return if the function represents the value true, the second argument specifies what to return if the function represents the value false.

True as a Church Boolean

Let's define an expression to represent the Boolean value true. To be able to more easily refer to that expression, let's give it the name tru.

tru is a curried function with two arguments. It ignores the value of the second argument and always returns the value of the first argument.

The above tree exhibits two of the three kinds of terms of lambda calculus: abstraction (definition of an anonymous function with one parameter, as in λt. and λf.) and variable (node t).

False as a Church Boolean

Now let's define an expression to represent the Boolean value false. To be able to more easily refer to that expression, let's give it the name fls.

Like tru, fls also is a curried function with two arguments. It ignores the value of the first argument and always returns the value of the second argument.

Your tree should look almost identical to the one for tru. The only difference is that the body of the inner abstraction consists of f.

Conditionals based on a Church Boolean

Now that we have a way to express the two possible Boolean values, let's introduce a conditional operator (similar to a statement like if (l) { return m; } else { return n; }or an expression like l ? m : n in a language like Java). To be able to more easily refer to that expression, let's give it the name test.

test takes a Church Boolean l, which is either tru or fls, the argument m to return in case l is true, and the argument n to return in case l is false.

The above tree includes two applications. They are represented by a node  . The left hole of an application represents the function to apply and the right hole represents the argument. The inner application applies the function l to argument m. Note that l is the first argument (the argument of the outermost node λl. ) and corresponds to the logical condition. It is a Church Boolean, and thus a curried two-argument function. We apply it to m, get back another function of one argument, and apply that one to n. If l represents tru then we get back the first argument (m). If l represents fls then we get back the second argument (n).

This example shows how the complete application of curried functions leads to chains of application nodes ( ) in the tree, one node for each argument of the curried function.

Logical AND with Church Booleans

While test allows us to express conditionals, and thus allows us to map from Church Booleans to two arbitrary values, logical operators like AND, OR, and NOT may be more obvious operations on logical values. So let's define a logical AND for Church Booleans:

Here is how this and function works: it takes two Church Booleans b and c. If b is fls then b c fls returns fls. If b is tru then b x fls returns c.

Logical OR with Church Booleans

Now that we have seen how to construct a logical AND for Church Booleans, let's develop a logical OR.

Construct the expression tree for OR. Note that you will not need to use all of the available nodes. Double-click on a node to mark it as the root of the tree.

Logical NOT with Church Booleans

Logical AND and logical OR both are curried two-parameter functions. Now let's build the one-parameter function OR. Like previously, you are allowed to use the variables tru and fls (i.e., you do not need to recreate the expressions we bound to them earlier).

Construct the expression tree for OR. This time you have to construct the nodes yourself. You can type the node contents into the textfield. If you want to insert a hole into a node, use the character sequence {{}}. The lambda in the node is simply the corresponding character (you can copy-paste it from here: λ). Double-click on a node to mark it as the root of the tree.

Your probably realized that OR's parameter expects a Church Boolean, and that that Church Boolean will take two parameters.