Difference between revisions of "Complexity:Old"
Georg.moser (talk | contribs) |
Georg.moser (talk | contribs) |
||
Line 15: | Line 15: | ||
induced by full rewriting as opposed to complexities induced by | induced by full rewriting as opposed to complexities induced by | ||
specific strategies, as for example innermost rewriting. | specific strategies, as for example innermost rewriting. | ||
+ | We propose four sub-categories, structured in two logical layers: | ||
+ | "strategy" and "complexity certificate", such that for each of | ||
+ | the currently considered strategies, both notions of complexity are tested. | ||
== Syntax/Semantics for Input/Output == | == Syntax/Semantics for Input/Output == | ||
− | + | The current input format should be kept as far as possible, | |
+ | i.e., from a given TRS a complexity problem file is generated by | ||
+ | adding an annotation expressing one of the above given categories. This is | ||
+ | done on the fly during the competition to prevent the multiplication | ||
+ | of the database. | ||
+ | |||
+ | On the other hand the output format is adapted so that additional | ||
+ | information on the asymptotic complexity is given for lower as well | ||
+ | as upper bounds. Hence the output written to the first line of STDOUT | ||
+ | shall be a complexity statement according to the following grammar: | ||
+ | |||
+ | S -> NO | MAYBE | YES( F, F) | YES( ?, F) | YES( F, ?)<br> | ||
+ | F -> O(1) | O(n^Nat) | POLY | ||
+ | |||
+ | where "Nat" is a non-zero natural number and YES(F1, F2) means F2 is | ||
+ | upper bound and that F1 is a lower-bound. "O(n^k)" is the usual big-Oh | ||
+ | notation and "POLY" indicates an unspecified polynomial. Either of | ||
+ | the functions F1, F2 (but not both) may be replaced by ``don't know'', | ||
+ | indicated by ?. Any remaining output on STDOUT will be considered as | ||
+ | proof output and has to follow the normal rules for the competition. | ||
== Scoring == | == Scoring == | ||
− | + | ||
== Problem selection == | == Problem selection == | ||
Line 40: | Line 62: | ||
issues with the rules proposal that need to be clarified, or voted upon. | issues with the rules proposal that need to be clarified, or voted upon. | ||
+ | * | ||
+ | * the precise format for the subcategories needs to be fixed; JW suggest: | ||
+ | |||
+ | (START-TERMS CONSTRUCTOR-BASED) (VAR x) (RULES a(b(x)) -> b(a(x))) | ||
+ | |||
+ | to indicate runtime complextiy and full rewriting , GM suggests | ||
+ | |||
+ | (VAR x) (RULES a(b(x)) -> b(a(x))) (COMPLEXITY RUNTIME) | ||
+ | |||
+ | for the same thing | ||
== Participants == | == Participants == |
Revision as of 12:32, 20 October 2008
This page is to record the current status of discussion on the proposed Complexity Category of the Termination Competition.
(Discussion should take place on the termtools mailing list.)
Contents
Overview of the Event
It is a challenging topic to automatically determine upper bounds on the complexity of rewrite systems. By complexity of a TRS, we mean the maximal length of derivations, where either no restrictions on the initial terms are present ("derivational complexity") or only constructor based terms are considered ("runtime complexity"). See (Hirokawa, Moser, 2008) for further reading on the notion of runtime complexity. Additionally one distinguishes between complexities induced by full rewriting as opposed to complexities induced by specific strategies, as for example innermost rewriting. We propose four sub-categories, structured in two logical layers: "strategy" and "complexity certificate", such that for each of the currently considered strategies, both notions of complexity are tested.
Syntax/Semantics for Input/Output
The current input format should be kept as far as possible, i.e., from a given TRS a complexity problem file is generated by adding an annotation expressing one of the above given categories. This is done on the fly during the competition to prevent the multiplication of the database.
On the other hand the output format is adapted so that additional information on the asymptotic complexity is given for lower as well as upper bounds. Hence the output written to the first line of STDOUT shall be a complexity statement according to the following grammar:
S -> NO | MAYBE | YES( F, F) | YES( ?, F) | YES( F, ?)
F -> O(1) | O(n^Nat) | POLY
where "Nat" is a non-zero natural number and YES(F1, F2) means F2 is upper bound and that F1 is a lower-bound. "O(n^k)" is the usual big-Oh notation and "POLY" indicates an unspecified polynomial. Either of the functions F1, F2 (but not both) may be replaced by ``don't know, indicated by ?. Any remaining output on STDOUT will be considered as proof output and has to follow the normal rules for the competition.
Scoring
Problem selection
(to be extended)
Participation
The sources of all tools that want to participate in the competition have to be publicly available.
Wishlist
(to be extended)
Questions
issues with the rules proposal that need to be clarified, or voted upon.
- the precise format for the subcategories needs to be fixed; JW suggest:
(START-TERMS CONSTRUCTOR-BASED) (VAR x) (RULES a(b(x)) -> b(a(x)))
to indicate runtime complextiy and full rewriting , GM suggests
(VAR x) (RULES a(b(x)) -> b(a(x))) (COMPLEXITY RUNTIME)
for the same thing
Participants
insert your name here if you intend to participate
- Johannes Waldmann (Matchbox), but will need more time (December 2008)
- M. Avanzini, G. Moser, A. Schnabl (TCT)