| Sussman and Steele | December 22, 1975 | 15 | Substitution Semantics and Styles |
Recursive programs
Now, let's see how lambda calculus may be used (informally) to model a computation. Consider the standard definition of the factorial function:
(DEFINE FACT (LAMBDA (N) (IF (= N 0) 1 (* N (FACT (- M 1))))))
We are being very informal—lambda calculus as presented by [Church] does not include such constructs as DEFINE, IF, or =, *, or even 1! The "usual" lambda calculus construct for defining recursive functions is a rather obscure object called the "fixed-point" operator. We have been lax to avoid the hassle of "rigor mortis" in this tutorial paper. Similarly, IF is the SCHEME conditional construct we will use for convenience, it reduces to its second or third argument depending on whether the first reduces to TRUE or FALSE. The objects *, =, 0, 1, etc. may be thought of as abbreviations for complex lambda expressions (such as Church numerals) whose details we are not interested in. On the other hand, we may think of them as primitive expressions, defined by additional axioms; this viewpoint leads to practical interpreter implementations.
Now let's reduce the expression (FACT 3). We will perform the expression reductions, except for the IF primitive, in Applicative Order (call by value), though this is not necessary, as we will discuss later. We display a "trace" of the substitutions:
=> (FACT 3) => (IF (- 3 0) 1 (* 3 (FACT (- 3 1)))) => (* 3 (FACT (- 3 1))) => (* 3 (FACT 2)) => (* 3 (IF (= 2 0) 1 (* 2 (FACT (- 2 1))))) => (* 3 (* 2 (FACT (- 2 1)))) => (* 3 (* 2 (FACT 1))) => (* 3 (* 2 (IF (= 1 0) 1 (* 1 (FACT (- 1 1)))))) => (* 3 (* 2 (* 1 (FACT (- 1 1))))) => (* 3 (* 2 (* 1 (FACT 0)))) => (* 3 (* 2 (* 1 (IF (= 0 0) 1 (* 0 (FACT (- 0 1))))))) => (* 3 (* 2 (* 1 1))) => (* 3 (* 2 1)) => (* 3 2) => 6
You will note that we have calculated (fact 3) by a process wherein each expression is replaced by an expression which is provably equivalent to it via an axiom or which is produced by application of a primitive function.
