Rewrite systems on a lattice of types (Q1064065)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Rewrite systems on a lattice of types |
scientific article |
Statements
Rewrite systems on a lattice of types (English)
0 references
1985
0 references
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.
0 references
partial algebras
0 references
modification of the Knuth-Bendix completion algorithm
0 references
decision procedures
0 references
equational theories
0 references
static partiality
0 references
lattice- structured polymorphism
0 references
unification algorithm
0 references
data types
0 references