15
$\begingroup$

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way.

true  = \t. \f. t;
false = \t. \f. t;
not   = \x. x false true;
and   = \x. \y. x y false;
or    = \x. \y. x true y;

Also boolean algebra can be encoded in System F in this way:

CBool = All X.X -> X -> X;
true  = \X. \t:X. \f:X. t;
false = \X. \t:X. \f:X. f;
not   = \x:CBool. x [CBool] false true;
and   = \x:CBool. \y:CBool. x [CBool] y false;
or    = \x:CBool. \y:CBool. x [CBool] true y;

Is there a way to express boolean algebra in simply typed lambda calculus? I assume that answer is NO. (For example, Predecessor and lists are not representable in simply typed lambda-calculus.) If the answer is NO indeed, is there a simple intuitive explanation, why it is impossible to encode booleans in simply typed lambda calculus?

UPDATE: We assume that there are base types.

UPDATE: The negative answer with explanation was found here (Comment "Here's a proof sketch to show that simply-typed lambda calculus with products and infinitely many base types does not have booleans.") This is what I was looking for.

$\endgroup$
  • 2
    $\begingroup$ Try typing the definitions into Haskell and see what happens when you give types to various expressions. You'll see that the code relies heavily on polymorphism. $\endgroup$ – Dave Clarke Feb 6 '12 at 12:30
  • 2
    $\begingroup$ Sorry to be pedantic, but questions about the expressivity of this or that calculus become meaninful only with a clear understanding of what you mean by "expressed", "encoded" and "represented", as there are multiple reasonable ways of understanding these terms. Moreover, since you stipulate the existence of base-types, you'd need to be specific about what those are, and what constructors/destructors they come with. $\endgroup$ – Martin Berger Feb 6 '12 at 12:48
  • 3
    $\begingroup$ Sorry that I was not pedantic. The answer was found here: math.andrej.com/2009/03/21/… $\endgroup$ – Ilya Klyuchnikov Feb 6 '12 at 13:41
  • 3
    $\begingroup$ I feel like I should get some credit for running such a nifty blog :-) $\endgroup$ – Andrej Bauer Feb 6 '12 at 13:51
  • 7
    $\begingroup$ The definition of a Boolean type used on the blog is stronger than here. In fact, Jeremy’s answer shows that simply typed lambda calculus with at least one base type (call it $O$) can express Boolean algebra in the sense of the OP: define $B=O\to O\to O$, $\mathrm{true}=\lambda x:O.\lambda y:O.x$, $\mathrm{false}=\lambda x:O.\lambda y:O.y$, $\mathrm{not}=\lambda a:B.\lambda x:O.\lambda y:O.ayx$, $\mathrm{and}=\lambda a:B.\lambda b:B.\lambda x:O.\lambda y:O.a(bxy)y$, $\mathrm{or}=\lambda a:B.\lambda b:B.\lambda x:O.\lambda y:O.ax(bxy)$. $\endgroup$ – Emil Jeřábek Feb 7 '12 at 12:59
3
$\begingroup$

The OP wrote above that the question is answered by a post on @AndrejBauer's blog.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.