Lambda Calculus: What about “if”

In the last article we talked about subtraction. But of course there is more to “programming” than just arithmetic. One of the most basic things we need is a way to decide an output based on some value. You all know this as “if” and we will talk in this part about representing Booleans and implementing a “if” function like this:

$$ If(condition, then, else) = \begin{cases} then & \text{if } condition=true \\ else & \text{else} \end{cases} $$

Representing Booleans

Just like with the natural numbers we introduced in the first article we are going to represent \(T\) (short for true) and \(F\) (short for false) in the form of abstractions – to be more precise: we will just reuse the tuple-selectors from the previous article:

$$ T := \lambda xy.x $$ $$ F := \lambda xy.y $$

And, Or, Not

The next step is to get the usual logical operators into our calculus. Let’s start with \(And\). It should operate on two Booleans \(a\) and \(b\) and return another Boolean, that is an abstraction with two parameters. Now if both arguments are \(T\) the resulting function has to return the first argument you can pass to it, if not the second. Of course \(a\) will behave similar: if it is true it will return the first argument given, if it is false the second. As we have to chain two true’s you can see that the following abstraction does the trick (you might observe that this uses “currying”).

$$ And := \lambda ab.abF $$

Here is a sample session from my interpreter to verify that this is indeed a AND:

LAMBDA CALCULUS INTERPRETER
===========================
>>> T := \xy.x
\xy.x
== [T]
>>> F := \xy.y
\xy.y
== [F]
>>> And := \ab.abF
\ab.(ab\xy.y)
== [And]
>>> And T T
\xy.x
== [T]
>>> And T F
\xy.y
== [F]
>>> And F T
\xy.y
== [F]
>>> And F F
\xy.y
== [F]

Of course you can also work this out with a pencil and the lambda-calculus rules.

OR is similar: if the first argument is true than we can return true, if not the answer is just the second argument (remember: \( true || b = true \) and \( false || b = b ). This translates directly into

$$ Or := \lambda ab.a T b $$

>>> Or := \ab.a T b
\ab.(a\xy.xb)
== [Or]
>>> Or T T
\xy.x
== [T]
>>> Or T F
\xy.x
== [T]
>>> Or F T
\xy.x
== [T]
>>> Or F F
\xy.y
== [F]

Having seen all this NOT should not be a problem for you (right? – you might want to try it before reading on – I will give you the answer at the end Zwinkerndes Smiley )

Finally: IF

After all of this IF is just a piece of cake – remember: if the condition is true we want to return the first argument that follows (the \(then\)-branch); and if the condition is false we want to return the second argument (the \(else\)-branch).

You should know by now that this is just the behavior that \(True\) and \(False\) already have! So the “condition” already does the work and our IF is just the identity-function – neat isn’t it?

In case you don’t believe:

>>> If := \x.x
\x.x
== [If]
>>> If T a b
a
>>> If F a b
b

Promised you your not…

So here is the NOT – in case you did not find yourself (there are many right definitions) – the easiest one is just to use the same trick as with the IF – use the argument to invert:

$$ Not := \lambda a.a F T $$

>>> Not := \a.a F T
\a.(a\xy.y\xy.x)
== [Not]
>>> Not T
\xy.y
== [F]
>>> Not F
\xy.x
== [T]

Conclusion

So this is it – the first control-structure you need for a general-purpose programming language – and it was rather easy.

BTW: we have already seen how to do a kind of FOR loops – you can just use the natural number representation for that.

It’s much harder to get something similar to a WHILE loop, or – as we are in functional land, a recursive function. And in the next article we will see how to implement this using one of the infamous fixpoint operators – so stay tuned Smiley mit geöffnetem Mund