16
$\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.

Improve this question
$\endgroup$
5
  • 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, 2012 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, 2012 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, 2012 at 13:41
  • 6
    $\begingroup$ I feel like I should get some credit for running such a nifty blog :-) $\endgroup$
    – Andrej Bauer
    Feb 6, 2012 at 13:51
  • 8
    $\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, 2012 at 12:59

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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