|
|
(35 intermediate revisions by 7 users not shown) |
Line 1: |
Line 1: |
− | This page is to record the current status of discussion
| |
− | on the proposed Complexity Category of the Termination Competition.
| |
− |
| |
− | The first installation of this event is planned for November 1, 2008.
| |
− |
| |
− | (Discussion should take place on the termtools mailing list.)
| |
− |
| |
− | == 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 ==
| |
− |
| |
− | As competition semantics, we propose to focus on <em>polynomial</em>
| |
− | bounds.
| |
− |
| |
− | Although there has been some discussion, unfortunately no agreement on a
| |
− | new input format specific for the complexity category could be found.
| |
− | Hence, as ad-hoc solution for the competition on November 1, the only demand from
| |
− | the input is that it includes a well-formed description of a TRS,
| |
− | all remaining annotations will be ignored.
| |
− | To control the four subcategories, specific runme scripts are to be used.
| |
− |
| |
− | For the future, one could use an XML input format that is generated on the fly.
| |
− | The below proposal extends the current proposal of an XML import/export format,
| |
− | see [http://termination-portal.org/wiki/TPDB_XML_Format]:
| |
− |
| |
− | <pre>
| |
− | <complexity>
| |
− | <theory><theorydecl>Multiple</theorydecl></theory>
| |
− | <startterm>
| |
− | <CONSTRUCTOR-BASED/>
| |
− | <FULL/>
| |
− | <AUTOMATON>
| |
− | <automatonstuff/>
| |
− | </AUTOMATON>
| |
− | </startterm>
| |
− | <strategy>
| |
− | <INNERMOST/> |
| |
− | <OUTERMOST/> |
| |
− | <CONTEXTSENSITIVE>
| |
− | <contextsensitivestuff/>
| |
− | </CONTEXTSENSITIVE>
| |
− | |<NONE/>
| |
− | </strategy>
| |
− | <conditional type="ltr|join"/>
| |
− | <type>TRS|SRS</type>
| |
− | </complexity>
| |
− | </pre>
| |
− |
| |
− | 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:
| |
− |
| |
| <pre> | | <pre> |
− | S -> NO | MAYBE | YES( F, F) | YES( ?, F) | YES( F, ?)
| + | This page is no longer maintained. |
− | F -> O(1) | O(n^Nat) | POLY
| |
| </pre> | | </pre> |
| | | |
− | where "Nat" is a non-zero natural number and YES(F1, F2) means F2 is
| + | The entry point to the complexity category is here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition]. |
− | 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.
| |
− | | |
− | <em>Example</em>: Consider R= {a(a(x)) -> b(c(x)), b(b(x)) -> a(c(x)), c(c(x)) -> a(b(x))}. Within
| |
− | the derivational complexity category a syntactically correct output would be "YES(O(n^2),POLY)".
| |
− | (Whether this output would also indicate a correct tool, is another question.)
| |
− | | |
− | == Scoring ==
| |
− | | |
− | Currently we focus on (polynomial) <em>upper</em> bounds. As
| |
− | the output format indicates, this restriction should be lifted
| |
− | later, see below. In order to take into account the quality of the upper
| |
− | bound provided by the different tools, we propose the following
| |
− | scoring algorithm, where we suppose the number of competitors is x.
| |
− | | |
− | Firstly, for each TRS the competing tools are ranked, where constant
| |
− | complexity, i.e., output "YES(?,O(1))" is best and "MAYBE", "NO" or
| |
− | time-out is worst.
| |
− | As long as the output is of form "YES(?,O(n^k))" or "YES(?,POLY)" the
| |
− | rank of the tool defines the number of points. More precisely the
| |
− | best tool gets x+1 points, the second gets x points and so on. On the
| |
− | other hand a negative output ("MAYBE", "NO" or time-out) gets 0
| |
− | points.
| |
− | If two or more tools would get the same rank, the rank of the
| |
− | remaining tools is adapted in the usual way.
| |
− | | |
− | Secondly, all resulting points for all considered systems are summed
| |
− | up and the contestant with the highest number of points wins. If this
| |
− | cannot establish a winner, the total number of wins is counted. If
| |
− | this still doesn't produce a winner, we give up and provide two (or
| |
− | more) winners.
| |
− | | |
− | The maximal allowed CPU time is 60 seconds.
| |
− | | |
− | == Problem selection ==
| |
− | | |
− | We propose to run each complexity-subcategory
| |
− | on all TRS and SRS families from the newly organised TPDB, after
| |
− | the following selection function defined below has been applied.
| |
− | | |
− | === Selection function ===
| |
− | | |
− | In the following, we denote by ''select'' the function that relates
| |
− | each family from the TPDB to the number of randomly chosen examples within this family as defined
| |
− | for the termination competition.
| |
− | The idea is to make ''select''
| |
− | aware of different difficulties of proving complexity bounds. We do so by
| |
− | # partitioning each family ''F'' into ''n'' different sets ''F = F_1 \cup ... \cup F_n'', where the sets ''F_i'' may be seen as collections of TRSs similar in difficulty. For this years competition we propose following partitioning of a family ''F'':
| |
− | #:* '''subcategories runtime-complexity (RC), innermost runtime-complexity (iRC), and innermost derivational-complexity (iDC):''' we propose to partition each family into
| |
− | #:*:(i) those upon which a polynomial bound could be shown automatically in last years competition (denoted by ''F_auto'' below) and
| |
− | #:*:(ii) those where a polynomial bound could not be shown (''F_nonauto'').
| |
− | #:* '''subcategory derivational complexity (DC)''': as above, but we split (ii) into duplicating TRS (''F_duplicating'') and non-duplicating TRSs (note that any TRS from (i) is non-duplicating)
| |
− | # In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F'' such that ''p(F_1) + ... p(F_n) = 1''. For this year's competition we propose the following distribution:
| |
− | #:for all subcategories and families ''F'', we propose ''p(F_auto) = 0.4'' and ''p(F_nonauto) = 0.6'' (For the category DC, we additionally set ''p(F_duplicating) = 0.0''). Based on the probability distribution ''p'' we then define the extended selection function "select_comp" such that ''select_comp(F,i) = min(|F_i|, p(i) * select(F))''. Here ''|F_i|'' denotes the size of ''F_i''.
| |
− | # From each partition ''F_i'' of a family ''F'', we randomly select ''select_comp(F,i)'' examples.
| |
− | | |
− | | |
− | == Test Cases ==
| |
− | In the following test cases we restrict to full rewriting.
| |
− | <em>
| |
− | test cases - derivational complexity
| |
− | </em>
| |
− | | |
− | <pre>
| |
− | R = {a(b(x)) -> b(a(x))}, expected output "YES(?,O(n^2))" or "YES(O(n^1),O(n^2))" or "YES(O(n^2),O(n^2))"
| |
− | | |
− | R= {a(a(x)) -> b(c(x)), b(b(x)) -> a(c(x)), c(c(x)) -> a(b(x))}, expected output "YES(O(n^2),?)" or "YES(?,?)"
| |
− | | |
− | R= {+(s(x),+(y,z)) -> +(x,+(s(s(y)),z)), +(s(x),+(y,+(z,w))) -> +(x,+(z,+(y,w)))}, expected output "YES(?,?)"
| |
− | </pre>
| |
− | | |
− | <em>test cases - runtime complexity </em>
| |
− | <pre>
| |
− | R = {a(b(x)) -> b(b(a(x)))}, expected output "YES(?,O(n^1))" or "YES(O(n^1),O(n^1))"
| |
− | | |
− | R = {plus(0,y) -> y, plus(s(x),y) -> s(plus(x,y)), mul(0,y) -> 0, mul(s(x),y) -> plus(mul(x,y),y)}, expected output "YES(?,O(n^2))" or "YES(O(n^1),O(n^2))" or "YES(O(n^2),O(n^2))"
| |
− | | |
− | R = {f(x,0) -> s(0), f(s(x),s(y)) -> s(f(x,y)), g(0,x) -> g(f(x,x),x)}, expected output "YES(?,O(n^1))" or "YES(O(n^1),O(n^1))"
| |
− | | |
− | R= {f(0) -> c, f(s(x)) -> c(f(x),f(x))}, expected output "YES(?,?)"
| |
− | </pre>
| |
− | | |
− | In the following test cases we restrict to innermost rewriting.
| |
− | | |
− | <em>test cases - derivational complexity </em>
| |
− | <pre>
| |
− | R = {f(x) -> c(x,x)}, expected output "YES(O(n^1),O(n^1))" or "YES(?,O(n^1))"
| |
− | </pre>
| |
− | | |
− | <em>test cases - runtime complexity </em>
| |
− | <pre>
| |
− | R= {f(x) -> c(x,x), g(0) -> 0, g(s(x)) -> f(g(x))}, expected output "YES(O(n^1),O(n^1))" or "YES(?,O(n^1))"
| |
− | </pre>
| |
− | | |
− | == Wishlist ==
| |
− | *
| |
− | * assessment of lower bounds:<br>
| |
− | In the future the tools should also be able to provide certificates on the
| |
− | lower bound. This would imply to extend the grammar as follows
| |
− | | |
− | <pre>
| |
− | F -> O(1) | O(n^Nat) | POLY | EXP | INF
| |
− | </pre>
| |
− | | |
− | such that e.g. "YES(EXP,?)" indicated an exponential lower-bound,
| |
− | or "YES(INF,INF)" indicated non-termination.
| |
− | * as for the upper bound the lower bound certificate should be ranked and
| |
− | both ranks could be compared lexicographically
| |
− | | |
− | == Questions ==
| |
− | *
| |
− | * the precise format for the subcategories needs to be fixed; JW suggests:
| |
− | | |
− | (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 <br>
| |
− | | |
− | <em>resolved for the competition on Nov 1, see above, for suggestion of XML input format</em>
| |
− | | |
− | * JW would prefer the following output format as it is easier to parse:
| |
− | | |
− | F -> POLY(Nat) | POLY(?)
| |
− | | |
− | Here "POLY(k)" abbreviates "O(n^k)" and "POLY(?)" denotes an unspecified
| |
− | polynomial.<br>
| |
− | | |
− | <em>resolved</em>
| |
− | | |
− | == Participants ==
| |
− | | |
− | insert your name here if you intend to participate.
| |
− | The sources of all tools that want to participate in the competition
| |
− | have to be publicly available.
| |
− | | |
− | *
| |
− | * Johannes Waldmann (Matchbox), but will need more time (December 2008)
| |
− | * M. Avanzini, G. Moser, A. Schnabl (TCT)
| |
− | * N. Hirokawa (Hydra), but might need more time
| |
− | * M. Korp, C. Sternagel, H. Zankl (CaT)
| |