Confluence Competition

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

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.