TermComp Discussions @ WST

[ffrohn]

This is the place to collect TermComp-related topics that should be discussed at WST, if time allows:

• Full run vs. running on subsets of TPDB?
• "Bring your own benchmarks": The idea is that everybody who wants to participate has to contribute a certain number of benchmarks. This is done at the SAT competition.
• Do we want winner's certificates?
• Uniform format for certification?
• How to deal with several certifiers? Do we want a "competition" between certifiers?
• clean up termination-portal.org
• move termination-portal.org to some more recent infrastructure
• Shall we try to standardize ARI (together with CoCo)?
• Docker / new infrastructure: experiences, criticism, ideas to improve...
• How can we attract new / more participants?
• New categories?

If you have further ideas, please add a comment. As we won't have time to discuss all of these things, please indicate if you're particularly interested in one of these topics.

[ffrohn]

• Shall we archive participating provers (e.g., on Zenodo)?

[jwaldmann]

• "won't have time to discuss ..." but WST is the ideal place to discuss (in person), and we should make room in the schedule, e.g., cut short (not remove, but compress) the presentation of system descriptions, unless there is strong public interest. Or merge somehow, e.g., presentation of cetera has just one technical point (our approach to the RFC theorem in Agda) and can then quickly turn into a discussion about "several certifiers"

• "several certifiers": I brought this up because we are working on https://git.imn.htwk-leipzig.de/waldmann/cetera#cetera meanwhile we think it's too early to be run in termcomp2025 (also, containerisation, and ceta-2/3 changes, are eating my time) but we hope to have something moderately interesting, and working, for 2026.

• "competition between certifiers" - this would only work for a common subset (of proof techniques), could still be interesting to compare efficiency of extracted code for certificate checking - that's mainly for Isabelle/Agda/Haskell compiler authors? But in general - certifiers will differ, so the prover has to know who will certify the output, in order to adapt the proof search strategy. (E.g., "matchbox for common-subset-of ceta and cetera")

[ffrohn]

• Demo categories: At least this year, they caused tons of work, and I don't see much benefit. Other competitions do not have them either, as far as I know. I'd like to get rid of them.

[jwaldmann]

benefit is (ideally) that a demonstration of a (new) category creates awareness, interest, and participants (for the future).

but in practice, "demo" = "only one participant"?

what are 2025 demo categories? I am counting

$ for f in *.txt; do wc -l $f | tr -d '\n' && echo -n " - " && cat $f; done| grep "1 "
1 C_Complexity.txt - nlommen/koat:35b7a7
1 Complexity_ITS.txt - nlommen/koat_loat:35b7a7
1 Derivational_Complexity_Full_Rewriting.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Derivational_Complexity_Innermost_Rewriting.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Higher_Order_Rewriting.txt - cynthiakop/wanda:secondtry
1 Integer_TRS_Innermost.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Java_Bytecode_Recursive.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Java_Bytecode.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Logic_Programming_with_Cut.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Prolog.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 PTRS_Innermost.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 PTRS_Standard.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Runtime_Complexity_Full_Rewriting.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 Runtime_Complexity_Innermost_Rewriting.txt - jckassing/aprove_solver:aprove_termcomp25_v5 cert
1 Runtime_Complexity_Parallel_Innermost_Rewriting.txt - jckassing/aprove_solver:aprove_termcomp25_v5
1 TRS_Conditional_Termination.txt - raulgut/muterm-image:term-comp2025
1 TRS_Outermost.txt - jckassing/aprove_solver:aprove_termcomp25_v5 cert

so, clearly, Aprove should pay your (over)time for handling these :-)

perhaps introduce rules like

• "a demo category needs a participant, and a sponsor (different person, different affiliation)" who writes a short paper (for next WST) describing the intention and merits of having the category, and helps the termcomp organizer in preparing/running it. (modelled after "Robert's Rules of Order": every motion (to be considered by an assembly) needs to be seconded https://www.gutenberg.org/cache/epub/9097/pg9097-images.html#sec67)
• "a demo category only runs once" (meaning: it must acquire more participants for next year)

[AkihisaYamada]

I'd propose

• a demo category runs on request

So it will run on the first proposal, and when the tool made progress for the category. The VBS makes the progress visible (so a demo run is expected to have some "news").

It is also good for potential new participants to know the state of the art.

[ffrohn]

But that's basically what we have (request = registration).

I like the idea of linking demo categories to (WST) papers: Run the category if the merits of having it become clear from a recent (i.e., submitted / published after the previous competition) paper.

[AkihisaYamada]

I'd say registration is just declaration that the tool is ready to participate. Otherwise, if a new tool want to participate, it must negotiate so that the original tool will register too.

I think, request = paper is a bit too strong. Just a bugfix may worth a rerun, but not a paper.

[AkihisaYamada]

I'd propose (any) request = GitHub issue.

[jwaldmann]

Re: infrastructure (let's wait for results but ...) matchbox wants: more time, or more cores, or both. mnm wants: more RAM (I guess). Can you show us (in the meeting) the costs that this would bring.

[jwaldmann]

Re: winners' certificates: If you bring them (files, templates) I can print them (during WST).

[J-C-Kassing]

I am particularly interested in:

• Full run vs. running on subsets of TPDB
  -> I am in favor of running on subsets to increase the volatility of the results, which will hopefully increase the excitement of the competition. However, this requires fixed rules for selecting the subsets so that not all benchmarks used come from the same group.

• How can we attract new / more participants?
  -> What about a "Publicity Chair", i.e., a person who is responsible for creating visibility of the competition, designing logos, trying to attract new research groups to the competition, etc. More importantly, someone that helps the organizer, who can then focus on running the competition.

• Clean up termination-portal.org

• Shall we try to standardize ARI (together with CoCo)?
  -> We should definitely try to do that. Maybe we can create a "TRS-Lib Standard" (similar to the SMT-LIB Standard) that allows for shorts scripts as well? Having command language including statements like (check-termination) or (check-confluence) for tools sounds like an interesting idea to me.

• New Categories & Demo Categories
  -> If there are no significant updates to the tools in demo categories and there are no new benchmarks, then I do not see a reason to run the demo categories in the competition. A significant update could require a short paper (for next WST) as Johannes suggested. Perhaps such improvements should be evaluated by the tool authors themselves and only mentioned as an “honorable mention” by the competition itself.
  Nevertheless, I think reducing the number of categories is a good idea, as it provides a better overview and makes getting started with new tools less overwhelming.

[jwaldmann]

not at business meeting, but at workshop dinner: ask participants for predictions (bets) on certain outcomes of the competition (Geoff does something like this for CASC, https://tptp.org/CASC/30/Gambling.html)

bets could be placed on any (even a silly) property, the goal is to induce discussion among participants, and (side goal) to collect some money for supporting (recognizing the work of) the competition organizer.

[jwaldmann]

some more ideas: https://git.imn.htwk-leipzig.de/waldmann/cetera/-/blob/wst2025/doc/wst25/talk/termcomp.tex?ref_type=heads

Examples where status of benchmark is known but not well-known

• SRS_Standard/Zantema_06/while1 is YES, Aprove did this in TC 2008, maybe matchbox does it this year (https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/561)
• SRS-Relative/Zantema_06_relative : only rel03 remains open? (https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/402)
• SRS_Standard/Gebhardt_06 is fully solved (https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/487#note_24336)
• SRS-Standard/Yolcu-21 : Farkas is solved, see paper cited in https://github.com/emreyolcu/rewriting-collatz?tab=readme-ov-file
• SRS-Standard/Wenzel-16 is fully solved https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/381

[AkihisaYamada]

• Docker / new infrastructure: experiences, criticism, ideas to improve...

The -- options are not too easy to deal with. I'd propose

• The solver name accuired by cat NAME.txt.
• Execusion by solver benchmark, with environment variables $TIMEOUT, $CATEGORY, and more in future.

[AkihisaYamada]

• clean up termination-portal.org
• move termination-portal.org to some more recent infrastructure

I think GitHub pages is a convenient option. It seems you just need markdown files so editing won't be a problem.

[jwaldmann]

fixed rules for selecting the subsets so that not all benchmarks used come from the same group.

we've been there ... https://termination-portal.org/wiki/Termination_Competition_Problem_Selection_Algorithm

What about a "Publicity Chair", a person who is responsible for ...

That's the task of termcomp SC? If you know what this chair should do, then - become a member of the SC, and do it.