Rewrite systems on a lattice of types (Q1064065)

The Knuth-Bendix algorithm is an established technique for compiling decision procedures for simple equational theories. Certain problems are known to exist in using the method for sets of rules which involve partial operations. This paper describes an extension that enables the treatment of static partiality through use of a particularly expressive lattice-structured polymorphism. Natural relationships between types are expressed by a partial ordering, and functions have sets of signatures to describe their full sortal behaviour. A finitary unification algorithm is defined for expressions in this typing scheme. Apart from enabling the treatment of certain partial operations, the use of a lattice of types gives a natural framework for specifying data types in Computer Science without over-specifying error situations.