HRS Category
The HRS category deals with confluence of higher-order rewrite systems (HRSs) described in
- R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192(1):3–29, 1998.
Input
The input is a higher-order rewrite system (new!), specified in the HRS format.
Problem
An HRS is confluent if any two convertible terms are joinable modulo beta-eta-equivalence. The problem is to answer the question whether the input HRS is confluent or not confluent.
Problem Selection
Problems with tags 'hrs' and 'literature' in our problem database (Cops) are used. If the number of such problems exceeds 100, then 100 problems are selected from these problems; otherwise, all of them are considered. Our advisory board performs the selection using a random number.
Output Format
The output format should follow the same rule as that of the TRS category.
Scoring
The scoring is same as the TRS category.