TY - GEN
T1 - On the completeness of context-sensitive order-sorted specifications
AU - Hendrix, Joe
AU - Meseguer, José
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=38049148582&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38049148582&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-73449-9_18
DO - 10.1007/978-3-540-73449-9_18
M3 - Conference contribution
AN - SCOPUS:38049148582
SN - 9783540734475
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 229
EP - 245
BT - Term Rewriting and Applications - 18th International Conference, RTA 2007, Proceedings
PB - Springer
T2 - 18th International Conference on Rewriting Techniques and Applications, RTA 2007
Y2 - 26 June 2007 through 28 June 2007
ER -