The Lambda Calculus ------------------- NOTE: I will use L, rather than greek lambda (easier to print) Devised by Alonzo Church circa 1930, as a model for computability. Simple and powerful system, based on function ABSTRACTION to generalise expressions through the introduction of names, and function APPLICATION to evaluate generalised expressions by giving names particular values. (1) Only abstraction and application are needed to develop representations for arbitary programming language constructs. Thus L-calculus as a universal machine code (2) L-calculus is evaluation order independent. We can investigate implications of different evaluation orders. (3) Well developed proof techniques. (4) Easy to implement. Lambda Expressions ------------------ L-calc is a system for manipulating L expressions. A L-exp may be a NAME to identify an abstraction point, a FUNCTION to introduce an abstraction, or a FUNCTION APPLICATION to specialise an abstraction. ::= || A name is any sequence of non-blank characters. A L-function is an abstraction over a L-expression: ::= L. where: ::= Example: Lx.x Lx.Ly.x Lx.Ly.y Lf.La.(f a) The L (lambda) precedes and introduces a name used for abstraction. The name is the function's BOUND VARIABLE and is similar to a formal parameter in Pascal etc. The "." separates the name from the expression in which abstraction with that name takes place. What follows the "." is the function's BODY. Note that the body may be any L expression, including another function. Example: Lx.x The bound variable is x, the body is x Lx.Ly.x The bound variable is x, the body is Ly.x Lf.La.(f a) The bound variable is f, the body is La.(f a) A function application has the form: ::= ( ) where: ::= ::= Example: (Lx.x La.Lb.b) A function application specialises an abstraction by providing a value for the bound variable. In a function application the function is APPLIED TO the argument expression. Example 1: consider Lx.x the "identity" function. --------- Bound variable is: x Body expression is: x Suppose we apply the identity function to itself: (Lx.x Lx.x) (Lx.x Lx.x) is a function application, with Function expression: Lx.x Argument expression: Lx.x When this application is evaluated, we replace the bound variable in the function expression's body with the argument expression. That is: replace x in the body of Lx.x with the argument Lx.x This gives us Lx.x NOTE: names are not significant. Therefore La.a, Lx.x, and LIveGotToGetOutOfThisPlace.IveGotToGetOutOfThisPlace (if its the last thing I ever do!) are the same thing, namely the identity function. Example 2: Consider the function Ls.(s s) --------- Bound variable: s Body: (s s) which is a function application which has Function expression: s Argument expression: s The function applies its argument to its argument, the "self application" function. (Lx.x Ls.(s s)) is a function application with: Function expression: Lx.x Argument expression: Ls(s s) To evaluate replace the bound variable x with the argument expression Ls.(s s) in the body of Lx.x (namely x) Giving: Ls.(s s) Example 3: (Ls.(s s) Lx.x) is a function application with: --------- Function expression: Ls.(s s) Argument expression: Lx.x To evaluate, replace the bound variable s in the function expression's body (s s) with the argument expression Lx.x Giving: (Lx.x Lx.x) which is again a function application with Function expression: Lx.x Argument expression: Lx.x To evaluate, replace the bound variable x in the function expression's body x with the argument expression Lx.x Giving: Lx.x Example 4: (Ls.(s s) Ls.(s s)) is a function application with: --------- Function expression: Ls.(s s) Argument expression: Ls.(s s) To evaluate, replace the bound variable s in the function expression's body (s s) with the argument expression Ls.(s s) Giving: (Ls.(s s) Ls.(s s)) which is a function application with Function expression: Ls.(s s) Argument expression: Ls.(s s) To evaluate, replace the bound variable s in the function expression's body (s s) with the argument expression Ls.(s s) Giving: (Ls.(s s) Ls.(s s)) which is .......... Example 5: Consider the function Lf.La.(f a), the application function --------- Bound variable: f Body: La.(f a) which is a function, with Bound variable: a with Body: (f a) which is a function application with Function expression: f Argument expression: a ((Lf.La.(f a) Lx.x) Ls.(s s)) is a function application with Function expression: (Lf.La.(f a) Lx.x) Argument expression: Ls.(s s) The function expression (Lf.La(f a) Lx.x) is itself a function application which must be evaluated before we evaluate the total function application ((Lf.La.(f a) Lx.x) Ls.(s s)). Therefore we evaluate first the function application (Lf.La.(f a) Lx.x): Function expression: Lf.La.(f a) Argument expression: Lx.x To evaluate, replace the bound variable f in the function expression's body La.(f a) with the argument expression Lx.x Giving: La.(Lx.x a) We now substitute back into the original function application to give us the new (reduced) function application: (La.(Lx.x a) Ls.(s s)) To evaluate, replace the bound variable a in the function expression's body (Lx.x a) with the argument expression Ls.(s s) Giving: (Lx.x Ls.(s s)) Which is again a function application with Function expression: Lx.x Argument expression: Ls.(s s) To evaluate, replace the bound variable x in the function expression's body x with the argument expression Ls.(s s) Giving: Ls.(s s) More briefly: ((Lf.La.(f a) Lx.x) Ls.(s s)) => (L.a(Lx.x a) Ls.(s s)) => (Lx.x Ls.(s s)) => Ls.(s s) where => is a reduction. Syntactic Sugar --------------- If we remove all the inessential features of a functional programming language we will generally arrive at the lambda calculus. Conversely, many functional languages may be viewed as the lambda calculus with "extra dressing", ie a little bit of sugar to make them more palatable. This has been refered to as "syntatctic sugar" [Landin 1964]. Therefore we might add a wee bit of sugar as follows. Whenever we need the identity function, we have to write down Lx.x, and so on. We might therefore use some identifier for this function, such as I, as follows: I = Lx.x apply = Lf.La(f a) self_apply = Ls.(s s) and so on. Furthermore, as we have seen above, we introduce the notation => to show the result of making a substitution of a bound variable in a function body with the argument expression. This replacement is called a BETA REDUCTION, and the resultant on the rhs of => is a reduced expression, sometimes refered to as a REDEX.