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.