Understanding conditional expressions with λ calculus

In spite of the fact that the structure of imperative programming languages is modeled on a machine architecture, […], some believe that using imperative languages is somehow more natural than using a functional language. So, these people [computer scientists] believe that even if functional programs were as efficient as imperative programs, the use of imperative programming languages would still dominate.
- Sebesta, R. W. (1993). Concepts of programming languages. Pearson Education India.

Our computers are based on von Neumann architecture, where it's primary components are the memory, which stores instructions and data, and the processor, which provides operations for modifying the contents of the memory — the basis of imperative and OO programming languages. Thanks to the evolution of hardware, compiler optimization and the immutable state that helps to solve concurrency problem, non-efficient functional algoritms aren't a problem anymore, so much that programming languages like Erlang and Elixir were created.

λ calculus is the model of computation that functional programming is based on and it is Turing complete, this means that every λ calculus program has a turing equivalent program — so the halting problem is still over there. It's main purpose is to manipulate λ expressions, that may be a name, a function or a function application.

A name is just a sequence of characters. A function is an abstraction over a λ expression and it has the form λ<name>.<body>. We can give names to functions using def, e.g. def <name> = <function>.

The simplest function is the identity function: def identity = λx.x.

JS equivalent to identity.

The third kind of λ expression is an application, which has the form
(function argument) — any resemblance to Lisp's syntax isn't pure coincidence.

We can apply identity to any value and it will returns it, so we can apply identity to identity, since we treat functions as values.

Application of identity function to identity.

Conditional expressions

The base form of a conditional (ternary) expression is:

<cond> ? <expr1> : <expr2>

We can model it as def cond = λexpr1.λexpr2.λc.((c expr1) expr2), because boolean values are defined as:

def true = λfirst.λsecond.first
def false = λfirst.λsecond.second

true is a function that receives two arguments and returns first, while false also receive two arguments, but returns second. This means that if c is true, cond will return expr1(first argument), but if is false, will return expr2 (second argument).

There are λ calculus abstractions about the truth table, and we are going to explore the operator and. We can model it as and = x ? y : false. So, if x is false, false is returned. Otherwise, the return depends on y's value, so we define and as:

def and = λx.λy.(((cond y) false) x)

Replacing cond from and expression and simplifying it, we get:
 (I underline on each line the name that is being replaced)

Simplifying body of and function.

We will now use def and = λx.λy.((x y) false).

JS equivalent to and.

So far, we have been using lots of brackets to manipulate λ expressions and we can reduce this by just eliminating them, so instead of
((<function> <arg1>) <arg2>) we can use <function> <arg1> <arg2> in a function application. We can also simplify name/function association by dropping the “λ” and the “.” and moving the bound variable to the left of the “=”, so
def <names> = λ<name>.<body> becomes 
def <names> <name> = <body> . Now we can rewrite and expression as
def and x y = x y false.

We can also rewrite the cond expression to an
def cond expr1 expr2 c = c expr1 expr2 and then cond c expr1 expr2, which is the same as cond <condition> <true choice> <false choise>
and finally to an if…. then… else… form:

if <condition>
then <true choice>
else <false choice>

And we end up with the usual imperative form of a condition evaluation :)

def and x y =
 if x
 then y
else false


This article was based on chapters 1–3 of An Introduction to Functional Programming Through Lambda Calculus. An brief and also good reference is the λ calculus chapter from Haskel Programming from first principles book and a blog post from Caelum [pt-BR].