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 five techniques:
- Church-Rosser modulo by Jouannaud and Kirchner (SIAM Journal of Computing, 1986)
- development closedness of Aoto, Yoshida and Toyama (RTA 2009)
- 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.2 (latest version, 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