CoLL

About

CoLL is an automatic confluence tool for left-linear term rewrite systems based on Hindley's Commutation Theorem.
The latest version is based on the techniques:

• Church-Rosser modulo by Jouannaud and Kirchner (SIAM Journal of Computing, 1986)
• parallel closedness of Toyama (NTT ECL Technical Report, 1981)
• parallel-upside and outside closedness of Oyamaguchi and Ohta (Transactions on Information and Systems, 2004)
• simultaneous closedness of Okui (RTA 1998)
• weighted rule labeling of van Oostrom (RTA 2008) and Aoto (RTA 2010)
• redundant rule elimination
• commuting composable decomposition

Download

The source code is freely available.

• CoLL v1.6.2 (latest version, September 26, 2023)
  Corrected calculation of join sequences for rule labeling.
• CoLL v1.6.1 (July 1, 2022)
  Improved Huet's strong closedness criterion.
• CoLL v1.6 (February 1, 2022; July 10, 2022: Re-archived.)
  A maintenance release.
• CoLL v1.5 (July 1, 2020; July 10, 2022: Re-archived.)
  Added several closedness criteria and fixed several bugs.
• CoLL v1.4 (May 30, 2019)
  Fixed a bug in AC-related confluence criteria.
• CoLL v1.3 (May 30, 2019)
  Release for CoCo 2019.
• CoLL v1.2 (January 17, 2018)
  Corrected a renaming bug in rule labeling. Turned off unsound methods for commutation proofs. Tentatively turned the AC-related confluence criteria due to an implementation bug.
• CoLL v1.1 (February 27, 2015)
  Fixed a performance bug in enumeration for the commutation theorem.
• CoLL v1.0 (February 26, 2015)
  April 13, 2015: Despite the extension name, coll-1.0.tar.gz is a non-gzipped .tar file. Please use the next command for extraction:

  tar xfv coll-1.0.tar.gz

• CoLL v0.1 (July 4, 2014)

Requirement

The tools require Linux environments and OCaml. For more detailed information, see the README file bundled with the source codes.

Usage

A typical usage is

$ coll [option] <filename.trs>

Here the input file is specified in the WST competition format. The tool outputs YES if confluence is proved, NO if confluence is disproved, and MAYBE if the tool does not reach any conclusion.

Experimental Data

Experiments for Kiraku Shintani and Nao Hirokawa, ``CoLL: A Confluence Tool for Left-Linear TRSs'' (submitted). The submission is based on CoLL v1.0.

errata in Figure 1
YES of 'development closed'	23 → 17
YES of 'all three '	131 → 125
NO of 'all with elimination'	8 → 9

Tool Authors

• Nao Hirokawa
• Kiraku Shintani

Contact

• Nao Hirokawa