Understanding `tru` in Lambda Calculus from TAPL

Question

In Dr. Benjamin Pierce's Types and Programming Languages, page 58 notes:

Another language feature than can be easily encoded in the lambda-calculus is boolean values and conditions. Define the terms tru and fals as follows:

tru = $\lambda$t. $\lambda$f. t;

fals = $\lambda$t. $\lambda$f. f;

The terms tru and fls can be viewed as representing the boolean values "true" and "false," in the sense that we can use these terms to perform the operation of testing the truth of a boolean value.

Looking at the tru definition (if that's the right word), what does each term mean? I assume that t is the argument to the function?

In short, I'm requesting an explanation of the terms of tru. In addition, I'd appreciate an explanation of how tru would be called/invoked.

Answer 1

You can think of tru as a function of two arguments (represented by currying): it takes args (t, f) to t. These are not great name choices, since they're easily confused with "true" and "false"; I could equally well have said "it takes args (x, y) to x," instead. But you'll see shortly why they're used.

Similarly, fals takes (t, f) to f.

Why these are the right definitions? That's a little trickier.

Suppose you have an expression like

if cond then e1 else e2

whose value is e1 if the condition is true, and whose value is e2 if the condition is false. You can rewrite this in lambda-calc form as

cond(e1, e2)

(or, in real lambda calc form, as "cond e1 e2", since it eschews parens...but I find programming-language-like form easier to read).

If cond is tru, then cond(e1, e2) will be e1; if it's fals, then cond(e1, e2) will be e2, just as desired.

So an "if expression" can be encoded as a function-application, where the applied function is the "condition", which is either "tru" or "false".

I apologize for this answer using kind of a mashup of notations, etc., but I hope that the gist comes across OK.

Answer 2

You could view tru as the map $(t,f) \mapsto t$ and fals as the map $(t,f) \mapsto f$. In a different choice of words, tru is the projection on the first factor of a Cartesian product of two objects, while fals is the projection on the second one. They are precisely the functions car and cdr from Scheme. That these two functions may be used to simulate boolean operations is, indeed, amazing.