Case Study: How to build your own stack frames.

      Whenever possible, one should always define the abstract architecture
of the machine at a high-level first. After doing so, you will then
convert this description rigorously into an implementation. In this
particular case, the implementation will be stack-based, so the stack
operators will be seen to emerge systematically from the corresponding
recursive definitions.


      So in reality, you *don't* define your stack machine at the outset. You
*derive* it. This is the approach that is guaranteed to give you the most
reliable (and bug-free) results: because the logical proof of correctness
and the design process are one and the same!


      The case in point cited below is a revision of an article completely
specifying the development of the architecture of the SECD-2 and SEQCD
machines. The premise is the question: "what if Landin had derived his
SECD machine rigorously instead of coming up with a design out of thin
air?" The answer offered, SECD-2, is able to process lambda expressions
in applicative order (one can also define a "normal order" version of SECD-2,
and this will lead to a combinator reduction architecture I call COM). The
SEQCD machine is an extension that is able to handle an extension of the
Lambda Calculus which comprises the rational infinite lambda terms. In
this extended lambda calculus one can directly represent imperative constructs
such as the goto statement or while loop. Amazingly, even though it is not
specifically designed to do so, the SEQCD machine will process imperative
language constructs exactly like you'd expect an ordinary computer to do,
yet it handles lambda expressions perfectly well. The imperative behavior
is completely emergent and was pretty much an unexpected feature.


The front end to the extended lambda calculus (the Regular Infinite
Lambda Calculus) is basically a functional language with imperative
syntax. As of yet it has not been implemented and only specified in
outline. Its name is JOLT.


(1) What If
      One will frequently note in the literature where abstract machines are
defined, but almost invariably where the definitions appear to be pulled out
of the hat. This seems like a rather counter-productive way to do things.
Not only do you have the labor of actually pulling machine out of the hat, but
then you have to establish a link to some invariant properties and then go
through the process of proving the machine correct. And half the time, it's
not correct.


      One notices, for instance, that in Werner Kluge's "The Organization of
Reduction, Data Flow, and Control Flow Systems" the author goes through all
the trouble of formally defining normal and applicative order reduction and
then just basically throws it all away and outlines a set of architectures
that might as well have just been concocted. The irony is that the entire
latter half of the book is unnecessary. Abstract machine architectures for
normal order reduction and applicative order reduction can be rigorously
derived from the corresponding definitions presented in that book.


      One can see the contrast of the two approaches in the specification of
the SECD and CAML machines. Whereas the latter is actually *derived*
systematically from a definition of beta reduction, the former is not
linked to any such definition. The result is pretty obvious: SECD doesn't
work.


      The better way of doing things is not to even think about machines at
all in the beginning, but to think about formal definitions instead. A
formal definition for any kind of non-trivial system will invariably be
recursive. The process of specifying the abstract machine, then, comes
down to nothing more than eliminating the recursion from the definition.
In the process, all three problems mentioned above are solved by the
time-honored method of rendering them irrelevant: (1) the machine design
is not concocted but is derived rigorously, (2) the linkage to a specification
is automatic, and (3) the proof of correctness is the derivation of the
machine itself!


      What if SECD has been designed rigorously? I will also ask the related
question: what if the correspondence between imperative and functional
languages (a' la Landin's 1965 approach) had been completed? As it turns out,
both questions have the same answer -- the SEQCD Machine.


      The SEQCD Machine is just a minor extension of the SECD-2 machine, which is
about to be described below. Because of the way it handles its environment,
it turns out to be an entirely trivial process to extend SECD-2 to an
applicative order machine for processing Regular Infinite lambda expressions
in such a way that the result will miraculously behave just like a processor
for an imperative language. This behavior is totally emergent, there's
nothing explicitly imperative in the SEQCD machine.


      So what's described here is the precursor: SECD-2.


(2) The SECD-2 Machine
      You may want to consult the reference: Werner Kluge's "The Organization of
Reduction, Data Flow, and Control Flow Systems". A definition for applicative
order evaluation can be found on p.114 (I've modified the notation slightly).


      For lambda terms, we'll use the abstract syntax:
                            Term -> \Var . Term
                                      -> Term Term
                                      -> Var


Here, "\" is being used to denote the lambda operator because it looks like a
lambda.


      Define the partial function:


                      [T]: the result of reducing T in applicative order


and in the following, let x denote a variable, and T, T' and U arbitrary terms.
Then
                  [x] = x
                  [\x.T] = \x.[T]
                  [(\x.T) U] = { \x.T, [U] }
                  [T U] = { [T], [U] }, T not a lambda term


where { f, x } is an auxilliary procedure defined as follows:


                  { \x.T, U } = [x <- U, T],
                  { T, U } = T U, T not a lambda term


where (x <- U, T) is my notation for denoting the result of substituting U
for all free occurrences of x in the term T. The substitution operator can be
defined recursively as follows:


                            (x <- U, y) = U if y = x
                                                              y otherwise
                            (x <- U, \y.T) = \z.(x <- U, y <- z, T)
                            (x <- U, T T') = (x <- U, T) (x <- U, T')


where z is an otherwise unused variable introduced, as usual, to help prevent
accidental captures of any free variable, y, in the term U by the \y operator.


      These two sets of rules can be joined into one. Define a substitution
environment as a list of parallel substitutions (i.e. as a function mapping
variables to terms). Define the following:


                                  I ---------- the empty environment (the identity function)
                                  E, x <- U -- the environment altered by binding x to U.


As functions, these environments have the properties:


                                I(x) = x for all variables x.
                                (E,x<-U)(y) = U if y is the variable x.
                                                        = E(y) for all other variables y.


Let (E, T) denote the result of applying the substitutions in the environment
E to all the variables in term T. Then the following apply:


                      (E, x) = E(x)
                      (E, \x.T) = \z.(E, x <- z, T)
                      (E, TU) = (E, T) (E, U)


Noting that z is an otherwise unused variable, this definition follows
directly from the definition of the substitution operator above.


      Combining this with the reduction process [T] defined above, use the
notation:
                                          [E, T] to denote [(E, T)].


In the following we will restrict environments to those that bind variables
only to terms already reduced to normal form.


Then it follows that:


                [E, x] = [E(x)] = E(x)
                [E, \x.T] = [\z.(E,x<-z,T)]
                                    = \z. [(E,x<-z), T]


                [E, (\x.T) U] = [\z.(E,x<-z,T) (E,U)]
                                            = { \z.(E,x<-z,T), [E,U] }
                [E, TU] = [(E,T) (E,U)]
                                            = { [E,T], [E,U] } T not a lambda term
                where
                      { \x.T, U } = [(I, x <- U), T],
                      { T, U } = T U, T not a lambda term


Note that


              [E, (\x.T) U] = { \z.(E,x<-z,T), [E,U] }
                                          = [ (I, z<-[E,U], E, x<-z, T) ]
                                          = [(E, x<-[E,U]), T]


Thus, we arrive at a combined definition:


                [S0] [T] = [I, T]
                where
                      [S1] [E, x] = E(x)
                      [S2] [E, \x.T] = \z.[(E,x<-z), T]
                      [S3a] [E, (\x.T) U] = [(E, x<-[E,U]), T]
                      [S3b] [E, TU] = { [E,T], [E,U] } T not a lambda term
                      where
                            [S4a] { \x.T, U } = [(I, x <- U), T],
                            [S4b] { T, U } = T U, T not a lambda term


      It's not hard to derive an abstract machine from this. This machine
will be based on the following inductive assertions:


                          s, E, C, D -> ... -> e, E', [E,C], D
                          t, E, C, D -> ... -> f, E, [E,C], D


and will therefore have 4 states. The start state, s, will be an optimized
state that evaluates an expression while letting the environment go. The
end state, e, is the corresponding end state. On the other hand, the start
state, t, will evaluate an expression taking care to preserve the environment
all the way to the corresponding end state, f. Our task is to make use of
the t->f in the right places to avoid the need to save copies of the
environment as much as possible. It turns out that there will only be one
place where it remains necessary to copy the whole environment and it closely
corresponds to the call-return operation of imperative languages. In all
other places we only need to save single variables. One should note that


                                        E, x<-U, x<-E(x) = E, x<-E(x) = E


so that the operation updating x is reversible as long as we retain the
original
state of the variable x.


      Thus, to evaluate an expression, C, we merely need to carry out the process:


                C --> s, I, C, [] -> ... -> e, E', [I,C], [] --> [I,C] = [C].


The dump, D, is tentatively identified as a hetergeneous tagged stack whose
exact format will be specified as the least that is required to make the
inductive proof of the assertions above work. We'll derive it by actually
carrying out the proof first. That may seem odd -- proving the consistency
of something whose creation is generated by the proof itself -- but that's
the perfect way to do things: it's a form of bootstrapping. The tagged
stack will be represented using list notation. Inductive steps will be
indicated by an ellipsis (...). Other steps will be labeled by the rules
that they will come to denote.


                R0 R4
[S0] T --> s, I, T, [] ... e, I, [I,T], [] --> [T]


                                R1a
[S1] s, E, x, D --> e, E, E(x), D
                                R1b
          t, E, x, D --> f, E, E(x), D


                                      R2a
[S2] s, E, \x.T, D --> s, (E,x<-z), T, 1:z:D R5a
                                      ... e, E', [E,x<-z,T], 1:z:D --> e, E', \z.[E,x<-z,T], D


                                      R2b
          t, E, \x.T, D --> t, (E,x<-z), T, 2:x:E(x):1:z:D
                                      ... f, (E,x<-z), [E,x<-z,T], 2:x:E(x):1:z:D


                                      R6 R5b
                                      --> f, E, [E,x<-z,T], 1:z:D --> f, E, \z.[E,x<-z,T], D


                                  R3a
[S3] s, E, TU, D --> t, E, U, 3:T:D ... f, E, [E,U], 3:T:D


                                  R3b
          t, E, TU, D --> t, E, U, 4:T:D ... f, E, [E,U], 4:T:D


                                                        R7a
[S3a] f, E, [E,U], 3:\x.T:D --> s, (E,x<-[E,U]), T, D
                                                        ... e, E', [E,x<-[E,U],T), D


                                                        R8a
            f, E, [E,U], 4:\x.T:D --> t, (E,x<-[E,U]), T, 2:x:E(x):D
                                                        ... f, (E,x<-[E,U]), [E,x<-[E,U],T], 2:x:E(x):D
                                                        R6
                                                        --> f, E, [E,x<-[E,U],T], D


                                                  R7b
[S3b] f, E, [E,U], 3:T:D --> s, E, T, 5:[E,U]:D T not a lambda term
                                                  ... e, E', [E,T], 5:[E,U]:D
                                                  ... e, E'', {[E,T], [E,U]}, D


                                                  R8b
            f, E, [E,U], 4:T:D --> t, E, T, 5:[E,U]:D
                                                  ... f, E, [E,T], 5:[E,U]:D
                                                  ... f, E, {[E,T], [E,U]}:D


We have inductively asserted that


                e, E, T', 5:U':D -> ... -> e, E', { T', U' }, D
and f, E, T', 5:U':D -> ... -> f, E, { T', U' }, D


In order to fill out this part of the induction, we need to look at the
respective cases S4a and S4b.


                                                R9a
[S4a] e, E, \x.T, 5:U:D --> s, (I,x<-U), T, D ... e, E', [I,x<-U,T], D


                                                R10a
            f, E, \x.T, 5:U:D --> s, (I,x<-U), T, 6:E:D R11
                                                ... e, E', [I,x<-U,T], 6:E:D --> f, E, [I,x<-U,T], D


                                          R9b
[S4b] e, E, T, 5:U:D --> e, E, TU, D T not a lambda term


                                          R10b
            f, E, T, 5:U:D --> f, E, TU, D




      Collecting these rules together, we get the following specification


R0 initialize: T --> s, I, T, []


R1a s, E, x, D --> e, E, E(x), D
R1b t, E, x, D --> f, E, E(x), D


R2a s, E, \x.T, D --> s, (E,x<-z), T, 1:z:D
R2b t, E, \x.T, D --> t, (E,x<-z), T, 2:x:E(x):1:z:D


R3a s, E, T U, D --> t, E, U, 3:T:D
R3b t, E, T U, D --> t, E, U, 4:T:D


R4 e, E, T, [] --> T and halt


R5a e, E, T, 1:z:D --> e, E, \z.T, D
R5b f, E, T, 1:z:D --> f, E, \z.T, D


R6 f, E, T, 2:x:U:D --> f, (E,x<-U), T, D


R7a f, E, U, 3:\x.T:D --> s, (E,x<-U), T, D
R7b f, E, U, 3:T:D --> s, E, T, 5:U:D T not a lambda term


R8a f, E, U, 4:\x.T:D --> t, (E,x<-U), T, 2:x:E(x):D
R8b f, E, U, 4:T:D --> t, E, T, 5:U:D T not a lambda term


R9a e, E, \x.T, 5:U:D --> s, (I,x<-U), T, D
R9b e, E, T, 5:U:D --> e, E, T U, D T not a lambda term


R10a f, E, \x.T, 5:U:D --> s, (I,x<-U), T, 6:E:D
R10b f, E, T, 5:U:D --> f, E, T U, D T not a lambda term


R11 e, E', T, 6:E:D --> f, E, T, D


      From this, we can directly read off the struture of the tagged stack. It
consists of a list of records in the following formats:


                                              1 z
                                              2 x U
                                              3 T
                                              4 T
                                              5 U
                                              6 E


where T is an unevaluated term, U a term in normal form, x a variable, z
a fresh variable, and E an environment.


      As an interesting exercise to test the robustness of the approach, let's
add in an extra class of terms and clause in the definition of [T]: the
conditional. We'll use the following C-like syntax:


                            Term -> Term? Term: Term


      To evaluate C? T: F the conditional C will first be reduced to normal form.
If it is zero, then F will be reduced and T discarded, else T will be reduced
and F discarded. Formally, this can be represented by the definition:


                                [C? T: F] = if([C], T, F)
                                where
                                      if(0, T, F) = [F]
                                      if(X, T, F) = [T] otherwise


Combining this with the substitution operation we get the following result:


                      [E, (C? T: F)] = [(E,C)? (E,T): (E,F)]
                                                    = if([E,C], (E, T), (E, F))


Defining IF(X, E, T, F) = if(X, (E, T), (E, F)), we get the following result


            [S5] [E, (C? T: F)] = IF([E, C], E, T, F)
                      where
            [S6a] IF(0, E, T, F) = [E, F]
            [S6b] IF(X, E, T, F) = [E, T] otherwise


      From this, we may add the following items to the inductive derivation


                                                R12a
[S5] s, E, (C? T: F), D --> t, E, C, 7:T:F:D
                                                ... f, E, [E,C], 7:T:F:D


                                                R12b
          t, E, (C? T: F), D --> t, E, C, 8:T:F:D
                                                ... f, E, [E,C], 8:T:F:D


                                              R13a
[S6a] f, E, 0, 7:T:F:D --> s, E, F, D ... e, E', [E,F], D


                                              R14a
            f, E, 0, 8:T:F:D --> t, E, F, D ... f, E, [E,F], D


                                              R13b
[S6b] f, E, X, 7:T:F:D --> s, E, T, D ... e, E', [E,T], D (X not 0)


                                              R14b
            f, E, X, 8:T:F:D --> t, E, T, D ... f, E, [E,T], D (X not 0)


This leads to the following additions:


R12a s, E, (C? T: F), D --> t, E, C, 7:T:F:D
R12b t, E, (C? T: F), D --> t, E, C, 8:T:F:D


R13a f, E, 0, 7:T:F:D --> s, E, F, D
R13b f, E, X, 7:T:F:D --> s, E, T, D (X not 0)


R14a f, E, 0, 8:T:F:D --> t, E, F, D
R14b f, E, X, 8:T:F:D --> t, E, T, D (X not 0)


      This results in the addition of two more types of stack records of the
form:
                                                    7 T F
                                                    8 T F


(3) The SEQCD Machine
      Where does the Q in SEQCD come in? Well, this is the part where we
deal with Regular Infinite lambda expressions. A Regular Infinite
expression (of any kind) will be defined as an infinite expression which
contains a finite number of isomorphically distinct subterms. An example
is the following expression


                  X = 0; Y = 1;
                        X < 3? (
                            X = X + 1; Y = Y * 2;
                                  X < 3? (
                                        X = X + 1; Y = Y * 2;
                                              X < 3? (
                                                  ...
                                              ): Y
                                  ): Y
                        ): Y


with the following notations:


                          X = U; T <--> (\X.T) U
                          X + Y <--> + X Y
                          etc.


      If we allow subexpressions to be labeled and use "goto Q" to denote an
occurrence of the subexpression labeled by Q, we can write the expression
above more succinctly as:


                            X = 0; Y = 1; goto Q;
                      Q: X < 3? ( X = X + 1; Y = Y * 2; goto Q; }: Y


In two short paragraphs we've established a convention that's literally
pulled an imperative language out of the hat! This, then, will be the
notation we'll use to represent Regular Infinite Lambda expressions.
Let's go one step further and add the following notation:


                          while E S Q <--> x: E? S': Q


where S is an expression with a "hole" in it and S' the result of inserting
a "goto x" in that hole. Thus, the above expression can be represented
as:


                      X = 0; Y = 1;
                      while (X < 3) (
                            X = X + 1; Y = Y * 2;
                      )
                      Y


where the "hole" is made more explicit as:


                                          X = X + 1; Y = Y * 2; ().


One may also add in the convenient C-like labels:


                                  break and continue.


      A Regular Infinite lambda expression may therefore be represented as
a set of labeled expressions:


                                              E0
                                          q1: E1
                                          ...
                                          qn: En


where E0 is the entire expression. If such an expression will be denoted
Q, then let the subexpression corresponding to qn be denoted Q(qn). The
main subexpression, E0, will be represented by Q(0).


      It's trivial to extend the abstract machine described previously to allow
it to process these kinds of expressions. The machine will have the following
configuration:
                                                          S, E, Q, C, D


where S is the current state (S = s, t, e, or f), E the current environment,
Q the regular infinite expression undergoing evaluation, C the current
subexpression. and D the dump.


      The initialization rule is modified to the following:


R0 initialize: Q --> s, I, Q, Q(0), []


We'll add in the following rule for the goto:


R15a s, E, Q, goto x, D --> s, E, Q, Q(x), D
R15b t, E, Q, goto x, D --> t, E, Q, Q(x), D


Every other rule is amended by adding in the Q component. That's all that's
required.


      Let's see how this abstract machine operates on the expression in the
example above. Written explicitly in lambda notation it takes on the form:


                    Q = (\x. (\y.goto q1) 1) 0
                            q1: (< x 3)? (\x. (\y.goto q1) (* y 2)) (+ x 1): y


      Rigorously applying the rules defining the abstract machine we get:


R0 Q --> s, I, Q, (\x. (\y.goto q1) 1) 0, []
R3a --> t, I, Q, 0, [3, \x.((\y.goto q1) 1)]
R1b --> f, I, Q, 0, [3, \x.((\y.goto q1) 1)]
R7a --> s, (I,x<-0), Q, (\y.goto q1) 1]


R3a,R1b,R7a --> s (I,x<-0,y<-1), Q, goto q1, []


R15a --> s, (I,x<-0,y<-1), Q, (< x 3)? ..., []
R12a --> t, (I,x<-0,y<-1), Q, < x 3, [7:...:y]
R3b,R1b,R8b,
R3b,R1b,R8b,
R1b,R10b,R10b --> f, (1,x<-0,y<-1), Q, 1, [7:...:y]


R13b --> s, (1,x<-0,y<-1), Q, (\x. (\y.goto q1) (* y 2)) (+ x 1), []


As an exercise, you may want to trace through the rules and prove that this
will lead to the configutations


  --> ... --> s, (I,x<-1,y<-2), Q, (\x. (\y.goto q1) (* y 2)) (+ x 1), []
  --> ... --> s, (I,x<-2,y<-4), Q, (\x. (\y.goto q1) (* y 2)) (+ x 1), []
  --> ... --> s, (I,x<-3,y<-8), Q, y, []
R1a --> e, (I,x<-3,y<-8), Q, 8, []
R4 --> 8


      Note that


                            (I, x<-1, y<-2), x<-2 = (I, x<-2, y<-2)


since each update to the environment overwrites the previous one.


      This machine had created its own variables for the loop, maintained
them in a way completely consistent with the imperative reading of the
while loop above, and then discarded them all without being explicitly told to
do so.


      Thus an intimate connection between imperative languages and functional
languages, completely refuting Backus's assertions about the intractibility
of imperative languages, is at last revealed.


--

Return to the comp.compilers page.
Search the comp.compilers archives again.