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:
For instance, consider the functional module NAT-SOUP (available in qlock.maude from the examples.zip bundle below):

fmod NAT-SOUP is
  sorts Nat NeSoup Soup .
  subsorts Nat < NeSoup < Soup .

  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.

Download

You need:
Documentation
05/15/2012