Difference between revisions of "Maude Tools:Ordersorted Term Patterns"
Maudesystem (Talk  contribs) (Created page with "== Introduction == This page introduces the Maude Ordersorted Pattern Solver, a tool that accepts an ordersorted pattern as input and can—in many...") 
(No difference)

Revision as of 22:23, 30 April 2015
Contents
Introduction
This page introduces the Maude Ordersorted Pattern Solver, a tool that accepts an ordersorted pattern as input and can—in many cases—discover a finite union of terms equivalent to the given pattern, if it exists.
Ordersorted term patterns are a simple notation for describing unions, intersections, and differences of sets of terms generated by an ordersorted signature.
Our tool transforms general patterns into finite unions by interpreting intersection as unification and difference as an application of our ordersorted symbolic difference algorithm.
Example Patterns
Suppose t1, t2, and t3 are terms in an ordersorted signature. Then:
 {t1,t2,t3} is the pattern representing the union of instances these terms.
 {t1}  {t2} is the pattern representing the instances of t1 that are not instances of t2.
 {t1,t2} & {t3} is the pattern representing the intersection of instances of t1 and t2 with t3.
Theoretical Details
Closure Under Boolean Operations
For some signatures, term patterns are closed under union, intersection, and difference. Otherwise, we can usually apply a transformation to a signature so that it becomes closed under these operations.
Special Patterns
Assuming finite signatures, there is a finite pattern which generates every term. There is also a finite pattern generates no terms (e.g. the empty pattern).
Pattern Equivalence
Two patterns are considered equivalent if they generate the same term set. This condition can be checked by observing if the subtracting each pattern by the other results in the empty pattern.
Relationship to Propositional Tree Automata
An ordersorted signature can be viewed as a tree automaton that accepts as inputs any term that the signature generates. The generalization of a tree automaton—a propositional tree automaton—can accept not only terms but also unions, intersections, and complements of terms. Our ordersorted term patterns provide a simpler and more intuitive algorithm which accomplishes this same task.
Ordersorted Symbolic Difference
Our symbolic difference algorithm generalizes previous approaches such as that of Lassez and Marriott, by extending to the case of ordersorted terms.
Download
Download link coming soon.
Tool Example Inputs
Example inputs coming soon.