Lambda Calculus

The models of computation can be broadly classified into two groups - those that are based on machine model and the λ Calculus.

Machine models are based on the idea of a program acting on data by modification. So a Turing Machine consists of a program acting on the data. There is a clear distinction between program and data. Programs are not data and data do not contain programs (‘first order’). The machine based languages are inherently imperative.

λ-calculus is a formal system invented in the 1930s by Alonzo Church, in which all computation is reduced to the basic operations of function definition and application. There is no separation of program from data; the λ calculus is inherently “higher order”.

λ calculus is different from machine models because it is based on the mathematical concept of a variable (which is not at all related to the concept of a “variable”, a misnomer for “assignables” in machine models). λ-calculus emphasizes the use of symbolic transformation rules and does not care about the actual machine implementation.

Grammar

The syntax of the λ-calculus comprises just three sorts of terms.

• A variable x by itself is a term;
• The abstraction of a variable x from a term t1, written λx.t1, is a term;
• And the application of a term t1 to another term t2, written t1 t2, is a term.

These ways of forming terms are summarized in the following grammar.

t ::=      -- Terms
  x        -- Variable
  λx. t    -- Abstraction
  t t      -- Application

Abstraction and Application

Abstraction is a key feature of essentially all programming languages. Instead of writing the same calculation over and over, we write a function that performs the calculation generically, in terms of one or more named parameters, and then instantiate this function as needed, providing values for the parameters in each case.

A λ function is such an abstraction which has the form:

λ<variable>.<lambda term>    -- refer to the grammar above

λ-calculus embodies a kind of function definition (and application) that is the purest possible form. In the lambda-calculus everything is a function: the arguments accepted by functions are themselves functions and the result returned by a function is another function.

(λx. f x) 4

In the above example we define a function that applies the given parameter (x here) to a previously defined function f. The value 4 is then applied to this newly defined function.

Conventions

Here are important conventions:

• Function application is left associative, i.e. f g h = ((f g) h)
• Consecutive abstractions can be un-curried, i.e. λx y z. t = λx. λy. λz. t

Free and bound variables

In λ-calculus all names are local to definitions (like in most programming languages). In the function λx.x we say that x is “bound” since its occurrence in the body of the definition is preceded by λx. A name not preceded by a λ is called a “free variable.”

In the expression

(λx.x) (λy.y x)

the x in the body of the first expression from the left is bound to the first λ. The y in the body of the second expression is bound to the second λ, and the following x is free.

Beta Reduction

In its pure form, the lambda-calculus has no built-in constants or primitive operators—no numbers, arithmetic operations, conditionals, records, loops, sequencing, I/O, etc. The sole means by which terms “compute” is the application of functions to arguments (which themselves are functions). Each step in the computation consists of rewriting an application whose left-hand component is an abstraction, by substituting the right-hand component for the bound variable in the abstraction' s body.

Following Church, a term of the form (λx.t1)t2 is called a redex (“reducible expression”), and the operation of rewriting a redex according to the above rule is called beta-reduction.

• Full Beta Reduction: Any redex may be reduced at any time. At each step we pick some redex, anywhere inside the term we are evaluating, and reduce it
• Normal Order Beta Reduction: The leftmost, outermost redex is always reduced first.
• Call By Name Beta Reduction: This is more restrictive form of normal order reduction, allowing no reductions inside abstractions.
• Call By Value Beta Reduction: Only outermost redexes are reduced and where a redex is reduced only when its right-hand side has already been reduced to a value.

Boolean Definitions

tru = λt. λf. t;
fls = λt. λf. f;

tru t f = t
fls t f = f

tests

test = λl. λm. λn. l m n;

test pred l m = pred l m
test tru "a" "b" -- "a"
test fls "a" "b" -- "b"

Reducing Test term

 test tru v w
 = (λl.λm.λn.l m n) tru v w         by definition
 → (λm.λn.tru m n) v w
 → (λn.tru v n) w
 → tru v w
 = (λt.λf.t) v w                    by definition
 → (λf. v) w
 → v

Logical Ops

and = λb. λc.b c fls;

and1 p q = p q fls   -- if p then q   else fls
or1  p q = p tru q   -- if p then tru else q
not1 p   = p fls tru -- if p then fls else tru

Pairs

pair = λf.λs.λb. b f s;
fst = λp. p tru;
snd = λp. p fls;

Pair v w is a function that, when applied to a boolean value b, applies b to v and w.

pair f s b = b f s
fst p = p tru
snd p = p fls

Reducing fst

  fst (pair v w)
= fst ((λf.λs.λb.b f s) v w)
→ fst ((λs.λb.b v s) w)
→ fst (λb. b v w)
= (λp.p tru) (λb.b v w)
→ (λb.b v w) tru
→ tru v w
→ v

Church Numerals

• For representing numbers by lambda-terms
• A number n is represented by a combinator (one, two, three, etc. below) that takes two arguments, s and z, and applies s, n times, to z.
• As with booleans and pairs, this encoding makes numbers into active entities: the number n is represented by a function that does something n times — a kind of active unary numeral.

zero  = λs. λz. z;            -- applies s to z zero times
one   = λs. λz. s z;          -- applies s to z once
two   = λs. λz. s (s z);      -- applies s twice
three = λs. λz. s (s (s z));  -- applies s three times
etc.                          -- and so on...

Successor

Remember, a Church numeral n is a function that applies s to z (n times).

scc = λn. λs. λz. s (n s z); -- Successor function

The term scc is a combinator that takes a Church numeral n and returns another Church numeral—that is, it yields a function that takes arguments s and z and applies s repeatedly to z. We get the right number of applications of s to z by first passing s and z as arguments to n, and then explicitly applying s one more time to the result.

scc  n s z = s (n s z)
scc' n s = s . n s

We can think of successor function in two ways. One way, as defined above, is applying s one more time to given number. Another way is to add given number n to one. Second approach is given below:

scc = λn. λs. λz. n s (s z)

scc  n s z = n s (s z)

Let us see if scc one is actually two:

scc one
= scc (λs. λz. s z)                       -- by definition of one
= (λn. λs. λz. n s (s z)) (λs. λz. s z)   -- by definition of scc
→ (λs. λz. (λs. λz. s z) s (s z))
→ λs. λz. (λz. s z)(s z)
→ λs. λz. s (s z)
= two                                     -- by definition, s applied twice

Addition

Addition of Church numerals can be performed by a term plus that takes two Church numerals, m and n, as arguments, and yields another Church numeral—i.e., a function—that accepts arguments s and z, applies s iterated n times to z (by passing s and z as arguments to n), and then applies s iterated m more times to the result:

plus = λm. λn. λs. λz. m s (n s z);

We can also think of addition in terms of successor (or increment) function.

plus m n = m incr n

Here, we apply m times the incrementation to n. In other words, increment n, m times.

Now, we can write -

two   = plus one one
three = plus two one
four  = add two two

Multiplication

Multiplying n and m is adding together m copies of n. Notice that, plus m adds m to any given number. If we apply add m n times to zero, we will have added n copies of m.

times = λm. λn. m (plus n) zero;

Intuitively, having a s.s.s. ... s of length m, in order to multiply it by n, we should combine n copies of such a chain. Or, if (m s) is a “super-successor” containing m exemplars of s, what we need is

mul n m s z = n (m s) z

which is same as

mul n m = n . m

Multiplication is functional composition!

Exponentiation

pow n m means n raised to m-th power. Or, n * n *.....* n- multiplying n by itself m times.

pow n m
 = (mul n ( ... (mul n (mul n one))))  -- m times
 = m (mul n) one

We know that in the theory of sets, for any sets A and B, the notation B^A denotes the set of all functions from A to B. Typically one applies the argument based on cardinality. Adding one element to A, permits to find |B| more mappings, from the additional element to all of B. So, the number of mappings is multiplied by |B|, in agreement with : B^A+1 = B^A * B.

pow n m = m n

exponentiation = inverse application.

isZero

To test whether a Church numeral is zero, we apply our numeral to a pair of terms zz and ss such that applying ss to zz one or more times yields fls, while not applying it at all yields tru.

Remember zero is a function that applies s to z zero times - zero = λs. λz. z or zero = λs. id.

That is, we need ss and zz such that zero ss zz is tru and fls for any other numeeral.

iszro = λm. m (λx. fls) tru;

Predecessor

Predecessor function is tricky! We begin with zero, and keep counting until n, but storing the previous number. Then when we get n, the previous one is its predecessor. We use Pairs, defined earlier, to keep two previous numbers.

zz = pair zero zero
ss  = λp. pair (snd p) (plus one (snd p));
prd = λm. fst (m ss zz);