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/%7Emarche/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
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.
On 08-11-2023 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/%7Emarche/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
Dear Florian, dear all,
(b) go back to the old format [1] (here's [2] an example)
...
Contra: There were some issues with the semantics,
also - cf. "Wadler's law of language design", issues with (comment) syntax (? - everything that's invalid, is accepted as comment)
for reference, early discussion is here https://verify.rwth-aachen.de/termtools/2003-November/subject.html
(c) a new S-expression based format has been proposed for the confluence competition [3]
Pro: human readable(?)
Pro: the format is used for SMTLIB as well (?)
- If you participate, can your tool still parse the old format?
matchbox - yes. https://hackage.haskell.org/package/tpdb
- Do you recall more details about the reasons for the switch from the
old format to the current one?
* avoiding discussion of concrete (surface) syntax, e.g., what is a valid identifier, a comment, etc.
* validation of termination proofs needed a (machine-readable) exchange format anyway (cf. https://verify.rwth-aachen.de/termtools/2007-May/000325.html ) but - TRS in CPF syntax (certificates) is not the same as TRS in XTC (benchmarks)? And the name is wrong ... https://verify.rwth-aachen.de/termtools/2009-December/000787.html
* XML was all the rage in the 90s - as was JSON was after that, and S-expressions before.
- Johannes.
Dear Florian,
On 11/8/2023 5:39 PM, Florian Frohn wrote:
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?
MU-TERM can deal with the original TPDB format.
- Do you recall more details about the reasons for the switch from the
old format to the current one?
From a programming perspective, utilizing standard formats like XML or JSON to define TRSs is a good idea, given the availability of libraries that facilitate the transformation of these files into data structures (not in Haskell, where we use Parsec, but in Python, for example, there are libraries to do this automatically) and also to interact between different tools. However, from a user standpoint, it is crucial that TRSs can be easy to write.
Best,
Raúl.
Dear all,
concerning the mismatch between CPF and XTC format, I can only say that this is no longer an issue:
CPF 3 has just been released and it will no longer support XTC itself, but a cleaned up variant. So competition organisers have to write a converter from their TRS-format to the CPF-input format, which should be an easy task.
Such a converter is already available for the new ARI-format, a format that will be used in CoCo starting in 2024.
For more information regarding the changes in CPF (in particular for running competitions), cf.
http://cl-informatik.uibk.ac.at/isafor/cpf3.html (overview) or http://cl-informatik.uibk.ac.at/isafor/cpf3.tgz (specification + converter)
Best, René
Am 13.11.2023 um 09:37 schrieb Raúl Gutiérrez raguti@upv.es:
Dear Florian,
On 11/8/2023 5:39 PM, Florian Frohn wrote:
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?
MU-TERM can deal with the original TPDB format.
- Do you recall more details about the reasons for the switch from the old format to the current one?
From a programming perspective, utilizing standard formats like XML or JSON to define TRSs is a good idea, given the availability of libraries that facilitate the transformation of these files into data structures (not in Haskell, where we use Parsec, but in Python, for example, there are libraries to do this automatically) and also to interact between different tools. However, from a user standpoint, it is crucial that TRSs can be easy to write.
Best,
Raúl.
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
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/%7Emarche/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
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:
Some benefits of a human-readable format have been pointed out.
Using an "established" format (that is also used at other
competitions, e.g., SMT-LIB or the CoCo-format) would be nice.
- 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/%7Emarche/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
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:
Some benefits of a human-readable format have been pointed out.
Using an "established" format (that is also used at other
competitions, e.g., SMT-LIB or the CoCo-format) would be nice.
- 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/%7Emarche/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
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.
On 16-01-2024 09:09, YAMADA, Akihisa wrote:
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:
Some benefits of a human-readable format have been pointed out.
Using an "established" format (that is also used at other
competitions, e.g., SMT-LIB or the CoCo-format) would be nice.
- 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/%7Emarche/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
Dear Cynthia,
there shouldn't be any intention towards setting a de-facto standard semantics. It's just that only 2nd-order HRS remain reachable by more than one tool.
(If I were to, I'd vote for a formalism that coincides with STTRS on lambda-free fragment, so not HRS. I also observe Isabelle's rewriting is not HRS.)
P.S. Will you mind using GitHub? It's far easier to chat than composing E-mails.
Best, Akihisa
On 2024/01/16 18:10, Cynthia Kop wrote:
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.
On 16-01-2024 09:09, YAMADA, Akihisa wrote:
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:
Some benefits of a human-readable format have been pointed out.
Using an "established" format (that is also used at other
competitions, e.g., SMT-LIB or the CoCo-format) would be nice.
- 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/%7Emarche/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
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
termtools@lists.rwth-aachen.de
-
Cynthia Kop -
Etienne Payet -
Florian Frohn -
Florian Frohn -
Johannes Waldmann -
Raúl Gutiérrez -
Thiemann, René -
YAMADA, Akihisa