AboutCoLL 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
DownloadThe source code is freely available.
- CoLL v1.5 (latest version, July 1, 2020)
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.gzis 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)
RequirementThe tool requires:
UsageA typical usage is
$ coll [option] <filename.trs>Here the input file is specified in the WST competition format. The tool outputs
YESif confluence is proved,
NOif confluence is disproved, and
MAYBEif the tool does not reach any conclusion.
Experimental DataExperiments 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|
- Nao Hirokawa
- Kiraku Shintani