# 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;