Structure Sharing

This was the first good idea that Bob Boyer and I had together. It developed in the Metamathematics Unit (eventually to become the Department of Computational Logic) at the University of Edinburgh, in 1971.

Structure sharing concerns a way to represent derived clauses in a resolution theorem prover. Roughly speaking, a derived clause is obtained from two parent clauses by substituting certain terms for variables, deleting certain elements of the parents, and unioning together the results. Until structure sharing came along, this was generally implemented quite literally and hence involved large amounts of copying (to perform the instantiation and deletion).

We realized that the derived clause could be represented succinctly by a record pointing to the two parents, the substitution, and an indication of which elements were to be deleted. In essence, a derived clause was represented by its derivation.

We then implemented efficiently the fundamental algorithms of resolution on this data structure, including renaming (or ``standardizing apart''), unification, resolution, factoring, and subsumption.

If one regards a resolution engine as executing a program in the predicate calculus (as Pat Hayes and Bob Kowalski were contemporaneously doing next door to us), then structure sharing is analogous to implementing procedure call via a stack of bindings rather than by literally substituting actuals for formals. This analogy gave momentum to the view that eventually led to Prolog. In addition, the basic idea in structure sharing is evident in the Warren Abstract Machine that underlies modern Prolog engines.

In fact, my dissertation actually presents an early version of a Prolog-like programming language called Baroque. See Chapter 6 (page 68) of the dissertation. The Baroque expression of the Lisp function LENGTH is

LEN1: (LENGTH NIL) -> 0;
LEN2: (LENGTH (CONS X Y)) -> Z
      WHERE
      (LENGTH Y) -> U;
      (ADD U 1) -> Z;
      END;

As said on page 71, ``This language is called BAROQUE. It has several properties not found in traditional programming languages. Among these are: pattern directed invocation and return, backtracking, and the ability to run functions "backwards" (from results to arguments).''

J.A. Robinson, inventor of unification and resolution, was a frequent visitor to Edinburgh and so liked our idea he awarded it the 1971 Programming Prize on behalf of the newly formed Foundation for the Advancement of Computational Logic by the Taking Out of Fingers.

There is a rather odd connection between structure sharing and the first modern WYSIWYG text editor, Bravo, and its successor, Microsoft Word.

For details of structure sharing, see

The Sharing of Structure in Theorem-proving Programs, with R.S. Boyer. In B. Meltzer and D. Michie (eds), Machine Intelligence 7. Edinburgh University Press, 1972, pp. 101-116.
Computational Logic: Structure Sharing and Proof of Program Properties. PhD Thesis, Department of Computational Logic,University of Edinburgh, 1973. (16 MB scanned pdf)

[Best Ideas] [Publications] [Research] [Home]