Lambda Calculus

2010/11/14 § Leave a comment

I found λ-calculus very much interesting and important language in aspect of studying the theoretical properties of the programming languages and as it also forms the basic building blocks of the functional languages, so here i want to present a basic introduction to lambda calculus and some of its basic operations. Please don’t forget to check the links sections below if you want to study it in details, there are lots of good tutorials available in web have tried to index few of them.

Why lambda calculus ?
The λ-calculus can be called as the smallest universal programming language of the world. Good thing about lambda calculus it that it just consists of a single transformation rule (variable substitution) and a single function definition scheme and still we can represent very complex structure and operations with it. Lambda calculus was introduced by Alonzo Church in the 1930 as part of an investigation into the foundations of mathematics and part of which was found to be relevant to the computation so we use it to study theory of programming languages. Lambda calculus can be seen as equivalent to Turing machine but the main difference is that λ-calculus mainly depends on the transformation rules and does not care about the actual machine implementing it on the other hand Turing machine heavily depends on it so it makes λ-calculus more suitable for the study of programming properties without worrying about the hardware implementing it

lambda expressions are composed of
Variables, Abstraction and applications which can be represented as
e ::= x | ?x.e | (e1 e2)
or recursively we can describe as follows as follows:
<expression> ::= <name> | <function> | <application>
<function>    ::= ? <name>.<expression>
<application> ::= <expression><expression>
The only keywords used in the language are ? and the dot. In order to avoid cluttering expressions with parenthesis, we adopt the convention that function application associates from the left i.e f x y means (f(x))(y) and lambda abstraction extends far to the right as possible. For example ?x.xy means ?x.(xy) rather than (\x.x)y.

lambda expressions are composed of
variables, Abstraction and applications which can be represented as

e ::= x | λx.e | (e1 e2)

or recursively we can describe as follows as follows:

<expression>  ::= <name> | <function> | <application>
<function>    ::=  λ <name>.<expression>
<application> ::= <expression><expression>

The only keywords used in the language are λ and the dot. In order to avoid cluttering expressions with parenthesis, we adopt the convention that function application associates from the left i.e f x y means (f(x))(y) and lambda abstraction extends far to the right as possible. For example λx.xy means λx.(xy) rather than (λx.x)y.

An example of a function can be something like λx.x, which is a identity function. The name after the λ is the identifier of the argument of this function. The expression after the point (in this case a single x) is called the “body” of the definition. Functions can be applied to expressions. An example of an application is (λx.x)y This is the identity function applied to y.

The names of the arguments in function definitions do not carry any meaning by themselves. They are just “place holders”.
Therefore (λx.x)  (λy.y)  (λz.z)

Free and Bound variables
If we have functions like λx.y x then we say that x is bound and y is free variable, one important thing to remember is that a variable binds to its nearest lambda, so if we have expression like (λx.y x) x the outer occurrence of x is free because there is no occurrence of λ to bind that variable.

Substitution
Understanding substation is little-bit difficult at first as we don’t have any name for our functions and we can perform different kinds of reduction to evaluate our expression.Please go through the Wikipedia [http://en.wikipedia.org/wiki/Lambda_calculus#Reduction] or Chapter 2 of this tutorial [ftp://ftp.cs.kun.nl/pub/CompMath.Found/lambda.pdf]

Programming with Lambda calculus
Natural Numbers
.
By using some base type which can’t be reduced further than that say ‘0’ or [] , and a successor function we can define complete set of natural numbers in church encoding, here is how we can define church numerals


0 := λfz.z

1 := λfz.f z

2 := λfz.f (f z)

3 := λfz.f (f (f z))

..

n := λfz. f^n z

similarly successor function can be defined as

Succ = λnfz.f (n f z)

Addition of two numbers m and n can be defined as the m-th composition of f composed with the n-th composition of f, or it can also be defined using the successor function we define above, since adding m to n can be seen as 1 m times to n, so


Plus ::= λnfz.f (n f z)
or
Plus ::= λmn.m Succ n

similarly multiplication can be defined as


Mult := λmnf.m (n f)
or
Mult := λmn.m (PLUS n) 0

Predecessor function is bit tricky, as we are dealing with the natural numbers here we can define pred. as if n = 0, then pred 0 = 0, else pred n = n – 1


Pred := λn f x . n (λg h . h (g  f)) (λu . x) (λu . u)

Predecessor can also be defined using pair function,
let Pair(x, y) be a pair, fst return the first element and snd returns the second element of pair, and let Si = λp. pair (snd p) (succ (snd p)) , its a function generates from the pair (n-1, n) or alternatively we can say is a shift and increment function, given a pair (m,n) the function ss maps it to (n, n+1) so given this function we can define Pred as


Pred := λn.fst (n Si  (Pair 0 0)).

which applies function Si n times to (Pair 0 0) and selects the first member of the pair and this approach gives prd of zero as zero.

Boolean and Conditionals
True and False is defined in church numerals as follows


True := λ x y . x

Frue := λ x y . y

The definition of true and false can simply be seen as The true function takes two arguments and returns the first one, and the false function returns the second of two arguments. Given those definitions we can easily define the conditional expressions as follows.

Given those definitions we can easily define the conditional expressions as follows

if true then e1 else e2 = true e1 e2
= (\x y .x ) e1 e2
= e1

simililarly

if false then e1 else e2 = false e1 e2
= (\x y .y ) e1 e2
= e2

once we have cnditional we can define all other logical operations as


not p = if p then false else true

p and q = if p then q else false

p or q  = if p then true else q

Recursion

Defining recursion in lambda calculus is bit tricky, Recursion is the definition of a function using the function itself but as all the lambda expressions are name less so we can define the recursion as we are used to define it in the programming languages that supports recursion so we use the help of  fixed point combinators,


Y = λg.(λx.g (x x)) (λx.g (x x))

When any function is applied to the Fixed point combiner it simply calls a function and recreates it self

so if we apply g to Y it simply expands to g (Y g) i.e. Y g = g (Y g)

Please go through the Section 4 Recursion [www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf] of this paper or page two of this tutorial also has one nice example of how Fixed point is applied to recursive function in lambda calculus.

Similarly we can define other complex structures like tree, list etc using the pair.

So lambda calculus is very simple yet powerful and is a Turing-Complete and the lambda-calculus along of the “halting-problem” is unsolvable these properties make it as a perfect system for the theoretical study of programming languages.

Here are some of the resources to lambda calculus that can be freely available in web

[1] http://en.wikipedia.org/wiki/Lambda_calculus
[2] John Harrrison – Lambda calculus: [http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh-1996/chapter2.ps.gz]
[3] John Harrrison – Lambda calculus as a programming language: [http://www.cl.cam.ac.uk/teaching/Lectures/funprog-jrh-1996/chapter3.ps.gz]
[4] For solving your lambda expressions and checking reductions http://ellemose.dina.kvl.dk/~sestoft/lamreduce/lamframes.html
[5] A Tutorial Introduction to the Lambda Calculus – Ra´l Rojas [www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf]
[6] Church Numerals – http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf
[7] Introduction to Lambda Calculus – [ftp://ftp.cs.kun.nl/pub/CompMath.Found/lambda.pdf]
[8] Peter Selinger – Lecture Notes on the Lambda Calculus [http://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf]

Where Am I?

You are currently viewing the archives for November, 2010 at Dinesh Simk.