Applicative Order and Normal Order ---------------------------------- There are two approaches to evaluating function applications. Both of these approaches have one thing in common, namely they both ultimately evaluate the function expression to deliver a result. These two approaches are as follows: (a) all occurrences of the function expression's bound variable, in the function's body is replaced by THE VALUE OF THE ARGUMENT EXPRESSION. This is called "APPLICATIVE ORDER". (b) all occurrences of the function expression's bound variable, in the function's body is replaced by THE UNEVALUATED ARGUMENT EXPRESSION. This is called "NORMAL ORDER". Applicative order is the same as call by value, that is the arguments are evaluated before they are passed to a function. This is what happens in ml. Normal order is the same as "call by name" in Pascal, and may be considered as "lazy evaluation". So far we have assumed normal order. This is in fact why we could not define the lambda function Ls.(s s) in ml. To do so we require normal order, whereas ml exploits applicative order. It (ml) recognises that Ls.(s s) will not terminate and therefore disallows it. Bound and Free Variables ------------------------ Consider the function application: (Lf.(f Lx.x) Ls.(s s)) => (Ls.(s s) Lx.x) => (Lx.x Lx.x) => Lx.x We previously stated that Lx.x is the same as La.a which is the same as Lf.f So we should be able to replace Lx.x with Lf.f in the above function application: (Lf.(f Lf.f) Ls.(s s)) This should give the same result. The bound variable f should be replaced with the argument expression Ls.(s s). In fact we should replace only the first f in (f Lf.f) but we should not replace the f in the body of Lf.f, as this is a new function expression with a new bound variable, which just happens to have the same name. Given L. refers to the same variable throughout except where another function has that same as its bound variable. References to in the new functions body then corresponds to a new bound variable. A variable is said to be BOUND to occurrences in the body of a function for which it is the bound variable, provided no other functions within the body introduce the same bound variable, otherwise it is said to be FREE. Lf.(f Lx.x) f is bound, x is bound Lf.(f x) f is bound, x is free (f Lx.x) f is free, x is bound (f x) f is free, x is free All free occurrences of in are references to the same bound variable introduced by the original function. is in scope in whenever it occurs free, except where another function introduses it in a new scope. All this may sound a little bit too abstract for our liking and we may be more comfortable if we can find a familiar analogue (just as we did with "Lx.x" and "fn x => x"). We might think of L. as a local variable definition in any block structured programming language such as Pascal. Once we have declared a local variable it is accessable to subsequent blocks (begin/end pairs), and might be viewed as a global variable to these subsequent blocks. However, if within one of these subsequent blocks we make another local declaration of a variable with the same name as a variable in an outer block we then use the that local declaration. We might consider GLOBAL = FREE, LOCAL = BOUND, and L. a local declaration of with scope . Basically, we need to enhance BETA REDUCTION with this in mind. Name Clashes and Alpha Conversion --------------------------------- Given the following function application: ((Lf.La.(f a) g) boing) => (La.(g a) boing) => (g boing) Again, we have previously stated that we can consistently change the names of variables within a lambda function without affecting the semantics of that lambda function. For example, La.a and Lx.x are the same, and Lf.f is the same as Lx.x (the identity function I). Therefore we can re-write the above function application, replacing "g" with "a" and hopefully deliver the same result: ((Lf.La.(f a) a) boing) => (La.(a a) boing) => (boing boing) Woops! Something is clearly wrong here. What we should of expected as a result is (a boing) not a (boing boing). What went wrong? Within the inner function La.(f a), f is free but we went and replaced it (via BETA reduction) with a, which is bound in La.(f a). That is, we have created a new occurrence of a bound variable. We can avoid this by renaming (again, remember Lx.x = La.a). A NAME CLASH arises when a BETA reduction places an expression with a free variable in the scope of a bound variable with the same name as that free variable. Consistent renaming removes that clash. This "consistent renaming" is refered to as ALPHA CONVERSION. ETA Reduction ------------- Lx.(f x) is convertible to f iff x is not free in f.