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 and 64-bit Linux executable of CoLL are freely available.
- CoLL v1.1 (latest version, February 27, 2015)
fixed a performance bug in enumeration for the commutation theorem
- CoLL v1.0 (February 26, 2015)
- 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