HRS Category

This category is concerned with confluence of higher-order rewrite systems.

Format

The input is a higher-order rewrite system, specified in the HRS format.

The question to be answered is whether the higher-order rewrite system is confluent. 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. (FUN 
     abs : (term -> term) -> term
     app : term -> term -> term
   )
   (VAR
     x : term
     S : term
     F : term -> term
   )
   (RULES
     app(abs(\x.F x),S) -> F(S),
     abs(\x.app(S,x)) -> S
   )
   

   The correct answer is YES and a possible output is

   YES
   
   The HRS is weakly orthogonal.
   

2. (FUN
     f : o -> o -> o
     s : o -> o
     a : o
     b : o
     mu : (o -> o) -> o
   )
   (VAR
     x : o
     Z : o -> o
   )
   (RULES
     f x x -> a,
     f x (s x) -> b,
     mu (\x. Z x) -> Z (mu (\x. Z x))
   )
   

   The correct answer is NO and a possible output is

   MAYBE
   

Problem Selection

Problems are selected among those in HRS format in COPS.