Dear all,
the GitHub repository is ready for termCOMP 2022 registration: https://github.com/TermCOMP/starexec-master
I hope the instruction there is clear enough. Please post questions on this list otherwise.
You can monitor the status of registration and run at http://termcomp.github.io/Y2022/
Best, Akihisa
Dear all,
Salvador proposed a new category "TRS Conditional (Termination)" (previous "TRS Conditional" will be called "TRS Conditional (Operational Termination)"). The benchmark set will be the same "TRS_Conditional".
Carsten proposed "Runtime Complexity: TRS Parallel Innermost". The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Thanks for the proposals!
... but in general, please post proposals to this list, so that potential future participants can know.
Best, Akihisa
On 6/17/2022 12:01 PM, YAMADA, Akihisa wrote:
Dear all,
the GitHub repository is ready for termCOMP 2022 registration: https://github.com/TermCOMP/starexec-master
I hope the instruction there is clear enough. Please post questions on this list otherwise.
You can monitor the status of registration and run at http://termcomp.github.io/Y2022/
Best, Akihisa
Dear René, Johannes, and participants in certified categories,
CeTA 2.42 is ready for test as post processor "ceta-2.42".
FIY: this is the bash script for the post processor: https://github.com/TermCOMP/CeTApostproc
Best, Akihisa
Dear Akihisa,
Thank you for considering the proposals!
Carsten proposed "Runtime Complexity: TRS Parallel Innermost".
The motivation for this category is to make a first step to extending termCOMP from sequential to parallel computation.
Some details on the specific form of parallel computation to be analysed:
* As usual, analysis of runtime complexity would consider the set of start terms with a defined function symbol at the root and constructor terms below the root (i.e., basic terms).
* The parallel-innermost rewrite relation is given by a variant of innermost term rewriting in which all innermost redexes are contracted simultaneously.
A formal definition is available, e.g., in Definition 3 of
Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio: Orderings for Innermost Termination. RTA 2005: 17-31
https://doi.org/10.1007/978-3-540-32033-3_3 https://www.lsi.upc.edu/%7Ealbert/papers/rta2005.pdf
* The runtime complexity function is defined analogously to runtime complexity for other rewrite strategies, but using the parallel-innermost rewrite relation.
... but in general, please post proposals to this list, so that potential future participants can know.
Excellent point!
The parallel-innermost rewrite relation is a subset of the transitive closure of the innermost rewrite relation (every parallel-innermost step can be simulated by one or more innermost steps). Thus, an upper bound for innermost runtime complexity is also a valid upper bound for parallel-innermost runtime complexity.
This means that *any* complexity analysis tool that is able to find upper bounds for innermost runtime complexity can join this new category with only a small adjustment to the tool's parser.
The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Here, I would propose using only a subset of the existing benchmark set "Runtime_Complexity_Innermost_Rewriting". The reason is that for many TRSs, the innermost and the parallel-innermost rewrite relation on terms reachable from basic terms as start terms are provably identical (thus, also innermost runtime complexity and parallel-innermost runtime complexity are identical for these TRSs).
This property can be checked syntactically. In version 11.2 of the TPDB, for 369 out of 663 TRSs, innermost and parallel-innermost rewriting from basic terms define the same relation. Thus, it is the remaining 294 TRSs where an analysis of parallel-innermost runtime complexity would be of specific interest.
The following paper describes specific techniques to approximate the runtime complexity function for parallel-innermost rewriting, both by lower bounds and by potentially tighter upper bounds than those given by innermost runtime complexity:
Thaïs Baudon, Carsten Fuhs, Laure Gonnord Analysing Parallel Complexity of Term Rewriting In Proc. LOPSTR 2022. To appear.
The final version of the paper is currently in preparation. An overview of the results is available in the following slide deck presented at the TeReSe workshop in Nijmegen on 8 June 2022:
https://deividrvale.github.io/assets/pdf/terese2022/slides_carsten.pdf
This slide deck includes (on slide 10) also the syntactic check (and its proof idea) to detect TRSs where innermost and parallel-innermost rewriting from basic terms coincide.
I will also give a presentation about this proposal for a new category (and why it is interesting!) at the Workshop on Termination on 11/12 August 2022.
Best regards,
Carsten
On 20/06/2022 07:31, YAMADA, Akihisa wrote:
Dear all,
Salvador proposed a new category "TRS Conditional (Termination)" (previous "TRS Conditional" will be called "TRS Conditional (Operational Termination)"). The benchmark set will be the same "TRS_Conditional".
Carsten proposed "Runtime Complexity: TRS Parallel Innermost". The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Thanks for the proposals!
... but in general, please post proposals to this list, so that potential future participants can know.
Best, Akihisa
On 6/17/2022 12:01 PM, YAMADA, Akihisa wrote:
Dear all,
the GitHub repository is ready for termCOMP 2022 registration: https://github.com/TermCOMP/starexec-master
I hope the instruction there is clear enough. Please post questions on this list otherwise.
You can monitor the status of registration and run at http://termcomp.github.io/Y2022/
Best, Akihisa
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
WARNING: This email originated from outside of Birkbeck. Do not click links or open attachments unless you recognise the sender. Under testing so any comments sg@dcs.bbk.ac.uk
Dear all,
Thanks Carsten for your message.
Following Akihisa's suggestion, I would also like to say something about my proposal of a termination category for CTRSs.
Actually, I first addressed my proposal to TermCOMP SC because I thought this would be the right way to do it. I'm happy to share this with everybody.
During the last year we have been investigating confluence of CTRSs.
As a consequence of this research, we understood that, besides simplifyingness, decreasingness, and operational termination, termination of CTRSs (i.e., the absence of infinite ->-sequences) plays an important role in this field. Although this is not new and other researchers have noticed the point in the past, see, e.g.,
https://doi.org/10.1007/3-540-19242-5_3
https://doi.org/10.1007/3-540-60381-6_10
among others, termination tools have payed scant attention to the issue.
MU-TERM implements a number of techniques for proving termination of CTRSs, some on them based on an extended notion of dependency pair as explained here
https://doi.org/10.1016/j.jlamp.2016.03.003 https://doi.org/10.1016/j.jcss.2018.04.002
Our aim is to encourage other teams to work on this problem as it is also relevant in the analysis of computational properties of CTRSs, in particular, confluence.
Best regards,
Salvador.
El 1/7/22 a las 17:11, Carsten Fuhs escribió:
Dear Akihisa,
Thank you for considering the proposals!
Carsten proposed "Runtime Complexity: TRS Parallel Innermost".
The motivation for this category is to make a first step to extending termCOMP from sequential to parallel computation.
Some details on the specific form of parallel computation to be analysed:
- As usual, analysis of runtime complexity would consider the set of
start terms with a defined function symbol at the root and constructor terms below the root (i.e., basic terms).
- The parallel-innermost rewrite relation is given by a variant of
innermost term rewriting in which all innermost redexes are contracted simultaneously.
A formal definition is available, e.g., in Definition 3 of
Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio: Orderings for Innermost Termination. RTA 2005: 17-31
https://doi.org/10.1007/978-3-540-32033-3_3 https://www.lsi.upc.edu/%7Ealbert/papers/rta2005.pdf
- The runtime complexity function is defined analogously to runtime
complexity for other rewrite strategies, but using the parallel-innermost rewrite relation.
... but in general, please post proposals to this list, so that potential future participants can know.
Excellent point!
The parallel-innermost rewrite relation is a subset of the transitive closure of the innermost rewrite relation (every parallel-innermost step can be simulated by one or more innermost steps). Thus, an upper bound for innermost runtime complexity is also a valid upper bound for parallel-innermost runtime complexity.
This means that *any* complexity analysis tool that is able to find upper bounds for innermost runtime complexity can join this new category with only a small adjustment to the tool's parser.
The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Here, I would propose using only a subset of the existing benchmark set "Runtime_Complexity_Innermost_Rewriting". The reason is that for many TRSs, the innermost and the parallel-innermost rewrite relation on terms reachable from basic terms as start terms are provably identical (thus, also innermost runtime complexity and parallel-innermost runtime complexity are identical for these TRSs).
This property can be checked syntactically. In version 11.2 of the TPDB, for 369 out of 663 TRSs, innermost and parallel-innermost rewriting from basic terms define the same relation. Thus, it is the remaining 294 TRSs where an analysis of parallel-innermost runtime complexity would be of specific interest.
The following paper describes specific techniques to approximate the runtime complexity function for parallel-innermost rewriting, both by lower bounds and by potentially tighter upper bounds than those given by innermost runtime complexity:
Thaïs Baudon, Carsten Fuhs, Laure Gonnord Analysing Parallel Complexity of Term Rewriting In Proc. LOPSTR 2022. To appear.
The final version of the paper is currently in preparation. An overview of the results is available in the following slide deck presented at the TeReSe workshop in Nijmegen on 8 June 2022:
https://deividrvale.github.io/assets/pdf/terese2022/slides_carsten.pdf
This slide deck includes (on slide 10) also the syntactic check (and its proof idea) to detect TRSs where innermost and parallel-innermost rewriting from basic terms coincide.
I will also give a presentation about this proposal for a new category (and why it is interesting!) at the Workshop on Termination on 11/12 August 2022.
Best regards,
Carsten
On 20/06/2022 07:31, YAMADA, Akihisa wrote:
Dear all,
Salvador proposed a new category "TRS Conditional (Termination)" (previous "TRS Conditional" will be called "TRS Conditional (Operational Termination)"). The benchmark set will be the same "TRS_Conditional".
Carsten proposed "Runtime Complexity: TRS Parallel Innermost". The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Thanks for the proposals!
... but in general, please post proposals to this list, so that potential future participants can know.
Best, Akihisa
On 6/17/2022 12:01 PM, YAMADA, Akihisa wrote:
Dear all,
the GitHub repository is ready for termCOMP 2022 registration: https://github.com/TermCOMP/starexec-master
I hope the instruction there is clear enough. Please post questions on this list otherwise.
You can monitor the status of registration and run at http://termcomp.github.io/Y2022/
Best, Akihisa
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
WARNING: This email originated from outside of Birkbeck. Do not click links or open attachments unless you recognise the sender. Under testing so any comments sg@dcs.bbk.ac.uk
Dear Carsten,
thank you for the detail.
The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Here, I would propose using only a subset of the existing benchmark set "Runtime_Complexity_Innermost_Rewriting".
This is due to a (rather strong) request of the TPDB organizer (me) to avoid clones.
In near future, TPDB and COPS (https://cops.uibk.ac.at/) might get a unified back-end. Then we should be able to tell what categories each benchmark is for. Please wait until then.
Best, Akihisa
This property can be checked syntactically. In version 11.2 of the TPDB, for 369 out of 663 TRSs, innermost and parallel-innermost rewriting from basic terms define the same relation. Thus, it is the remaining 294 TRSs where an analysis of parallel-innermost runtime complexity would be of specific interest.
The following paper describes specific techniques to approximate the runtime complexity function for parallel-innermost rewriting, both by lower bounds and by potentially tighter upper bounds than those given by innermost runtime complexity:
Thaïs Baudon, Carsten Fuhs, Laure Gonnord Analysing Parallel Complexity of Term Rewriting In Proc. LOPSTR 2022. To appear.
The final version of the paper is currently in preparation. An overview of the results is available in the following slide deck presented at the TeReSe workshop in Nijmegen on 8 June 2022:
https://jpn01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdeividrval...
This slide deck includes (on slide 10) also the syntactic check (and its proof idea) to detect TRSs where innermost and parallel-innermost rewriting from basic terms coincide.
I will also give a presentation about this proposal for a new category (and why it is interesting!) at the Workshop on Termination on 11/12 August 2022.
Best regards,
Carsten
On 20/06/2022 07:31, YAMADA, Akihisa wrote:
Dear all,
Salvador proposed a new category "TRS Conditional (Termination)" (previous "TRS Conditional" will be called "TRS Conditional (Operational Termination)"). The benchmark set will be the same "TRS_Conditional".
Carsten proposed "Runtime Complexity: TRS Parallel Innermost". The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Thanks for the proposals!
... but in general, please post proposals to this list, so that potential future participants can know.
Best, Akihisa
On 6/17/2022 12:01 PM, YAMADA, Akihisa wrote:
Dear all,
the GitHub repository is ready for termCOMP 2022 registration: https://jpn01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com...
I hope the instruction there is clear enough. Please post questions on this list otherwise.
You can monitor the status of registration and run at https://jpn01.safelinks.protection.outlook.com/?url=http%3A%2F%2Ftermcomp.gi...
Best, Akihisa
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
WARNING: This email originated from outside of Birkbeck. Do not click links or open attachments unless you recognise the sender. Under testing so any comments sg@dcs.bbk.ac.uk
Dear Akihisa,
This is due to a (rather strong) request of the TPDB organizer (me) to avoid clones.
Thank you for taking the initiative on this matter! I think that this is a very sensible request.
If I understand correctly, the issue is that currently each benchmark in the TPDB consists of two elements:
(1) The program (TRS, logic program, Haskell program, LLVM program, Java Bytecode program, ...), and:
(2) The property of the program that should be analysed.
(Here it is debatable whether a strategy annotation for a TRS like "innermost" belongs rather to (1) or to (2). Perhaps (2) is more suitable - innermost runtime complexity and full runtime complexity are different properties of the same set of TRS rules.)
As an example for the number of clones, consider AG01/#3.53.xml:
$ find TPDB -name "#3.53.xml" TPDB/Runtime_Complexity_Full_Rewriting/AG01/#3.53.xml TPDB/TRS_Standard/AG01/#3.53.xml TPDB/Derivational_Complexity_Innermost_Rewriting/AG01/#3.53.xml TPDB/Runtime_Complexity_Innermost_Rewriting/AG01/#3.53.xml
In addition to these four clones with the same rewrite rules, my suggestion for analysis of parallel-innermost runtime complexity would add a fifth clone of the benchmark, where only the rewrite strategy would change over the benchmark in category Runtime_Complexity_Innermost_Rewriting.
It would indeed make sense to store just /one/ copy of the TRS rules together with an annotation of the set of properties that are considered interesting to analyse at termCOMP.
Would the input format for termCOMP participants change? Participating tools are currently expecting (1) and (2) to be both present in the same file.
In near future, TPDB and COPS (https://cops.uibk.ac.at/) might get a unified back-end. Then we should be able to tell what categories each benchmark is for. Please wait until then.
Sounds good. I will wait for further instructions regarding the desired format before I submit a pull request.
Best regards,
Carsten
On 03/07/2022 08:36, YAMADA, Akihisa wrote:
Dear Carsten,
thank you for the detail.
The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Here, I would propose using only a subset of the existing benchmark set "Runtime_Complexity_Innermost_Rewriting".
This is due to a (rather strong) request of the TPDB organizer (me) to avoid clones.
In near future, TPDB and COPS (https://cops.uibk.ac.at/) might get a unified back-end. Then we should be able to tell what categories each benchmark is for. Please wait until then.
Best, Akihisa
This property can be checked syntactically. In version 11.2 of the TPDB, for 369 out of 663 TRSs, innermost and parallel-innermost rewriting from basic terms define the same relation. Thus, it is the remaining 294 TRSs where an analysis of parallel-innermost runtime complexity would be of specific interest.
The following paper describes specific techniques to approximate the runtime complexity function for parallel-innermost rewriting, both by lower bounds and by potentially tighter upper bounds than those given by innermost runtime complexity:
Thaïs Baudon, Carsten Fuhs, Laure Gonnord Analysing Parallel Complexity of Term Rewriting In Proc. LOPSTR 2022. To appear.
The final version of the paper is currently in preparation. An overview of the results is available in the following slide deck presented at the TeReSe workshop in Nijmegen on 8 June 2022:
https://jpn01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdeividrval...
This slide deck includes (on slide 10) also the syntactic check (and its proof idea) to detect TRSs where innermost and parallel-innermost rewriting from basic terms coincide.
I will also give a presentation about this proposal for a new category (and why it is interesting!) at the Workshop on Termination on 11/12 August 2022.
Best regards,
Carsten
On 20/06/2022 07:31, YAMADA, Akihisa wrote:
Dear all,
Salvador proposed a new category "TRS Conditional (Termination)" (previous "TRS Conditional" will be called "TRS Conditional (Operational Termination)"). The benchmark set will be the same "TRS_Conditional".
Carsten proposed "Runtime Complexity: TRS Parallel Innermost". The benchmark set will be "Runtime_Complexity_Innermost_Rewriting".
Thanks for the proposals!
... but in general, please post proposals to this list, so that potential future participants can know.
Best, Akihisa
On 6/17/2022 12:01 PM, YAMADA, Akihisa wrote:
Dear all,
the GitHub repository is ready for termCOMP 2022 registration: https://jpn01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com...
I hope the instruction there is clear enough. Please post questions on this list otherwise.
You can monitor the status of registration and run at https://jpn01.safelinks.protection.outlook.com/?url=http%3A%2F%2Ftermcomp.gi...
Best, Akihisa
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
WARNING: This email originated from outside of Birkbeck. Do not click links or open attachments unless you recognise the sender. Under testing so any comments sg@dcs.bbk.ac.uk
WARNING: This email originated from outside of Birkbeck. Do not click links or open attachments unless you recognise the sender. Under testing so any comments sg@dcs.bbk.ac.uk
termtools@lists.rwth-aachen.de
-
Carsten Fuhs -
Salvador Lucas -
YAMADA, Akihisa -
YAMADA, Akihisa