Hello Florian,

> - If you participate, can your tool still parse the old format?

The XML format was introduced before the higher-order competition was, so Wanda cannot parse the human-readable variant of the higher-order format. However, I would be in favour of changing the higher-order format used in the competition altogether (although that's a separate discussion), and at that point we might as well go for a human-readable presentation instead.

(Wanda can parse the human-readable variant of the first-order format, but is not a competitor in those categories.)

Personally, I strongly prefer a format that a human can read and, most importantly, write by hand to quickly test examples, and even if the higher-order format isn't changed I'd gladly sacrifice the time to change Wanda's parser if it meant I could test other tools on a given example without having to jump through hoops to translate it to XML first. I also think it would be a good idea for the termination and confluence competition to do the same.

Cynthia.

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