Quick question regarding indirection cells...

[David Lester]

> I suspect indirection nodes are treated in Wadsworth's original
> thesis on the subject.  There are few copies available, but the
> Oxford library has the original, perhaps you can ask someone there
> to check for you.  -- P

I'm not so sure that you'll find a mention there. The reason is that
Chris was dealing with the lambda calculus and not some more general
functional programming language.

You have already mentioned one reason why indirections may be required
(copied node is larger than redex node), but there is a second reason:
the easy and correct implementation of letrec. There is a subtle
footnote (or aside) in Johnsson and Augustssons' papers to the effect
that the order in which the cases of a letrec are compiled matters.
If you get it wrong then (with their copying update instruction) you
copy HOLE nodes, rather than the correct nodes.

Of course, for the lambda calculus, there is no letrec's and hence all
graphs are acyclic; furthermore for the pure lambda calculus there are
no constructors (and hence none that is larger than an application
node).

A more plausible source for this would be David Turner's work, where I
am fairly certain he mentions the knot-tying Y combinator (the lambda
calculus equivalent in Wadsworth obviously isn't knot-tying). From
memory, there is little mention of indirection nodes in that paper,
but without something like this it is difficult to make the whole
thing work (look carefully at the compilation of letrec's in Turner's
papers).

---

As an aside, the reason that I used indirection nodes was to maintain a
(sort-of) graph isomorphism. Two interpreter states are isomorphic if their
indirection-node-elided and garbage-collected graphs are isomorphic.

Consider the reduction of Y f:

G/M style (copying update):


             n0:@
               / \
              Y   f

becomes:

             n0:@
               / \
              /   \
             /    /
            /    /
            |n1:@--+
            \  / \_/
              f

whereas, with indirection nodes we get

             n0:^
                 \
                  \
                  /
                 /
             n1:@--+
               / \_/
              f

Notice that we are going to need a much more complicated notion of
isomorphism definition to make the G/M style graph equivalent to that
produced by an interpreter than the second case, where we need only to
eliminate the indirections.

The suggestion in Chapter 6 of my thesis was that if we exchange the
roles of n0 and n1, (i.e. n0 is now an application node and n1 the
indirection) then we have eliminated the possibility of chains of
indirection nodes accumulating.

But, as the supervisor for this thesis, you knew that didn't you? :-)

---

In a fit of insanity I suggested to one of my PhD students that he
might like to test his theorem prover on the proof given in Chapter 3
of my thesis. He concluded that Lemmata 3.18 and 3.19 should have been
proved mutually inductively (when they are then provably correct)
rather than individually (when they can't be proved correct). The rest
of the theorems in the Chapter 3 were correct. See [1].


---
David Lester.

[1] Sava Mintchev and David Lester, "Towards Machine--checked Compiler
    Correctness for Higher-order Pure Functional Languages", Proceedings
    of the 8th Annual Conference of the European Association for Computer
    Science Logic, Kazimierz, Poland, LNCS 933(369--381) Springer-Verlag,
    1995.