Question

How do you define a function that tests if a number is even using lambda calculus? The function should return true if the number is even, and false otherwise.

Answer 1

Lambda calculus is a notation for describing mathematical functions and programs. It is a mathematical system for studying the interaction of functional abstraction and functional application. It captures some of the essential, common features of a wide variety of programming languages. Because it directly supports abstraction, it is a more natural model of universal computation than a Turing machine is.

A λ-calculus term is:

• a variable x∈Var, where Var is a countably infinite set of variables;
• an application, a function e₀ applied to an argument e₁, usually written e₀e₁ or e₀(e₁); or
• a lambda abstraction, an expression λx.e representing a function with input parameter x and body e. Where a mathematician would write x ↦ x², or an SML programmer would write fn x => x*x, in the λ-calculus we write λx.x².

In BNF notation,

e ::= x | λx.e | e₀e₁

We use the metavariable e to represent a λ-calculus term.

Parentheses are used just for grouping; they have no meaning on their own. Like other familiar binding constructs from mathematics (e.g., sums, integrals), lambda terms are greedy, extending as far to the right as they can. Therefore, the term λx. λy. y is the same as λx.(x (λy.y)), not (λx.x) (λy.y). As in SML, application terms are left-associative, so x yz is the same thing as (x y) z.

For simplicity, multiple variables may be placed after the lambda, and this is considered shorthand for having a lambda in front of each variable. For example, we write λxy.e as shorthand for λx.λy.e. This shorthand is an example of syntactic sugar. The process of removing this shorthand is currying, just as in SML, and adding it is called uncurrying.

We can apply a curried function like λx.λy.x one argument at a time. Applying it to one argument results in a function that takes in a value for x and returns a constant function, one that returns the value of x no matter what argument it is applied to. As this suggests, functions are just ordinary values, and can be the results of functions or passed as arguments to functions (even to themselves!). Thus, in the lambda calculus, functions are first-class values: lambda terms serve both as functions and data.

We introduce the following two functions

which we call the values

“true” T ≡ λxy.x and

“false” F ≡ λxy.y

The first function takes two arguments and returns the first one, the second function returns the second of two arguments.

3Logical operations It is now possible to define logical operations using this representation of the truth values.

The AND function of two arguments can be defined as ∧ ≡ λxy.xy(λuv.v) ≡ λxy.xyF

The OR function of two arguments can be defined as ∨ ≡ λxy.x(λuv.u)y ≡ λxy.xTy

Negation of one argument can be defined as ¬ ≡ λx.x(λuv.v)(λab.a) ≡ λx.xFT

The negation function applied to “true” is ¬T ≡ λx.x(λuv.v)(λab.a)(λcd.c)

which reduces to TFT ≡ (λcd.c)(λuv.v)(λab.a) = (λuv.v) ≡ F that is, the truth value “false”