Dear Akihisa,

I was under the impression that those discussions were about the confluence competition, not the termination competition?

The termination competition has always used plain matching, not modulo matching, and while the argument for HRSs in the confluence case is "most papers on higher-order confluence consider modulo matching" the opposite is true when it comes to termination.  I would be very disappointed if HRSs became the de facto standard for higher-order analysis since it would throw away a vast body of work on "HOR union beta", and moreover steer future developments in a direction that makes it much harder to extend results to orders above 2.

(Side note: the page somewhat misrepresents Wanda: Wanda's format does not coincide with HRSs in the second-order case, but can represent them -- that does not mean that the power on this subset is the same.)

Cynthia.

Dear all,

I'd also like to start a discussion on higher-order categories. The proposal reflects (long) discussions with Cynthia, Frédéric, and Makoto.

https://github.com/orgs/TermCOMP/discussions/86

Main points are that there is also a simply typed TRS (STTRS) format, and that HRS category adopts HRS semantics, and restricted to 2nd order.

Best,
Akihisa

On 2024/01/15 18:23, Florian Frohn wrote:

Dear all,

in the meantime, the ARI format has been finalized [1]. I've created GitHub discussions on more concrete proposals how to adapt it for termCOMP.

All TRS categories but equational and relative rewriting:

https://github.com/orgs/TermCOMP/discussions/83

Equational Rewriting:

https://github.com/orgs/TermCOMP/discussions/84

Relative Rewriting:

https://github.com/orgs/TermCOMP/discussions/85

Please share your opinions in these discussions. In particular, please let us know if your tool would drop out of the competition due to lack of resources for implementing a parser for the ARI format.

Best
Florian


[1] http://project-coco.uibk.ac.at/ARI/index.php


On 11/15/23 10:40, Florian Frohn wrote:

Dear all,


thank you very much for your input! Let me try to summarize what we got so far:

1. Some benefits of a human-readable format have been pointed out.

2. Using an "established" format (that is also used at other competitions, e.g., SMT-LIB or the CoCo-format) would be nice.

3. Using a standardized format like XML has benefits as well, e.g., there's no need to discuss concrete syntax and one can use existing libraries.

Regarding the old TPDB format, some tools cannot parse it anymore, and it had a few quirks that were heavily discussed in the past [1].

In any case, a conversion to CeTA's new input format will be necessary. For the CoCo-format, a suitable converter is already available.

If there are other points that should be taken into account, please share them!


Best
Florian


[1] https://verify.rwth-aachen.de/termtools/2003-November/subject.html

On 11/8/23 17:39, Florian Frohn wrote:

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
_______________________________________________
Termtools mailing list -- termtools@lists.rwth-aachen.de
To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de

_______________________________________________
Termtools mailing list -- termtools@lists.rwth-aachen.de
To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de

_______________________________________________
Termtools mailing list -- termtools@lists.rwth-aachen.de
To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de

_______________________________________________
Termtools mailing list -- termtools@lists.rwth-aachen.de
To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de