* 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