Confluence Competition

HRS Category

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


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.


  1. (FUN 
      abs : (term -> term) -> term
      app : term -> term -> term
      x : term
      S : term
      F : term -> term
      app(abs(\x.F x),S) -> F(S),
      abs(\,x)) -> S
    The correct answer is YES and a possible output is
    The HRS is weakly orthogonal.
  2. (FUN
      f : o -> o -> o
      s : o -> o
      a : o
      b : o
      mu : (o -> o) -> o
      x : o
      Z : o -> o
      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

Problem Selection

Problems are selected among those in HRS format in COPS.