Saigawa, CoLL, and Hakusan

About

These are a fully automatic confluence tool for first-order term rewrite systems.

Download

Latest Version

• CoLL 1.6.2: see CoLL's website
• CoLL-Saigawa 1.7: collsaigawa-1.7.tgz
  (September 26, 2023: Fixed a performance bug in rule labeling.)
• Hakusan 0.11: hakusan-0.11.tgz
  (June 20, 2024: Supported rule removal and CPF-3 outputs. An external termination tool is no longer necessary.)
  
• Saigawa 1.12: saigawa-1.12.tgz
  (May 11, 2019; improved performance of the criterion based on critical-pair-closing systems)

Older Versions

Hakusan

• Hakusan 0.10: hakusan-0.10.tgz
  (December 9, 2023: All proof outputs are now certifiable by CeTA. The options are reorganized.)
• Hakusan 0.9: hakusan-0.9.tgz
  (September 26, 2023: Supported -pcps+, -pcpscert, -pcpscert+, and renamed -pcpcs to -orthogonal+. Corrected a performance bug in non-confluence check.)
• Hakusan 0.8: hakusan-0.8.tgz
  (August 3, 2023: Supported certificate outputs for rule labeling (-prlcert). Termination tools with XML inputs can be used (-ttx).)
• Hakusan 0.6: hakusan-0.6.tgz
  (March 4, 2023: Supported a reduction method.)
• Hakusan 0.5: hakusan-0.5.tgz
  (July 9, 2022: A release for CoCo 2022.)
• Hakusan 0.4: hakusan-0.4.tgz
  (May 6, 2022: Corrected the PCPS criterion.)
• Hakusan 0.3: hakusan-0.3.tgz
  (April 28, 2022: A maintenance release.)
• Hakusan 0.2: hakusan-0.2.tgz
  (April 7, 2022: Supported the automatic mode -auto.)
• Hakusan 0.1: hakusan-0.1.tgz
  (February 19, 2022: This is a prototype tool for the future version of CoLL/Saigawa.)

Saigawa

• Saigawa 1.11: saigawa-1.11.tgz
  (May 10, 2019; improved performance of hot decreasingness)
• Saigawa 1.10: saigawa-1.10.tgz
  (March 25, 2018; fixed a bug in hot decreasingness)
• Saigawa 1.9: saigawa-1.9.tgz
  (January 23, 2018; implemented criteria based on critical-pair-closing and hot-decreasingness)
• Saigawa 1.8: saigawa-1.8.tgz
  (June 3, 2015; included a missing interface file. Thanks to Bertram Felgenhauer)
• Saigawa 1.7: saigawa-1.7.tgz
  (February 1, 2015; fixed a bug in AC-unification.)
• Saigawa 1.6: saigawa-1.6.tgz
  (July 2, 2014; improved error messages.)
• Saigawa 1.5: saigawa-1.5.tar.gz
  (July 9, 2013; partly supported confluence criterion of [Hirokawa and Middeldorp, IWC 2013])
• Saigawa 1.4: saigawa-1.4.tar.gz (x64 Linux executable)
  (May 22, 2012; supported confluence criterion of [Jouannaud and Kirchner, SIAM Journal of Computing 1986])
• Saigawa 1.3: saigawa-1.3.tar.gz
  (May 22, 2012; supported confluence criterion of [Klein and Hirokawa, LPAR 2012])
• Saigawa 1.2: saigawa-1.2.tar.gz
  (October 3, 2011; supported fully automatic mode)
• Saigawa 1.1: saigawa-1.1.tar.gz
  (July 19, 2011; fixed a bug of -dc and -dc2)
• Saigawa 1.0: saigawa-1.0.tar.gz
  (November 30, 2010)

CoLL-Saigawa

• CoLL-Saigawa 1.6: collsaigawa-1.6.tgz
  (February 1, 2022: A maintenance release. July 10, 2021: Re-archived.)
• CoLL-Saigawa 1.5: collsaigawa-1.5.tgz
  (June 10, 2021: Supported parallel closedness based on parallel critical pairs, simultaneous closedness, parallel-upside closedness, and outside-parallel closedness. July 10, 2022: Re-archived.).
• CoLL-Saigawa 1.4: collsaigawa-1.4.tgz (May 30, 2019: Fixed a performance bug.)
• CoLL-Saigawa 1.3.1: collsaigawa-1.3.1.tgz
  (May 30, 2019: Fixed a bug in AC-related confluence criterion; release for CoCo 2019 full run)
• CoLL-Saigawa 1.3: collsaigawa-1.3.tgz
  (May 30, 2019: release for CoCo 2019)
• CoLL-Saigawa 1.2: collsaigawa-1.2.tgz
  (August 7, 2018: release for CoCo 2018)
• CoLL-Saigawa 1.1: collsaigawa-1.1.tgz
  (August 24, 2017: due to an implementation bug, an AC-related confluence criterion has tentatively been unavailable.)
• CoLL-Saigawa 1.0: collsaigawa-1.0.tgz
  (August 2, 2015: combined CoLL 1.1 and Saigawa 1.8)

Usage

Usage of saigawa is

$ saigawa [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 the paper of Nao Hirokawa, Dohan Kim, Kiraku Shintani, and René Thiemann, ``Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs'', 13th CPP, pp. 147–161, 2024.
• Experiments for the paper of Kiraku Shintani and Nao Hirokawa, ``Compositional Confluence Criteria'', LMCS 20(1), pp. 6:1–6:28, 2024.
• Experiments for the PhD thesis of Kiraku Shintani, ``Compositional Confluence Criteria for Term Rewriting'', JAIST, 2023.
• Experiments for the paper of Kiraku Shintani and Nao Hirokawa, ``Compositional Confluence Criteria'', 7th FSCD, LIPIcs 228, pp. 28:1–28:19, 2022.
• Experiments for the paper of Nao Hirokawa, Julian Nagele, Vincent Van Oostrom, and Michio Oyamaguchi, ``Confluence by Critical Pair Analysis Revisited'', CADE-27, 11716, pp. 319–336, 2019.
• Experiments for the paper of Dominik Klein and Nao Hirokawa, ``Confluence of Non-Left-Linear TRSs via Relative Termination'', LPAR-18, LNCS 7180, pp. 258–273, 2012.
• Experiments for the journal article of Nao Hirokawa and Aart Middeldorp, ``Decreasing Diagrams and Relative Termination'', JAR 47, pp. 481–501, 2011.

Tool Authors

• Nao Hirokawa
• Kiraku Shintani
• Dominik Klein

Contact

• Nao Hirokawa