On the Completeness of Context-Sensitive Order-sorted Specifications

Hendrix, Joe; Meseguer, José

Permalink

https://hdl.handle.net/2142/11291 Copy

Description

Title

On the Completeness of Context-Sensitive Order-sorted Specifications

Author(s)

• Hendrix, Joe
• Meseguer, José

Issue Date

2007-02

Keyword(s)

computer science

Abstract

We propose three different notions of completeness for term rewrite specifications supporting order-sorted signatures, deduction modulo axioms, and context-sensitive rewriting relative to a replacement map mu. Our three notions are: (1) an appropriate definition of mu-sufficient completeness with respect to a set of constructor symbols; (2) a definition of mu-canonical completeness under which mu-canonical forms coincide with canonical forms; and (3) a definition of semantic completeness that guarantees that the mu-operational semantics and standard initial algebra semantics are isomorphic. 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 ground confluence, ground sort-decreasingness, weakly normalization, and left-linearity. Although the general equational tree automata problems are undecidable, our algorithms work modulo any combination of associativity, commutativity, and identity axioms. For all combinations of these axioms except associativity without commutativity, our algorithms are decision procedures. For the associativity without commutativity case, which is undecidable in general, our algorithms use learning techniques that are effective in all practical examples we have considered. We have implemented these algorithms as an extension of the Maude sufficient completeness checker.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11291

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections