Problems

Starting 2024, CoCo will adopt the new ARI format.

Database

Problem sets used in the competition stem from ARI, a database of confluence problems. Each problem has a unique and persistent number. Each problem is equipped with tags, and problems can be queried using a combination of these tags.

Format

The ARI format replaces the COPS format. A conversion tool between ARI and COPS is available. The main difference is that function symbols, rather than variables, must be declared. Furthermore, S-expressions are used to specify terms, rules and the like. Here is an example:

; @author Kiraku Shintani
; @cops 1133
; secret problem 2019
; category: TRS
(format TRS)
(fun c 1)
(fun t 3)
(fun true 0)
(rule (c (t x y z)) (c (t y x z)))
(rule (c (t x y z)) (c (t x z y)))
(rule (c (t x x z)) true)

All ARI formats consist of an optional header part and a content part. The header part consists of line comments and metadata. Comments are marked with a semicolon ; and extend until the end of the line. Metadata are special comments that start with ;␣@. They resemble key-value pairs, where the key is some arbitrary string not containing white space and the value is a string not containing newlines. In a meta-info line the key is written using a leading @ symbol, separated from the value by a single space. For example, in the line

; @author John Smith

the key author is followed by the value John Smith. Such metadata is used to attribute the problem to one or more authors or contributors, or to cite the literature where the problem first appeared.

The content part of the format represents the rewrite system, and depends on the type of system represented. The following (extended) BNF indicates the lexical and parsing rules for the common syntax of the ARI format:

ARI-format ::= header content
    header ::= ( comment | meta-info )*
   comment ::= ; [␣\t]* (ε | [^@\n] [^\n]*) \n
 meta-info ::= ; ␣ @ [^\n]* \n
   content ::= TRS | CTRS | MSTRS | LCTRS | CSTRS | CSCTRS | multiple-TRS | INF
      term ::= identifier | ( identifier term+ )
    number ::= 0 | [1–9]+[0–9]* 

Comments may appear in the content part, between tokens. All comments are treated as spaces when parsing. An identifier is a non-empty string of printable US ASCII characters, except ␣ \t \n ( ) ; :. In comments other characters may be used as well.

Each problem has one of the following formats. Follow the links to check the details.

• TRS first-order term rewrite systems
• CTRS conditional term rewrite systems
• MSTRS many-sorted term rewrite systems
• LCTRS logically constrained term rewrite systems
• CSTRS context-sensitive term rewrite systems
• CSCTRS context-sensitive conditional term rewrite systems

In addition, there are derived formats for specifying commutation and infeasibility problems.

• multiple-TRS commutation
• INF infeasibility

Conversion Tool

The conversion tool can be used to transform ARI problems into COPS problems.

• Haskell source code
• Linux binary