|
|
(69 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}, expected output "YES(O(n),O(n))" of "YES(?,O(n))" (if tool output should be closed under extension of signature)
| |
− | | |
− | * 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= {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= {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= {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= {a(b(x)) -> b(b(a(x)))}, expected output "YES(?,O(n))" or "YES(O(n),O(n))"
| |
− | | |
− | * 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),O(n^2))" or "YES(O(n^2),O(n^2))"
| |
− | | |
− | * R= {if(tt,x,y) -> x, if(ff,x,y) -> y, le(0,s(y)) -> tt, le(x,0) -> ff, le(s(x),s(y)) -> le(x,y), insert(x,nil) -> cons(x,nil), insert(x,cons(y,ys)) -> if(le(x,y),cons(x,cons(y,ys)),cons(y,insert(x,ys))), sort(nil) -> nil, sort(cons(x,xs)) -> insert(x,sort(xs))}, expected output "YES(?,O(n^2))" or "YES(O(n),O(n^2))" or "YES(O(n^2),O(n^2))"
| |
− | | |
− | * R= {minus(0,y) -> 0, minus(x,0) -> x, minus(s(x),s(y)) -> minus(x,y), div(0,s(y)) -> 0, div(s(x),s(y)) -> s(div(minus(x,y),s(y)))}, expected output "YES(?,O(n))" or "YES(O(n),O(n))"
| |
− | | |
− | * 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(?,?)"
| |
− | | |
− | * R= {f(0) -> c, f(s(x)) -> c(f(x),f(x))}, expected output "YES(?,?)"
| |
− | | |
− | == 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)
| |