1

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.

Kevin Meredith
  • 969

2 Answers2

3

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.

John Hughes
  • 93,729
  • Reading your answer, it made me think of (const True) :: b -> Bool in Haskell. So, tru can be expressed in Haskell as: tru = const True, no? – Kevin Meredith Oct 16 '16 at 15:02
  • Also, as a follow-up, the lambda's in tru are simply arguments? And t is the output representing the True Boolean, i.e. a constant? – Kevin Meredith Oct 16 '16 at 15:05
  • @KevinMeredith true and false are defined so that the construction "if B then X else Y" is represented in lambda-calculus by "B X Y". If B is true then it will reduce to X, and if B is false then it will reduce to Y. – mercio Oct 16 '16 at 15:07
  • I know nothing about Haskell. It does not appear to me that the Haskell thing you've written corresponds to the lambda-calc notion I've described, but maybe it's just my lack of knowledge of the language. – John Hughes Oct 16 '16 at 15:20
0

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.

Alex M.
  • 35,207