| Sussman and Steele | December 22, 1975 | 14 | Substitution Semantics and Styles |
Section 3: Substitution Semantics and Programming Styles
In the previous section we showed several different SCHEME programs for computing the factorial function. How are they different? We intuitively distinguish recursive from iterative programs, for example, by noting that recursive programs "call themselves" but in the last section we claimed to do iteration with a seemingly recursive program. Experienced programmers "know" that recursion uses up "stack" so a program implemented recursively will run out of stack on a sufficiently large problem. Can we make these ideas more precise? One traditional approach is to model the computation with lambda calculus.
Reviewing the Lambda Calculus
Traditionally language constructs are broken up into two distinct classes: imperative constructs and those with side-effects—such as assignment and go-to; and applicative constructs—those executed for value—such as arithmetic expressions. In addition, compiled languages often require a third class, declarative constructs, but these are provided primarily to guide the compilation process and do not directly affect the semantics of execution, and so will not concern us here.
Lambda calculus is a model for the applicative component of programming languages. It models all non-imperative constructs as applications of functions and specifies the semantics of such expressions by a set of axioms or rewrite rules. One axiom states that a combination, i.e. an expression formed by a function applied to some arguments, is equivalent to the body of that function with the appropriate arguments substituted for the free occurrences of the formal parameters of the function in its body:
((LAMBDA <vars> <body>) <args>) = Subst[<args> <vars> <body>]
Another axiom requires that the meaning of an expression be independent of the names of the formal parameters bound in the expression:
(LAMBDA <vars> <body>) = (LAMBDA <newvars> Subst[<newvars> <vars> <body>]) provided that none of <newvars> appears free in <body>.
These constraints force Subst to be defined in such a way that an important kind of referential transparency is obtained. Besides these "structural" axioms, others are provided which specify the result of certain primitive functions applied to specific arguments. We shall not be concerned with these problems here—we will assume a small reasonable set of primitive functions.
