GCR Category

The GCR category is concerned with ground-confluence of many-sorted term rewrite systems (MSTRSs).

Format

The input is a many-sorted first-order rewrite system without conditions, specified in the MSTRS format.

The question to be answered is whether the rewrite system is confluent on all well-sorted ground terms that can be built from the function symbols in the (SIG funlist) declaration. The first line of the output must be

• YES, indicating that the input system is confluent,
• NO, indicating that the input system is non-confluent,
• any other answer (e.g., MAYBE) indicates that the tool could not determine the status of the input problem.

In the first two cases, the output must be followed by justification that is understandable by a human expert.

Examples

1. (VAR x)
   (SIG 
     (a -> 0)
     (b -> 0)
     (c -> 0)
     (f 0 0 -> 1)
   )
   (RULES
     a -> b
     f(b,b) -> f(a,a)
     f(x,a) -> f(a,a)
   )
   

   The correct answer is NO and a possible output is

   NO
   
   The peak f(c,b) *<- f(c,a) ->* f(a,a) is not joinable since f(c,b) is not
   among the reducts { f(a,a), f(b,a), f(b,a), f(b,b) } of f(a,a).
   

2. (SIG
      (0 -> Nat)
      (s Nat -> Nat)
      (eq Nat Nat -> Bool)
      (true -> Bool)
      (false -> Bool)
   )
   (RULES
      eq(x,x) -> true
      eq(0,s(x)) -> false
      eq(s(x),0) -> false
      eq(s(x),s(y)) -> eq(x,y)
      eq(x,y) -> eq(y,x)
   )
   

   The correct answer is YES and a possible output is

   YES
   
   Ground-confluence can be shown by rewriting induction, as explained in
   the FSCD 2016 paper of Takahito Aoto and Yoshihito Toyama.
   

Problem Selection

Problems are selected among those in COPS with the 'trs' or the 'mstrs' tag. The former are transformed into MSTRSs with a single sort, prior to passing them to competing tools.