Since languages with recursible first-class functions are Turing-complete, they should be able to express anything expressible in any other programming language. Therefore, it should be possible to model conditional expressions (i.e. if-statements) with first-class functions. Could someone illustrate how to do this?

  • $\begingroup$ Well usually this can be done by encoding true and false as functions: en.wikipedia.org/wiki/Lambda_calculus#Logic_and_predicates $\endgroup$ – Willem Van Onsem May 11 '18 at 7:15
  • $\begingroup$ This is called Church Encoding: en.m.wikipedia.org/wiki/Church_encoding That’s a really good keyword to start your search, and there should be quite a few tutorials on the subject too. Personally, I found ”Programming with nothing” a good hands-on exercise. $\endgroup$ – Ezku May 11 '18 at 7:20
  • $\begingroup$ Church encoding works to construct data types in untyped lambda calculus. The related Böhm–Berarducci Encoding, introduced in Automatic synthesis of typed Λ-programs on term algebras, gives a way of translating algebraic data types systematically to typed lambda calculus (System F) that also lets you easily eliminate (pattern-match) on the values. $\endgroup$ – Jon Purdy May 12 '18 at 2:26
  • $\begingroup$ Church encoding also works perfectly in the typed setting of System F. For instance, Church booleans can be given the type $\forall X.X → X → X$, and Church naturals can be given the type $\forall X.(X → X) → X → X$. $\endgroup$ – Rodolphe Lepigre May 12 '18 at 15:05

The usual encoding of booleans, due to Church, is

$$ {\sf true} = \lambda x. \lambda y. x \qquad {\sf false} = \lambda x. \lambda y. y $$

Roughly, "true" is the function which takes two arguments $x,y$ (first takes $x$, then also takes $y$) and returns the first one. Instead, "false" returns the second one.

If-then-else is then encoded as applying an encoded boolean to the "then" and "else" branches. In this way, the boolean chooses the right value to return.

$$ {\sf if}\ b\ {\sf then}\ t\ {\sf else}\ e = b\, t\, e $$

It is then easy to check the so-called "$\beta$" laws:

$$ {\sf if\ true\ then}\ t\ {\sf else}\ e = {\sf true}\, t\, e = (\lambda x.\lambda y.x)\, t\, e = (\lambda y.t)\, e = t $$


$$ {\sf if\ false\ then}\ t\ {\sf else}\ e = {\sf false}\, t\, e = (\lambda x.\lambda y.y)\, t\, e = (\lambda y.y)\, e = e $$

Essentially, these laws state what happens when you "construct" a boolean (using the constants $\sf true, false$), and then "destruct" it later on (using it in an $\sf if\ then\ else$).

Using functions in this way, one can write encodings for all the usual data types, like naturals, pairs, variants, lists, trees, etc.

| cite | improve this answer | |

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.