As computers are used more and more in safety-critical systems, such as nuclear reactor control and fly-by-wire aircraft, and as the cost of maintaining large suites of software rises, there is an increasing appeal for techniques to specify what a system is supposed to do and to verify that the software code satisfies this specification. In essence the verification step amounts to proving theorems about the code. To make such techniques tractable, considerable effort is devoted to the development of software tools to ease the theorem proving process.
Mechanical theorem proving, or automated deduction, predated the advent of digital computers. One mathematical system which received considerable attention was equational reasoning, or reasoning with equations. Equality is a fundamental logic concept of universal importance. Equations are often a natural way of expressing mathematical knowledge (and lie at the heart of the class of specification methods known as algebraic specification), and the properties of the equality relation allow us to reason by replacing equals by equals, a very powerful and general technique. The following simple example illustrates this.
Given the equations (or axioms):
0 + x = x (1)
x + 0 = x (2)
(-x) + x = 0 (3)
(x + y) + z = x + (y + z) (4)
prove that:
(- (-a) ) = a for any a
A typical human presentation of a proof might be:
(i) (-(-a)) = (-(-a)) + 0 by (2) (ii) = (-(-a)) + ((-a) + a) by (3) (ill) = ((-(-a)) + (-a)) + a by (4) (iv) = 0 + a by (3) (v) = a by (1)
How may this process be automated?
The process involved in automating such reasoning includes unification (finding variable bindings which will unify. an expression with one side of an axiom, for example replacement of x by (-(-a)) in axiom (2) in step (i) above), rewriting (replacing one side of an axiom by the other side within the context of an expression (replacing equals by equals) and strategy (finding the sequence of axiom applications to show that two expressions are equal).
The major difficulty in automating equational reasoning lies in strategy. Any strategy chosen needs to have two properties, first soundness (any solution found must be correct) and second completeness (if there is a solution, it will be found). Much equational reasoning research is based on the Knuth-Bendix algorithm, a complete and sound strategy for solving the equality problem expressed by a given set of axioms. Interestingly, this important algorithm was first presented by Knuth at a workshop organised in Oxford by the Atlas Computer Laboratory in 1970.
A key idea in equational reasoning is to treat a set of equations as rules for rewriting expressions. A rewrite rule written L = .R is an equation which is used in only one direction, ie L may be replaced by K but not vice versa. In the context of the example above, the equations can be written as:
0 + x = .x
x + 0 = .x
-x + x = .0
(x+y) + z = .x + (y+z)
A set of rewrite rules is called a rewrite system. If none of a set of rewrite rules apply to an expression E, then E is said to be in normal form with respect to that set.
There are two fundamentally important properties of rewrite systems. The rewrite system is said to be terminating if there are no infinite rewriting sequences E =.E' =.E" =...... . This is important because it guarantees that every expression has a normal form. The second property is that every expression has just an unique normal form, a property often called confluence. Confluence coupled with termination ensures that every expression has just one normal form and whether or not any two expressions are equal in such an equational system can be determined by checking whether or not those expressions have the same normal form. A set of rewrite rules which has these two properties is canonical. Intuitively a set of rewrite rules is finite, terminating if each of the right hand sides is somehow simpler than its left hand side. This can be ensured if an ordering of a certain type (termination ordering) can be associated with expressions. Given a terminating set of rewrite rules, the Knuth-Bendix algorithm essentially then adds new rules to the system to make it canonical.
ERIL was basically a very flexible tool to support equational reasoning. At the heart of ERIL was an implementation of the Knuth-Bendix algorithm which was rather more powerful than the original version. ERIL was able to handle algebraic structures which involve partial-functions (for example the division function which is not defined for division by zero) through a technique known as ordered sorts. Much of the power of ERIL derived from its interactive and highly configurable nature. It was possible to set up different sets of axioms, rules, canonical hypotheses and other equality sets, linking them in many different ways, thus providing a very flexible tool for research in equational reasoning.
Not all sets of equations generate sets of rewrite rules. An example is the commutative equation x + y = y + x. Such an equation can be applied an infinite number of times to an expression involving the operator +. No termination ordering can ever orientate such an equation since both sides have exactly the same structure and are derived from one another by a permutation of the variables concerned. There are ways in which such permutative equations may be handled in certain special situations, however, and ERIL was extended to incorporate the use of these.
The ERIL system was used at 25 sites in the UK and at overseas universities. It served as an implementation test bed for ideas in a number of SERC grant-aided projects in UK universities, including Royal Holloway and Bedford New College, University of Glasgow and Imperial College, London.
Jeremy Dick of Informatics was the originator of ERIL and it was also used in other projects locally by Brian Matthews and John Kalmus.