|
|
| (90 intermediate revisions by 8 users not shown) |
| Line 1: |
Line 1: |
| This page is to record the current status of discussion | | <pre> |
| on the proposed Complexity Category of the Termination Competition.
| | This page is no longer maintained. |
| | </pre> |
|
| |
|
| (Discussion should take place on the termtools mailing list.)
| | The entry point to the complexity category is here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition]. |
| | |
| == 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, ?)<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 ==
| |
| | |
| | |
| | |
| == 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)
| |
This page is no longer maintained.
The entry point to the complexity category is here: complexity competition.
