CPF 3 and CeTA 3

CPF 3

Note that CPF 3 has just been fixed with the release of CeTA 3.0.

CPF 3 has several non backwards compatible changes to improve the overall structure of CPF.

several XML-elements have been simplified so that they are less verbose, e.g., the <arg> element around arguments of terms
CPF 3 now support term-indexing and rule-indexing, e.g., it is possible to label rules (e.g., “r1”, “r17”, “A”, “B”) and then just specify to remove rules “A” and “B”.
the joining sequences in the various confluence and commutation criteria have been simplified and unified: these sequences are now just list of terms
all techniques in termination proofs that delete rules (in DP-setting or TRS-setting) now consistently require the set of deleted rules
there is no separation between <relativeTerminationProof> and <trsTerminationProof> any more
see file xml/cpf2_to_3.xsl for a detailed list of changes
overall the CPF 2 certificates in termCOMP and CoCo 2023 have been reduced from 8.7 Gb size to 2.9 Gb size for CPF 3; these certificates are available at http://cl-informatik.uibk.ac.at/software/ceta/cpf3archive/index.html

Converter

CeTA version 3.0 will no longer accept CPF 2 files, but insists on CPF 3 files. However, all of the current tools produce CPF 2 files. Therefore, this archive contains a converter from CPF 2 to CPF 3; it can be compiled by

cd xml; make

Afterwards

xml/cpf2_to_3.sh [--termIndex] proof.cpf2.xml > proof.cpf3.xml

converts a file from CPF 2 to CPF 3. The optional --termIndex flag turns on term-indexing. This will slow down the converter, but results in smaller proofs which are also faster to check by CeTA.

One can always perform a syntactic check on the valid CPF structure of an XML-file proof.cpf3.xml by

xmllint --huge --noout --schema xml/cpf3.xsd proof.cpf3.xml

The converter successfully converted all CPFs of CoCo 2020–2023 and of termCOMP 2023, so that the resulting CPF 3 files are valid w.r.t. the schema and are certified by CeTA 3.0.

A few CPF 3 examples are included in the examples-directory here or in the examples-directory of CeTA 3.0.

Running certification mode of a competition with CPF 3

CPF and CeTA 3 now have a new mode to take input, property, answer and proof as separate arguments. In this way it is ensured that the tools cannot change the input TRS, etc.

The workflow is as follows.

assume we are in category CR, and want to check confluence of example.trs via tool.sh
tool.sh is run on example.trs with first-line YES/NO/MAYBE and proof afterwards.
if the tool was successful,
store first line as string in file answer.txt
store proof in file proof.cpf2.xml
until tools do not support CPF 3: convert proof.cpf2.xml to proof.cpf3.xml as described above
if desired, run an XML syntax check as described above
run competition converter tool to convert example.trs to example.input.xml
finally invoke CeTA via

ceta --inputf example.input.xml --property CR --answerf answer.txt proof.cpf3.xml
(one could also use --answer and then provide a string directly, without storing the answer in a file answer.txt; invoke CeTA 3.0 without arguments or have a look at CeTAs Main.hs to see the various options)

So, the only thing that needs to be done by competition organizers is to provide a trusted converter from the competition format to the CPF input format, see the file xml/cpf3.xsd, element <input> for details:

for termination and complexity use CPF 3 element input/trsInput
for confluence use CPF 3 element input/trsWithSignature
for commutation use CPF 3 element input/twoTrsWithSignature
for infeasibility use CPF 3 element input/infeasibilityInput
for all categories, the root element must be input

CeTA 3 format of properties

for termination and relative termination use SN
for complexity use RC or DC
for the various CoCo categories use their abbreviation CR, COM, INF

CeTA 3 format of answers

YES or NO for all binary answers (termination, confluence, etc.)
WORST_CASE(?,O(n^d)) for complexity answers with a concrete number d