From MCIS Wiki

Contents 1 The Lambda Calculus 2 Slides 2.1 Alonzo Church 2.2 Influence 2.3 Definitions 2.4 Computational Mechanism: Beta Reduction 2.5 The "Reduces to" Graph 2.6 Some Functions 2.7 Alpha Conversion 2.8 Semantics 2.9 Encoding Values 2.10 Adding Vocabulary 2.11 Adding "Let" 2.12 Currying 2.13 Haskell Curry 2.14 Combinators 2.15 The Church Rosser Theorem 2.16 Equational Reasoning 2.17 Recursion 2.18 Reduction Strategies 2.19 Haskell Example 2.20 Wrapup

The Lambda Calculus

Some background resources:

• http://en.wikipedia.org/wiki/Lambda-calculus
• http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf
• http://users.bigpond.net.au/d.keenan/Lambda/

Slides

Lambda Calculus is one of the earliest formal "computing machines". It was developed to investigate the "decision problem" – is there an algorithm that can tell if statements in first-order predicate calculus are true?

Unfortunately, Gödel's incompleteness theorem applies and thus there is no algorithm to decide the truth of general math propositions!

Alonzo Church

Church developed Lambda Calculus. His field was logic – not computer science – but his work has served as one of the foundations of computer science

Alan Turing was a student of Church

Influence

• Programming language design (Lisp, Haskell, other functional languages)
• Semantics and compiler construction
• Type systems – the typed lambda calculus and other λ constructions
• Parallel programming

A Turing machine resembles computer hardware; Lambda Calculus resembles real programming languages.

Definitions

An expression is either:

• a variable – usually a letter such as x
• an application – a function applied to an argument. Written as e1 e2 – associates left, so� f g h means (f g) h
• an abstraction, written λx.e – we abbreviate λ x . λ y . z as λ x y . z

That's it! This gives you the "language" – a way of expressing the values in Lambda Calculus

It's often easier to visualize things graphically. Expressions can be represented as a tree: application (the symbol @ is often used) forks the tree, variables are at the leaves, and a lambda is a special node in which the left side is always a variable.

Example:

media:lamtree.png

Computational Mechanism: Beta Reduction

The idea behind Lambda Calculus is that there is an underlying "computational engine" that rewrites expressions.

This engine is non-deterministic – there may be many different things it can do to an expression.

When the left side of an application is a lambda term, the lambda is "called" and the result is the expression after the "." with the variable replaced by the expression on the right of the application.

You replace EVERY occurrence of the variable.

((λ x . (λ y . x)) (λ z . z)) (λ a . a)   =>
(λ y . (λ z . z)) (λ a . a)               =>
(λ z . z)

Beta reduction is the ONLY thing you need to make lambda calculus go!

An expression may have MANY reducable expressions in it – you can choose any to reduce.

The "Reduces to" Graph

You can create a graph whose nodes are lambda expressions and edges correspond to beta reductions.

Media:lamred.png

Note: this may be cyclic! Infinite loops are possible

Some Functions

λ x . x   -- This is the identity function (I)
λ y . y y  -- This applies a function to itself
λ x . (λ y . x)  -- This is called the constant function 

Alpha Conversion

The names of the variables in an expression are not "meaningful" – just as in a real programming language.

Ignoring "name capture", this gives a way of deciding if two expressions are the same.

So you would be able to show that λ x . x and λ y . y are the same expression. Compilers generally perform "alpha conversion" to replace all names by unique ones.

Semantics

So what is the meaning of a lambda calculus expression? This meaning is obtained by doing beta-reductions. That is, beta reduction preserves meaning.

A term in which no beta-reductions are possible is in "normal form". Two terms denote the same thing if they both reduce to the same normal form. Some terms are "strongly normalizing" – all reduction sequences are finite and lead to the same result. Same as "programs that always halt".

Encoding Values

This can be deeply confusing – the only "data" that lambda calculus works with is λ.

But you can encode any value as a lambda term! Church discovered a simple representation of integers:

0 := λ f . λ x. x 
1 := λ f . λ x. f x 
2 := λ f . λ x. f (f x) 
3 := λ f . λ x. f (f (f x)) 

How would you "add" such numbers?

All of the big theorems of lambda calculus can be proven without needing to add any new "domains". This is sufficient to prove that the decision problem is unsolvable.

But, in practical terms, trying to figure out what's going on when you have to write λ f λ x. f (f (f x)) instead of "3" is hard.

Adding Vocabulary

To use lambda calculus in a more conventional way, we add a vocabulary beyond plain lambda terms.

All we need to do is add one extra form of lambda expression, a constant, to the set of lambda terms. For example, you could add natural numbers 0, 1, 2, and so on as constants in the language.

Besides domain constants, you also need domain functions. All this means is that some of the domain constants are reducable. In other words, the term "k e", for some constant k, may be rewritten as some value determined by k and the input e.

For example, if "increment" and "0" are domain constants, then "increment 0" would rewrite to "1". This sort of reduction is "outside" of the ordinary lambda calculus beta reduction.

Adding "Let"

In real languages, we place a value in a variable so it can be used repeatedly by name.

   x = … big hairy expression …
   y = x + 1
   z = x * 4

W can do the same thing in L-C:

 (λ x . <exp>) <val>

is just a way to package up the <val> into a variable named "x". This is notated "let x = val in exp"

Currying

Unlike most programming languages, lambda calculus only supports functions with a single argument.

So how do you handle functions with more than one argument? Easy: a function of two arguments becomes a function of one argument which returns another function of one argument.

You write ((f x) y) to apply f to arguments x and y and λ x . λ y . <body> to denote a function of two arguments.

Haskell Curry

Haskell Curry was a pioneer in combinatory logic. The term "currying" is named after him even though someone else, Schönfinkel, actually came up with it first. But I'd rather say "Currying" than "Schönfinkeling" so it's OK by me. The Haskell language is named after him.

Combinators

A "combinator" is a lambda calculus term with no free variables. You can express combinators in lambda calculus but it's also possible to discard lambda calculus and work directly with combinators – hence "combinatory logic".

There are many different combinator sets that can form a basis for lambda calculus – the most commonly used is SKI (What's a basis???)

Any closed lambda calculus term corresponds some "tree" of S, K, and I combinators.

In programming language terms, a combinator is just a "top level" function.

comp = λ f . λ g . λ x . f (g x)     -- function composition

Here are SKI:

I = Identity = λ x. x
K = Constant = λ x . λ y . x
S = Substitution = λ x . λ y . λ z . x z (y z)
  (or sharing – x and y share z as an input)

For example, the Church Numeral for 2 expressed using SKI is

 S (S (K S) K) I

The Church Rosser Theorem

This is the "biggie" in terms of lambda-calculus theory. It states that it doesn't matter which reducable part of an expression you choose to apply beta reduction to. All choices eventually converge to a unique "normal form" (or go on endlessly!)

In programming language terms, you can evaluate expressions in any order without changing the result. This is certainly true in math:

    (2+3)*(4+5) => 5*(4+5) => 5*9 => 45
    (2+3)*(4+5) => (2+3)*9 => 5*9 => 45

It's C-R that allows you to parallelize programs expressed in lambda calculus. If there is more than one reducable part of a term, it can be evaluated on different machines.

This is also the source of "purity" – that is, a term has exactly one normal form (meaning).

Equational Reasoning

Another way to think about lambda calculus is that it gives you a way of transforming a program. This is exactly the same way that we reason about math terms – if two terms are equivalent, we can replace one by the other in an equation.

This can involve running Beta-reduction "backward" – this is called unfolding.

Recursion

It would seem that lambda calculus doesn't do recursion that way an ordinary programming language does. There is no notion of "naming" something so that it can refer to itself.

This can be addressed by the "Y" combinator:

Y = λf.(λx.f (x x)) (λx.f (x x)) 

Discovered by our buddy Haskell Curry!

It's not worth trying to work this out now but it's not all that hard – a recursive function gains an extra parameter which is "itself".

Reduction Strategies

Even if a term has a normal form you still need to choose reductions wisely. It's possible to go into an "infinite loop" reducing things in a normalizable term – all C-R guarantees is that some strategy will eventually find the normal form.

Of course, some terms have NO normal form. (Some programs are always infinite loops!)

Lambda calculus is a perfect way to model the semantics of a programming language.

That is, we want to "compile" programs into lambda calculus so that we have a formal way of determining its meaning.

You can also address reduction strategies.

Call by value = normalize function arguments before reducing the function

Call by need = normalize the result of the program instead of the arguments

CBN is "more general" than CBV in that more programs terminate

The one "big" language to be based on L-C is Haskell.

This uses a CBN evaluation order (that is, it finds a result if there is one) A type system adds "discipline" to the construction of the program – some L-C terms cannot be directly implemented in Haskell (the Y combinator, for example).

Haskell Example

Here's some Haskell code to chew on:

module Main where
i      = \x -> x
k      = \x -> \y -> x
s      = \x -> \y -> \z -> x z (y z)
zero   = \f -> \x -> x
one    = \f -> \x -> f x
two    = \f -> \x -> f (f x)
three  = \f -> \x -> f (f (f x))
church = \t -> t (+1) 0
skiTwo = s (s (k s) k) i
add    = \f -> \g -> \h -> \x -> f h (g h x)

Wrapup

• Studying L-C is a good way to learn about programming languages in general
• L-C is a formula for building new languages from a given vocabulary
• Reasoning about programs is important: L-C gives us tools to reason in a mathematical way about programs.
• A VERY simple language (constants, variables, application, and abstraction) are all that is needed to represent any program in any language