Rewrite systems on a lattice of types
type: Item
instance of: scholarly article
title: Rewrite systems on a lattice of types
zbMATH Open document ID: 0575.68043
DOI: 10.1007/BF00264228
author: R. J. Cunningham
author: A. J. J. Dick
published in: Acta Informatica
publication date: 1985-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 08A55
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 03C05
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 3919814
zbMATH Keywords: partial algebras
zbMATH Keywords: modification of the Knuth-Bendix completion algorithm
zbMATH Keywords: decision procedures
zbMATH Keywords: equational theories
zbMATH Keywords: static partiality
zbMATH Keywords: lattice- structured polymorphism
zbMATH Keywords: unification algorithm
zbMATH Keywords: data types
MaRDI profile type: Publication
cites work: Q3912057
cites work: Abstract data types and software validation
cites work: Q5581665
cites work: Q4124327
cites work: On theories with a combinatorial definition of 'equivalence'
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Data Types as Lattices
cites work: Q4124312
cites work: A Search Technique for Clause Interconnectivity Graphs
cites work: Q3992821
full work available at URL: https://doi.org/10.1007/bf00264228
OpenAlex ID: W2086827683
Recommended article: Q4206388
Recommended article: Q4858947
Recommended article: A Rewriting Semantics for Type Inference
Recommended article: A Rewriting Logic Approach to Type Inference
Recommended article: Term rewrite systems for lattice theory
Recommended article: Q3075239
Recommended article: Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework
Recommended article: A rewrite-based type discipline for a subset of computer algebra
Recommended article: An abstract formulation for rewrite systems
description: scientific article; zbMATH DE number 3919814