One has to be of an extremely unusual disposition to wish to work in the bare lambda calculus.
What is standard is to extend its expressions by adding various constants, and extend its reduction rules by adding reduction rules under the rubric of delta-reduction rules. These constants are understood to name familiar constants or familiar functions; for example, integers may be added and the function PLUS; then if an expression amounts to a suitable application, for example, PLUS 1 2, then the appropriate delta rule can be brought in to reduce this to 3.
Then, usually, a further extension is made to include local definitions and recursion.
The extensions here are extensions only in convenience. All the underlying theoretical results and theorems still hold. (Well, this should be the case. Actually it should be checked in detail. We will certainly look reasonably closely with local definitions and recursion.)
Constants are typically one of:- 0,1,2,..., ADD, SUB, MUL, DIV, TRUE, FALSE, IF, AND, OR, NOT, CONS, HEAD, TAIL, NIL, NULL, Y, and perhaps others.
The delta reduction rules are just the standard rules for evaluating the predefined functions, for example, AND TRUE TRUE reduces to TRUE. (Some questions do arise concerning reduction order here but we will avoid these at present.)
It is fairly standard to allow in local definitions and recursion.
The first is achieved by the construction
let <var> = <expr1> in <expr>
for example, let x = 2 in (λy.(+ y x) 3) . (Notice here we are allowing in 'multiple variable' functions eg (+ y x) which really just 'uncurries' ((+ y) x).)
We want to show and need to show that constructions like this do not add anything to the calculus-- that they are just abbreviations for standard lambda calculus constructions.
The simple let construction is merely an abbreviation for (λ<var>.<expr> <expr1>) so the example is an abbreviation of (λx.λy.((+ y x) 3 ) 2)
Some formulations allow for multiple 'simultaneous' let's, thus:-
let <var1> = <exprn+1> and <var2> = <exprn+2> and... <varn> = <expr2n> and in <expr>
for example, let x = 2 and y=3 in (+ y x)
There is a question here of the semantics of this. Were these multiple let's to be sequential we could deal with them by nesting the simple let's for example, let x = 2 and y=3 in (+ y x) amounts to let x = 2 in let y=3 in (+ y x) and this translates to (λx.(λy.(+ y x) 3 ) 2).
However, maybe you'd want multiple lets to be simultaneous. A trick is needed to do this, and it is a trick that is used elsewhere so it is worth explaining.
The problem we have to solve is this. The lambda calculus uses one variable at a time-- you abstract over one variable, you apply a one variable function to exactly one argument.... Yet sometimes we find ourselves wishing to deal with several distinct items all at once. In effect, we want to have a function of several variables, and apply this function to several arguments all at once. (In a way, this problem is the converse of currying.)
The solution is to form the multiple items into one single sequence, or list, or tuple -- so that you refer to individual items as being, say, third-in-sequence -- then you do the lambda abstraction over the single sequence.
This technique is known as tupling. You need constructor functions for tuples. One of these will make, for example, two-element tuples out of two single elements. You need accessor functions to access the individual elements in the tuple. (We have done this in the bare calculus, with the PAIR constructor and also with lists.) Then, for example, an expression like
let x = 2 and y=3 in (+ y x)
can be translated into a simple let. First a tuple will be formed out of 2 and 3, let us write this {2,3} and a tuple will be formed out of x and y, {x,y}, say. Then the entire expression can be written as a simple let in terms of the tuples and their accessors
let x = 2 and y=3 in (+ y x) becomes
let {x,y}={2,3} in (+ (first {x,y}) second {x,y}) and this becomes
(λtup.(+ (first tup) (second tup) ) {2,3}) and this will reduce to
(+ first{2,3} second{2,3}) => (+ 2 3) => 5
Let us just run over an example to show that our translations capture the different semantics .
Say x enters with the value 3 and consider let x = 2 and y=x in (+ y x). Under the sequential translation we get
(λx.(λy.(+ y x) x ) 2) which reduces to (λy.(+ y 2) 2 )) and further to 4
Under the parallel translation we get
(λtup.(+ (first tup) (second tup) ) {2,x}) which reduces to (+ 2 x) in env {x->3} and further to 5
It is also common to permit a recursive version of local definition
letrec <var> = <expr1> in <expr>
for example, let length = λlist.(IF (NULL list) 0 (+ 1 length (tail list)) in length (CONS 1 NIL)
Here we have the definition of a recursive function. Any occurrences of <var> in <expr1> in the definition mean <expr1> itself, the occurrences have to be unravelled out recursively-- let alone what happens down the right hand end. We know how to do this self-reference-- just abstract over the name and apply the fixpoint combinator, this gives us (Y λ<var>.(<expr1>)). So we can translate a simple letrec into a simple let
letrec <var> = <expr1> in <expr> abbreviates let <var> = (Y λ<var>.<expr1>) in <expr>
Then we just have to ensure that this is substituted in <expr> down the right-hand end, and this is done by the standard translation of let.
letrec <var> = <expr1> in <expr> translates or abbreviates (λ<var>.<expr> (Y λ<var>.(<expr1>)))
The final case of this is mutual recursion.
letrec <var1> = <exprn+1> and <var2> = <exprn+2> and... <varn> = <expr2n> in <expr>
for example
letrec f = ln(IF (EQ0 n) 0 (g n)) and g = ln(IF (EQ0 n) (f n) n ]) in f[7]
We know how to do this, although it is fiddly. We form a tuple of the right hand sides of the definitions; we refer to the defined names by the indices of their definitions in the tuple; we substitute these tuple-indices for the names throughout the tuple; we abstract over the tuple; and we apply the fixpoint combinator to the abstraction. We form a tuple of the left hand sides of the definitions. Then the whole multiple definition letrec becomes the simple let <lefttuple>= Y ltuple(<righttuple>) in <expr> and this abbreviates l<lefttuple>(<expr> (Y l<lefttuple>(<righttuple>))
For example, consider letrec f = (...g...) and g = (...f...) in f 7 where an expression like (... g...) is used to mean an expression containing a reference to g. First, form a tuple of the left hand sides of the definitions and the right hand sides:- {f,g} and {(...g...),(...f...)}. Then remove the names from the right hand tuple, using instead indices, {(...second[tuple]...),(...first[tuple]..)}. Abstract over this and apply the fixpoint combinator (Y λ<tuple>. (<(...second tuple ...),(...first tuple ..)> )) then put the lot together into a simple let.
let {f,g} = (Y λtuple ({(...second tuple ...),(...first tuple ..)} )]) in f 7
and we are familiar with the translation of a simple let.
Now we are in a position to appreciate what an entire functional program is, in a modern functional programming language. In effect it is just a letrec, with possibly a substantial number of recursive functions, followed by an expression to evaluate.
letrec
<var1> = <exprn+1>
and <var2> = <exprn+2>
and... <varn> = <expr2n>in <expr>