* Category type
demonstration category for CoCo 2016
* Problem and Semantics
Given an equational order-sorted conditional specification (Sigma, R \cup A) where A is the ACU-axioms, the problem is to answer whether the rewrite relation ->R,A is Church-Rosser modulo =_A (i.e., s =_{R \cup A} t implies that there exist u,v such that s -*->_{R,A} u =_A v <-*-_{R,A} t) or not.
We assume that the input specification (Sigma, R \cup A) is
- preregular and sort-decreasing,
- A-coherent (i.e. u' =_A u ->_{R/A} v implies u' ->_{R,A} v' =_A v for some v') and
- R is strongly deterministic (i.e. R is deterministic, and for any rhs t of the condition part,
t\sigma is an ->_{R,A}-normal form for every ->_{R,A}-normalized substitution \sigma.)
The mathematical foundations of the tool are presented in [1].
[1] Francisco Duran, Jose Meseguer: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebr. Program. 81(7-8): 816-850 (2012)
* Input format
The format of input equational order-sorted conditional specifications follows the standard Maude syntax, including:
- Both valid functional and system modules can be handled, although only the equational part of system modules is considered.
- Any declaration may be included, except membership axioms (using “mb” or “cmb”), no support for membership equational logic.
- Each functions may be associative (indicated as 'assoc') and/or commutative (indicated as 'com') and/or have an identity c (indicated as 'id: c’).
- Modules may be structured as desired, using any hierarchy of inclusions (in any of the possible modes).
The only restrictions are:
- Attributes “special” (built-in functions) and “iter” are not supported.
* Examples
(1) The following example specifies length of lists with associativity. + on numbers is ACU.
fmod NAT-ACU is
sorts Nat NzNat .
subsorts NzNat < Nat .
op 0 : -> Nat [ctor] .
op 1 : -> NzNat [ctor] .
op _+_ : NzNat NzNat -> NzNat [ctor assoc comm id: 0] .
op _+_ : Nat Nat -> Nat [ctor assoc comm id: 0] .
endfm
fmod NAT-LIST-ACU is
protecting NAT-ACU .
sort NeList List .
subsort Nat < NeList < List .
op __ : NeList NeList -> NeList [ctor assoc] .
op nil : -> List [ctor] .
vars l l' : List . var n : Nat .
op |_| : List -> Nat .
eq | nil | = 0 .
eq | n | = 1 .
eq | l l' | = | l | + | l' | .
endfm
(2) The following is a specification of hereditarily finite sets.
fmod HF-SETS is
sort Magma .
sort Set .
subsort Set < Magma .
op _`,_ : Set Magma -> Magma [ctor assoc comm] .
op _`,_ : Magma Magma -> Magma [assoc comm] .
op `{_`} : Magma -> Set [ctor] .
op `{`} : -> Set [ctor] .
vars M M' M'' N : Magma .
vars S S' : Set .
eq [01]: M, M, M' = M, M' .
eq [02]: M, M = M .
op _in_ : Magma Magma -> Bool .
eq [03]: M in {} = false .
eq [04]: {} in {{M}} = false .
eq [05]: {} in {{}} = true .
eq [06]: {} in {{}, M} = true .
eq [07]: {} in {{M}, N} = {} in {N} .
eq [08]: {M} in {M'} = M in M' .
ceq [09]: S in S', N = true if S in S' = true .
ceq [10]: S in S', N = S in N if S in S' = false .
ceq [11]: S, M in M' = M in M' if S in M' = true .
ceq [12]: S, M in M' = false if S in M' = false .
op _equiv_ : Magma Magma -> Bool [comm] .
eq [13]: M equiv M = true .
eq [14]: {} equiv {M} = false .
eq [15]: {M} equiv {M'} = M equiv M' .
eq [16]: S equiv S, M' = S equiv M' .
ceq [17]: S equiv M = false if S in {M} = false .
ceq [18]: S, M equiv M' = false if S in {M'} = false .
ceq [19]: M equiv M' = false if {M} in {{M'}} = false .
op _<=_ : Magma Magma -> Bool .
eq [20]: {} <= M = true .
ceq [21]: {M} <= M' = true if M in M' = true .
ceq [22]: {M} <= M' = false if M in M' = false .
ceq [23]: S, M <= M' = M <= M' if S <= M' = true .
ceq [24]: S, M <= M' = false if S <= M' = false .
eq [25']: M in {M} = true .
eq [26]: M in {M, M'} = true .
eq [27]: M in {M}, M' = true .
eq [28]: M in {M, M'}, M'' = true .
endfm