Lecture Notes in Computer Science, 2007, Volume 4533/2007, 229-245, DOI: 10.1007/978-3-540-73449-9_18

On the Completeness of Context-Sensitive Order-Sorted Specifications

Joe Hendrix and José Meseguer

View Related Documents

Abstract

We propose three different notions of completeness for order-sorted equational specifications supporting context-sensitive rewriting modulo axioms relative to a replacement map μ. Our three notions are: (1) a definition of μ-canonical completeness under which μ-canonical forms coincide with canonical forms; (2) a definition of semantic completeness that guarantees that the μ-operational semantics and standard initial algebra semantics are isomorphic; and (3) an appropriate definition of μ-sufficient completeness with respect to a set of constructor symbols. Based on these notions, we use equational tree automata techniques to obtain decision procedures for checking these three kinds of completeness for equational specifications satisfying appropriate requirements such as weak normalization, ground confluence and sort-decreasingness, and left-linearity. The decision procedures are implemented as an extension of the Maude sufficient completeness checker.
Research supported by ONR Grant N00014-02-1-0715.

Fulltext Preview

Image of the first page of the fulltext document