|
|
| (72 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> |
|
| |
|
| The first installation of this event is planned for November 1, 2008. | | The entry point to the complexity category is here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition]. |
| | |
| (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. 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.
| |
| | |
| <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.
| |
| | |
| NB: Derivational complexity is not closed under extensions
| |
| of the signature. Consider for example the TRS R={a -> b} (example suggested
| |
| by Nao Hirokawa). On the signature {a,b} the (derivational) complexity
| |
| is constant, while the complexity becomes linear on signature {a,b,c},
| |
| if the arity of c is binary. Thus, we demand that the complexity
| |
| certificate given by the provers has to be closed under extension of
| |
| signature.
| |
| | |
| == Problem selection ==
| |
| | |
| We propose the collection of all "standard" TRSs together
| |
| with all TRSs with flag "(STRATEGY INNERMOST)" as testbed. Here TRSs which
| |
| only differ by the flag in the current TPDB are only considered once.
| |
| However for sub-categories concerned with "derivational complexity" we
| |
| propose to restrict our attention to non-duplicating systems.
| |
| | |
| In the following test cases we restrict to full rewriting.
| |
| | |
| <em>Test Cases - derivational complexity </em>
| |
| *
| |
| * R= {a(b(x)) -> b(a(x))}, expected output "YES(?,O(n^2))" or "YES(O(n),O(n^2))" or "YES(O(n^2),O(n^2))"
| |
| | |
| * R= {op(op(x,y),z) -> op(x,op(y,z))}, expected output "YES(?,O(n^2))" or "YES(O(n),O(n^2))" or "YES(O(n^2),O(n^2))"
| |
| | |
| * R= {f(f(x)) -> f(g(f(x)))}, expected output "YES(?,O(n))" or "YES(O(n),O(n))"
| |
| | |
| * R= {half(0) -> 0, half(s(0)) -> 0, half(s(s(x))) -> s(half(x)), s(log(0)) -> s(0), log(s(x)) -> s(log(half(s(x))))}, expected output "YES(?,O(n^2))" or "YES(O(n),O(n^2))" or "YES(O(n^2),O(n^2))"
| |
| | |
| * R= {plus(mul(x,y),mul(x,z)) -> mul(x,plus(y,z)), plus(plus(x,y),z) -> plus(x,+(y,z)), plus(mul(x,y),plus(mul(x,z),u)) -> plus(mul(x,plus(y,z)),u)}
| |
| | |
| * 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(?,?)"
| |
| | |
| <em>Test Cases - runtime complexity </em>
| |
| *
| |
| * 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))" or "YES(O(n),O(n))"
| |
| | |
| * R= {d(0) -> 0, d(s(x)) -> s(s(d(x))), e(0) -> s(0), e(s(x)) -> d(e(x))}, expected output "YES(?,?)"
| |
| | |
| (to be extended)
| |
| | |
| == 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
| |
| | |
| F -> O(1) | O(n^Nat) | POLY | EXP | INF
| |
| | |
| 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.
| |
| | |
| * 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.
| |
| | |
| == 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)
| |
