Slide 12.1: The lambda calculus

Slide 11.11: Example II of program correctness (cont.)
Slide 12.2: Concepts and examples
Home

The Lambda Calculus

Functions play a prominent role in describing the semantics of a programming language, since the meaning of a computer program can be considered as a function from input values to output values. The lambda calculus is a formal mathematical system devised by Alonzo Church to investigate functions, function application and recursion. It is defined as follows:

Mathematical system for defining functions, proving equations between expressions, and calculating values of expressions.

It has influenced many programming languages but none more so than the functional programming languages. Lisp was the first of these although only the “pure” Lisp sublanguage can be called a true functional language. Three other functional programming languages are

Haskell, which is an open source product of more than twenty years. It includes a support for integration with other languages, built-in concurrency and parallelism, debuggers, profilers, and rich libraries.

Miranda, which is a pure, non-strict, polymorphic, higher order functional programming language designed by David Turner in 1983-6. The language was influencing in particular the design of Haskell, to which it has many similarities. Miranda is however a simpler language.

ML, which was conceived as a Meta Language for the theorem-proving system Edinburgh LCF, but it evolved into a successful general-purpose programming language. The language was standardised in 1990, and revised in 1997 as Standard ML '97.

Lambda calculus also provides the meta-language for formal definitions in denotational semantics. It has a good claim to be the prototype programming language.

Demonstration


let rec factorial = lambda n. if n=0 then 1 else n*factorial(n-1) in factorial 4 { this factorial covered by gnu GPL :-}