Equality Enrichments for Order-Sorted Maude Theories
An equality enrichment for an equational theory is a transformation that extends the input theory with equationally-defined equality and inequality predicates for all its sorts. These predicates are sound for comparing all terms, including those that contain variables.
The implementation of this transformation can be performed on order-sorted Maude functional modules with free constructors and supports any combination of associative and commutative function symbols. The resulting functional module preserves all computational properties (i.e., ground operational termination, ground confluence, ground sort-decreasingness, and sufficient completeness) of the input module.
On the installation and use
The transformation has been implemented entirely in Maude using its reflection capabilities.
The latest version of the tool works on Maude 2.6.
To load the tool one just needs to load the Maude code of the transformation.
If maude is your Maude executable,
the equality enrichment transformation is in file eq-enrich.maude,
and all files are in the same directory or in your path, you can load the equality enrichment transformation as follows:
$ maude eq-enrich.maude
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.6 built: Dec 10 2010 11:12:39
Copyright 1997-2010 SRI International
Sat May 7 21:19:03 2011
Maude>
The equality enrichment transformation offers the following command:
red eq-enrich(<input-module>)
extends the input functional module, assumed to have a sub-signature of free constructors,
with equationally-defined equality and inequality predicates for all its sorts.
For instance, consider the functional module
NAT-SOUP
(available in qlock.maude from the
examples.zip bundle below):
op 0 : -> Nat [ctor] .
op s_ : Nat -> Nat [ctor] .
op mt : -> Soup [ctor] .
op __ : NeSoup NeSoup -> NeSoup [ctor assoc comm] .
op __ : Soup Soup -> Soup [assoc comm] .
eq S:Soup mt = S:Soup .
endfm
Once loaded, the equality enrichment transformation can be performed on
NAT-SOUP as follows:
Maude> select EQ-ENRICH .
Maude> red eq-enrich(upModule('NAT-SOUP,false)) .
Currently, Maude's metalevel reduction commands can be used to reduce
meta-expressions involving the equality and inequality predicates.
For instance, the following command checks if the terms
mt s(X:Nat) and
s(X:Nat) are equal:
Maude> red metaReduce(eq-enrich(upModule('NAT-SOUP,false)),'_~_['__['mt.Soup,'s_['X:Nat]],'s_['X:Nat]]) .
result ResultPair: {'true.Bool,'Bool}
In a future release, this transformation will be part of the
Maude Formal Environment (MFE)
so that checks as the one above are available to other Maude tools and can also be executed
at the object level.
Order-Sorted Equality Enrichments Modulo Axioms.
Raúl Gutiérrez, José Meseguer, and Camilo Rocha. Technical Report, Department of Computer Science in
the University of Illinois at Urbana-Champaign. Urbana, December 2011.
Order-Sorted Equality Enrichments Modulo Axioms.
Raúl Gutiérrez, José Meseguer, and Camilo Rocha.
9th International Workshop on Rewriting Logic and its Applications (WRLA12).
Tallinn, March 2012. (To Appear)