We will take the doing of lambda calculus in the system to the level of writing one recursive function.
A lambda expression without any free variables is a closed lambda expression or a combinator.
Combinators can have free variables in its sub-expressions. We like combinators, simply because they do not require any external context for their evaluation (there are no free variables to worry about).
Some important combinators.
λx.x (* IDENTITY *)
λx.(x x) (* SELF APPLICATION *)
There is a remark to be made on self-application. We are going to need this in a vital way. But notice that it is available only in type-free systems. In a typed system a function has to be, for example, integer->boolean(ie truth value), but then if you try to apply it to itself you cannot do it because this function can only have integers as arguments not a (integer->boolean). So... you cannot do self-application in most functional programming languages nor in typed lambda-calculus.
λx.λy.λz.(x (y z)) (* COMPOSITION *)
λfirst.λsecond.λargument.(first (second argument))) (* composition, again *)
Although lambda abstractions are always abstractions of only one variable, when it comes to combinators there is the notion of the number of arguments that the combinator expects and this is the number required for it to reduce or unravel fully. For example, composition expects three arguments.
λx.λy.x (* TRUE *)
λfirst.λsecond.first (* true, again *)
You may be a bit puzzled by true and false, but they are designed to work with 'If-then-else' and
they may make more sense when you see it.
λx.λy.y (* FALSE *)
λfirst.λsecond.second (* false, again *)
λx.λy.λz.((x y) z) (* IFTHENELSE *)
λcondition.λthen.λelse.((condition then) else) (* if then else, again *)
We can now see how these fit together. True consumes two arguments and returns the first, false consumes two arguments and returns the second. For example, if you pop true into the condition of if-then-else, you will get back the first argument which is the then. Thus...
(((λcondition.λthen.λelse.((condition then) else ) λfirst.λsecond.first) thenArg) elseArg)
((λthen.λelse.((λfirst.λsecond.first then) else ) thenArg) elseArg)
(λelse.((λfirst.λsecond.first thenArg) else ) elseArg)
((λfirst.λsecond.first thenArg) elseArg)
You should perhaps try these:-
[When you are combining complex expressions, it is probably prudent to use different variables for the lambda expressions (otherwise you could be faced with a number of alpha rewrites to make those variable different and to avoid the capture of free variables).]
a) (((λx.λy.λz.((x y) z) λu.λv.u) hello) goodbye) ⇒ hello (*if-then-else applied to true returning first argument *)
b) (((λx.λy.λz.((x y) z) λu.λv.v) hello) goodbye) ⇒ goodbye (*if-then-else applied to false returning second argument *)
Here is some alternative software to illustrate the same proofs. (Click on the proofline to select it. Click on Rules and choose Rewrite Rules. Select the Rule you would like, Select the subexpression it is to apply to, Click Go).
Video illustrating reduction
[This is a Video, click the Play button to view it..]
As you can see, the writing of lambda expressions can be tricky and it lends itself to error. We can make this slightly easier by allowing in some definitions. Syntactically we are going to permit some characters like 'T', 'F', '⊃'. These will be constants (so they are well formed on their own, can be part of applications, or the scope of lambda abstractions, but cannot be the variable in a lambda abstraction). Then they will be used as plain abbreviations for longer expressions so, for example, we have
T=df. λx.λy.x (*TRUE*)
F=df. λx.λy.y (*FALSE*)
C=df. λx.λy.λz.((x y) z) (*IF-THEN-ELSE*)
⊃=df. λx.λy.λz.((x y) z) (*IF-THEN-ELSE*)
Then these abbreviations will be treated in the software just as Rewrite Rules. So, for example, if an expression has T in it, that T can be rewritten to λx.λy.x . (And, equally, any (sub)expression with the form λx.λy.x can be rewritten to T.)
'IF-THEN-ELSE has two abbreviations, either the letter 'C' (conditional), or the logical symbol '⊃'. Most readers will be familiar with ordinary propositional or predicate logic in which the symbol '⊃' is used for 'IF-THEN' as in (A⊃B). This logical IF-THEN is infix binary; that is, it takes two arguments and comes between those arguments. When it is used here in lambda calculus, it is going to be prefix and, conceptually at least, ternary; that is, it takes three arguments and comes before those arguments. For example, (((⊃ T) hello) goodbye). If the reader prefers to use 'C' as the abbreviation, that is fine too.
You should perhaps try these:-
a) (((⊃ T) hello) goodbye)⇒ hello (*if-then-else applied to true returning first argument *)
b) (((C F) hello) goodbye)⇒ goodbye (*if-then-else applied to false returning second argument *)
( Select line, select rewrite rule, expand definitions, reduce. Avoid expanding definitions until you need to.)