|
|
(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)
| |