The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/28900
Record Status Checked
Record Id 28900
Title Dynamic Order-Sorted Term-Rewriting Systems
Abstract <P> This thesis considers the problems of order-sorted equational logic and its operational interpretation, order-sorted term rewriting. <P> Order-sorted equational logic is a well-known paradigm in the field of algebraic specification for expressing partial functions and error handling. In this thesis we review the work undertaken in this field and present a new implementation of order-sorted term rewriting, an equational theorem-proving environment known as <EM>MERILL</EM>. This implementation extends previous implementations by integrating the order-sorted rewriting process with reasoning modulo associative-commutative axioms. The implementation of this system is described and examples of its use are given. <P> However, the standard theory of order-sorted equational logic and term rewriting also has theoretical and pragmatic difficulties. In particular, the restriction to sort-decreasing rules limits its practical application, and this can be traced to difficulties in the semantics. There have been several approaches to overcoming these problems, which are reviewed. <P> The thesis develops a new approach to the semantics of order-sorted specification, via a two-tier model, called a dynamic algebra, and a corresponding dynamic equational logic. A term-rewriting theory is then associated with this semantics. This approach, dynamic order-sorted term rewriting, uses dynamic terms where the sort of terms is carried as extra information within the structure of the term. This information may change as the rewriting process uncovers further sort information of terms. Matching and unification are defined for dynamic terms, although well-sorted unification proves to be undecidable. <P> Dynamic rewriting is shown to be sound and complete. However, to automatically generate rewriting proofs, the Church-Rosser property is required. To establish this, completion algorithms are given, subject to two properties: well-sorted unification and the coherence property. Criteria are given which satisfy these conditions; the definition of further criteria remains an open problem. An alternative approach of constrained order-sorted rewriting, using well-sortedness constraints, is also proposed. <P> Examples of the use of dynamic rewriting are given and an implementation of dynamic rewriting is proposed.
Organisation CCLRC , BITD
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Thesis PhD, University of Glasgow, 1996. http://ethos.bl.u…n=uk.bl.ethos.337505 1996