Introduction

Topic
5/9/17

Introduction

Due to Church. Very simple (based on elementary textual substitution), very powerful. In the 1930s and 1940s there was interest in the formal characterization of the informal notions of algorithm and computable by algorithm. There were several different lines into this including lambda calculus, recursive function theory, Turing's ideas on computability....Then it was proved that these different formal notions of lambda reducible, Turing computable, recursively enumerable... all captured exactly the same functions. They were equivalent. This provoked Church to propose what is known as Church's Thesis :

Church's Thesis:- computable = lambda reducible (= Turing computable = recursively enumerable= ..).

In other words, the informal notion of computable is captured exactly by all these different formal characterizations.

There is no question of proving Church's thesis as it asserts a relationship between informal and formal notions. There can though be arguments for or against it. One might criticise it by producing a hand-waving example which is suggested to be computable (step-by-step, deterministic, etc...) but yet not lambda reducible. As it happens, in the last 80 years no plausible counter-example has been offered. Indeed everything which appears to be computable has been shown to be lambda reducible. Church's thesis appears to be true.

If Church's thesis is true, everything that can be computed can be computed in the lambda calculus.

Also the lambda calculus is extremely simple, clear, and well understood. (It is true that the type-free lambda calculus was regarded somewhat suspiciously due to presumably being victim to similar paradoxes to those in naive set theory (does the set of all sets which do not contain themselves contain itself or not— if it does it does not and vv. This, Russell's paradox, is to some degree combatted by having a typed set theory). Dana Scott started producing models for lambda calculus in the late 60s and showed that type-free lambda calculus restricted to computable functions is ok— so all is well now.) There are also theorems in it about reduction orders which have great practical bearing on actual computing practice.

In brief, lambda calculus is an ideal theoretical foundation for Computer Science.

Functional programming languages are designed to sit on the lambda calculus. They start with a sound theoretical basis. As the cliché goes... All functional programming languages and constructs are syntactic sugar on top of lambda calculus.

Lambda calculus...

a) Expresses computation via anonymous functions (i.e. functions without names) and the functions are functions of a single variable.

b) Currying. This is a technique to deal with functions of several variables. Basically it treats the variables one at a time, often with the application of functions returning other functions as values. Functions are thus  'first class citizens'. Relies on free variables (needs closures or environments, and the like, if you are going to implement it) and the ability to return a function as a result (cannot do this in most computer programming languages). What this means will be explained.

Our interest is to take the bare calculus through to recursion (which is a feat because recursion relies on names and the lambda calculus does not have any) and to prove or become aware of various theorems about reduction.