Lambda Calculus

Developed by Alonzo Church - late 1930s and early 1940s
- Deals with the application of functions to their arguments
- Pure lambda-calculus contains no constants and is untyped
- No numbers; No built-in primitive functions (such as plus)

- only lambda abstractions (functions), variables and applications of one function to another.
All entities must therefore be represented as functions.
For example, the natural number N can be represented as the function which applies its first argument to its second N times (Church integer N).

Church invented lambda-calculus in order to set up a foundational project
restricting mathematics to quantities with "effective procedures".
- Resulting system admits Russell's paradox ==> oops.

Most functional programming languages are equivalent to lambda-calculus

extended with constants and types.
- Scheme/Lisp uses a variant of lambda notation for defining functions
but only its purely functional subset is equivalent to lambda-calculus.

Lambda Abstraction

A term in lambda-calculus denoting a function.
A lambda abstraction begins with a lower-case Greek lambda,
followed by a variable name (the "bound variable"), a full stop (dot)
and a lambda expression (the body).



\ x . \ y . x+y

is read as



\ x . (\ y . x+y).

A nested abstraction such as this is often abbreviated to:



\ x y . x + y

The lambda expression (\ v . E) denotes a function which takes an argument
and returns the term E with all free occurrences of v replaced by the
actual argument. Application is represented by juxtaposition so



(\ x . x) 42

represents the identity function applied to the constant 42.

A lambda abstraction in Lisp is written as the symbol lambda,
a list of zero or more variable names and a list of zero or more terms, e.g.



(lambda (x y) (plus x y))

Lambda expressions in Haskell are written as a backslash, "\", one or
more patterns (e.g. variable names), "->" and an expression, e.g. \ x -> x.

	Reduction System
Reduction - "expression contraction" - a transformation process for expressions - done by applying certain reduction rules (maybe repeatedly) - there are different kinds of reduction Beta Reduction - Application of a lambda abstraction to one or more argument expressions - rewrite/simplify the lambda expression by first replacing "bound variables" with the actual args example: (lambda x . x10) 4 --> 410 - (note in this example the lambda function takes only one argument) Beta abstraction is the reverse of beta reduction example: 4 * 10 --> (lambda x . x*10) 4 Delta Reduction - Application of a mathematical function to the required number of arguments An evaluation strategy (or reduction strategy) - Determines which part of an expression (which redex) to reduce first. - There are many such strategies. Applicative Order Evaluation Normal Order Evaluation

Reduction System

Reduction

- "expression contraction"

- a transformation process for expressions

- done by applying certain reduction rules (maybe repeatedly)

- there are different kinds of reduction

Beta Reduction

- Application of a lambda abstraction to one or more argument expressions

- rewrite/simplify the lambda expression by first replacing "bound variables"

with the actual args

example:




(lambda x . x*10) 4  --> 4*10

- (note in this example the lambda function takes only one argument)

Beta abstraction is the reverse of beta reduction

example:




4 * 10 -->  (lambda x . x*10) 4

Delta Reduction

- Application of a mathematical function to the required number of arguments

An evaluation strategy (or reduction strategy)

- Determines which part of an expression (which redex) to reduce first.

- There are many such strategies.

Applicative Order Evaluation

Normal Order Evaluation

	Church Rosser Theorem
	Sometimes the most famous (best) theorems state the most obvious things.

This property of a
reduction system states that if an expression can be reduced by zero
or more reduction steps to either expression M or expression N then
there exists some other expression to which both M and N can be
reduced. This implies that there is a unique normal form for any
expression since M and N cannot be different normal forms because the
theorem says they can be reduced to some other expression and normal
forms are irreducible by definition. It does not imply that a normal
form is reachable, only that if reduction terminates it will reach a
unique normal form.

	So How does all this relate to Scheme?
It is not important that you know the lambda calculus thoroughly, but please consider these points: the pure lambda calculus is just like Scheme where the only allowed expressions are variables, lambda-forms with one formal argument, and applications of an expression to a single expression as actual argument. In this setting, when Scheme evaluates a procedure application, the computational process it generates is a series of 1-beta-reductions where, in each step, one contracts the rightmost redex not in the scope of any lambda-abstraction. (Here, ``rightmost'' means starting furthest to the right in the expression.) The Scheme data types, such as numbers, pairs, lists, and multi-argument functions can be represented using only lambda-calculus constructs. For example, natural numbers, (i.e., nonnegative integers) are represented as Church numerals [ see below ]. Simulating Scheme (and all Scheme's nifty features) in the lambda-calculus underscores the power of the lambda-calculus as a simple yet general programming language. This is

So How does all this relate to Scheme?

It is not important that you know the lambda calculus thoroughly, but
please consider these points: the pure lambda calculus is just like
Scheme where the only allowed expressions are variables, lambda-forms
with one formal argument, and applications of an expression to a
single expression as actual argument. In this setting, when Scheme
evaluates a procedure application, the computational process it
generates is a series of 1-beta-reductions where, in each step, one
contracts the rightmost redex not in the scope of any
lambda-abstraction. (Here, ``rightmost'' means starting furthest to
the right in the expression.)
The Scheme data types, such as numbers, pairs, lists, and
multi-argument functions can be represented using only lambda-calculus
constructs. For example, natural numbers, (i.e., nonnegative
integers) are represented as Church numerals [ see below ].
Simulating Scheme (and all Scheme's nifty features) in the lambda-calculus
underscores the power of the lambda-calculus as a simple yet general
programming language. This is

Pure Lambda Calculus
- no mutators, no assignment statements, no variables
- no data-types, no constants

- no numbers

Examples to create numeric type out of pure lambda fn's:

zero function

- think of fn with no arguments
- could call it, z()
- or just call it 0, but remember it's not a number in the normal sense

successor function

- s(s(s(0)))

- how to represent negative numbers
- with neg fn, where neg(S) is ok, but ...(s(Neg()...())) is not ok
- use pred and successor fn's

Normal Forms
- s(s(s(p(p(p(0))))))
- p(p(s(s(p(s(0))))))

- p(s(0))
- 0
- they're all the same but last one is in some sense most reduced
- see Church-Rosser theorem

Now we have numbers, but they're not numbers until we can add, multiply them



fn add(N, T)

(add s(N), T) ==> add N, S(T))

(add 0, T) ==> T