* 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