April 2024 - Termtools - lists.rwth-aachen.de

TRS format at TermComp
by Florian Frohn 13 Jun '24

13 Jun '24

Dear all, at the last WST, there were some discussions about the input format for TRSs. My takeaway was that not everyone is happy with the current XML format. So we (the TermComp SC) recently started to discuss whether the format should be changed. As far as I can see, there are three obvious options: (a) keep the current format Pro: no work Contra: not human readable (b) go back to the old format [1] (here's [2] an example) Pro: - human readable - the same format is used for other categories (e.g., Complexity of ITSs and Termination of Integer TRSs) - some tools can still parse it Contra: There were some issues with the semantics, in particular if there were several VAR sections. However, from my understanding, these issues can be resolved by forbidding more than one VAR section. (c) a new S-expression based format has been proposed for the confluence competition [3] Pro: human readable(?) Contra: no tool can parse it yet So if you compete, or are interested in, the TRS categories at TermComp, please let us know what you think. I'm also particularly interested in the following questions: - If you participate, can your tool still parse the old format? - Do you recall more details about the reasons for the switch from the old format to the current one? A related (but mostly independent) question is whether we should separate the properties to be analyzed (full vs innermost rewriting, termination vs complexity etc.) from the actual TRS. That could avoid a lot of redundancy in the TPDB. If you have an opinion on that, please share it. Thanks, Florian [1] https://www.lri.fr/~marche/tpdb/format.html [2] https://aprove.informatik.rwth-aachen.de/interface/v-AProVE2023/trs_wst [3] http://cl-informatik.uibk.ac.at/iwc/2023/proceedings.pdf, page 32

8 16

new ARI format at termCOMP '24
by Florian Frohn 26 Apr '24

26 Apr '24

Dear all, the conversion to the new ARI format is done for all first-order TRS/SRS categories [1]. The tool to convert back and forth between XTC and ARI is available here [2] (note that you have to use the branch xtc, not the master branch). Some documentation for the new format is available here [3]. If you have suggestions to improve it, please let me know. Regarding valid identifiers, there might be (hopefully minimal) changes in the (near) future. In particular, the question which identifiers should be quoted is not entirely settled. If you're interested, please participate in the corresponding discussion on Github [4]. Nevertheless, I think the current version is good enough to start testing. Let me know if you run into any problems. Best Florian [1] https://github.com/TermCOMP/TPDB-ARI [2] https://github.com/TermCOMP/ari-conversion/tree/xtc [3] https://termination-portal.org/wiki/Term_Rewriting [4] https://github.com/orgs/TermCOMP/discussions/83#discussioncomment-8676014

1 0

Termination and Complexity Competition 2024: Call for Participation
by Florian Frohn 15 Apr '24

15 Apr '24

*Termination and Complexity Competition 2024* http://www.termination-portal.org/wiki/Termination_Competition_2024 *Call for Participation* Since the beginning of the millennium, many research groups developed tools for fully automated termination and complexity analysis. After a tool demonstration at the 2003 Termination Workshop in Valencia, the community decided to start an annual termination competition to spur the development of tools and termination techniques. The termination and complexity competition focuses on automated termination and complexity analysis for all kinds of programming paradigms, including categories for term rewriting, imperative programming, logic programming, and functional programming. In all categories, we also welcome the participation of tools providing certifiable proofs. The goal of the termination and complexity competition is to demonstrate the power of the leading tools in each of these areas. The competition will be affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2024, https://merz.gitlabpages.inria.fr/2024-ijcar/). It will be run on the StarExec platform (https://www.starexec.org/). The final run and a presentation of the final results will be live at IJCAR. We strongly encourage all developers of termination and complexity analysis tools to participate in the competition. We also welcome the submission of termination and complexity problems, especially problems that come from applications. A category is only run in the competition if there are at least 2 participants and at least 40 examples for this category in the underlying termination problem data base. If there is no category that is convenient for your tool, you can contact the organizers, since other categories can be considered as well if enough participants are guaranteed. For further information, we refer to the website of the termination and complexity competition: https://termination-portal.org/wiki/Termination_Competition_2024 <https://termination-portal.org/wiki/Termination_Competition_2024> _Important dates_ * Tool and Benchmark Submission: June 12, 2024 * First Run: June 19, 2024 * Bugfix Deadline: June 26, 2024 * IJCAR: July 3-6, 2024

1 0