On the completeness of context-sensitive order-sorted specifications

Joe Hendrix, José Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationTerm Rewriting and Applications - 18th International Conference, RTA 2007, Proceedings
PublisherSpringer
Pages229-245
Number of pages17
ISBN (Print)9783540734475
DOIs
StatePublished - 2007
Event18th International Conference on Rewriting Techniques and Applications, RTA 2007 - Paris, France
Duration: Jun 26 2007Jun 28 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4533 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other18th International Conference on Rewriting Techniques and Applications, RTA 2007
Country/TerritoryFrance
CityParis
Period6/26/076/28/07

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'On the completeness of context-sensitive order-sorted specifications'. Together they form a unique fingerprint.

Cite this