Termination-Portal.org - User contributions [en]

Termination Competition

2011-02-18T02:28:49Z

Hzankl: /* Annual International Termination Competition */

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an annual termination competition
to spur the development of tools and new termination techniques.

From 2004 till 2007 the competition was hosted in [http://www.lri.fr/~marche/termination-competition/ Paris].
Since 2008 the competition is hosted in [http://termcomp.uibk.ac.at Innsbruck].

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [[Complexity|complexity of term rewriting]] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
Planned extensions:
* [[Higher_Order|termination of higher order rewriting]] (under consideration)
* [[ITRS|integer term rewriting]] (under consideration)

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404&cid=1158078 Termination Competition 2010]

* [http://termcomp.uibk.ac.at/termcomp/competition/categoryList.seam?competitionId=101722&cid=51 Termination Competition 2009 (December)] [http://termcomp.uibk.ac.at/termcomp/competition/categoryList.seam?competitionId=101722&cid=51 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement], [http://termcomp.uibk.ac.at/status/rules.html Web site].

* [[Termination_Competition_2008|Termination Competition 2008]] ([[http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]])
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004]

Termination Competition

2011-02-18T02:21:16Z

Hzankl: /* History of Termination Competitions */

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the 2003 [[WST|Workshop on Termination]] in Valencia,
the community decided to install an [http://www.lri.fr/~marche/termination-competition/ annual termination competition]
to spur the development of tools and new termination techniques.

Upcoming events:

* [[Termination_Competition_2010|Termination Competition 2010 (July)]]

== Competition Categories ==

Currently, the competition features the following categories:
* termination of [[String Rewriting|string]] and [[Term Rewriting|term rewriting]]
* [[Logic_Programming|termination of logic programs]]
* [[Certified_Termination|certified termination]] of string and term rewriting (since 2007)
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [[Complexity|complexity of term rewriting]] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
Planned extensions:
* [[Higher_Order|termination of higher order rewriting]] (under consideration)
* [[ITRS|integer term rewriting]] (under consideration)

Discussion is open and primarily happens on the termtools mailing list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]].

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404&cid=1158078 Termination Competition 2010]

* [http://termcomp.uibk.ac.at/termcomp/competition/categoryList.seam?competitionId=101722&cid=51 Termination Competition 2009 (December)] [http://termcomp.uibk.ac.at/termcomp/competition/categoryList.seam?competitionId=101722&cid=51 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement], [http://termcomp.uibk.ac.at/status/rules.html Web site].

* [[Termination_Competition_2008|Termination Competition 2008]] ([[http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]])
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004]

Termination Competition 2010

2010-05-01T12:00:59Z

Hzankl: typo fixed

The 7th Termination Competition will be run during the
[http://www.floc-conference.org/IJCAR-home.html International Joint Conference on Automated Reasoning]
in July 2010.

The competition will be hosted by the
[http://cl-informatik.uibk.ac.at/ Computational Logic Research Group]
at the Institute of Computer Science of the University of Innsbruck, Austria.

Results will be available from the
[http://termcomp.uibk.ac.at/ Termination Competition/Execution Platform].

Go here for general information on [[Termination_Competition|Termination Competitions]].

Complexity Techniques

2010-03-27T18:41:03Z

Hzankl: /* Derivational Complexity */

This page is for listing all techniques applied by the participants of the complexity competitions.

'''Be aware:''' the lists are still preliminary.

== Derivational Complexity ==

{| class="wikitable" border="1"
|-
! Method
! 2008
! 2009
|-
| Arctic Interpretation
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Match Bounds
| [[Tools:CaT]]
| [[Tools:CaT]]
|-
| Matrix Interpretation Triangular
| [[Tools:CaT]], [[Tools:TCT]]
| [[Tools:CaT]], [[Tools:Matchbox]], [[Tools:TCT]]
|-
| Matrix Interpretation Non-Triangular
| ---
| [[Tools:Matchbox]]
|-
| Modular (Relative) Complexity Analysis
| ---
| [[Tools:CaT]]
|-
| Rewriting Right Hand Sides
| [[Tools:CaT]]
| [[Tools:TCT]]
|-
| Root Labeling
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|}

== Runtime Complexity ==

{| class="wikitable" border="1"
|-
! Method
! 2008
! 2009
|-
| Arctic Interpretation
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Match Bounds
| [[Tools:CaT]]
| [[Tools:CaT]]
|-
| Matrix Interpretation Triangular
| [[Tools:CaT]], [[Tools:TCT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Matrix Interpretation Non-Triangular
| ---
| ---
|-
| Modular (Relative) Complexity Analysis
| ---
| [[Tools:CaT]]
|-
| Polynomial Path Orders
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Rewriting Right Hand Sides
| [[Tools:CaT]]
| ---
|-
| Root Labeling
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Weak Dependency Pairs
| [[Tools:TCT]]
| [[Tools:TCT]]
|}

Complexity Techniques

2010-03-27T18:40:38Z

Hzankl: corrected 2009 cat methods

This page is for listing all techniques applied by the participants of the complexity competitions.

'''Be aware:''' the lists are still preliminary.

== Derivational Complexity ==

{| class="wikitable" border="1"
|-
! Method
! 2008
! 2009
|-
| Arctic Interpretation
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Match Bounds
| [[Tools:CaT]]
| [[Tools:CaT]]
|-
| Matrix Interpretation Triangular
| [[Tools:CaT]], [[Tools:TCT]]
| [[Tools:CaT]], [[Tools:Matchbox]], [[Tools:TCT]]
|-
| Matrix Interpretation Non-Triangular
| ---
| [[Tools:Matchbox]]
|-
| Modular (Relative) Complexity Analysis
| ---
| [[Tools:CaT]]
|-
| Rewriting Right Hand Sides
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Root Labeling
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|}

== Runtime Complexity ==

{| class="wikitable" border="1"
|-
! Method
! 2008
! 2009
|-
| Arctic Interpretation
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Match Bounds
| [[Tools:CaT]]
| [[Tools:CaT]]
|-
| Matrix Interpretation Triangular
| [[Tools:CaT]], [[Tools:TCT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Matrix Interpretation Non-Triangular
| ---
| ---
|-
| Modular (Relative) Complexity Analysis
| ---
| [[Tools:CaT]]
|-
| Polynomial Path Orders
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Rewriting Right Hand Sides
| [[Tools:CaT]]
| ---
|-
| Root Labeling
| [[Tools:CaT]]
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Weak Dependency Pairs
| [[Tools:TCT]]
| [[Tools:TCT]]
|}

People:Harald Zankl

2009-12-18T09:47:32Z

Hzankl:

{{Person
|firstname= Harald
|middlenames= Roman
|lastname= Zankl
|titles=
|email= firstname.lastname@uibk.ac.at
|homepage= http://cl-informatik.uibk.ac.at/~hzankl
|country= Austria
|university= University of Innsbruck
|department= Computer Science
|role=PhD
}}

People:Harald Zankl

2009-12-18T09:47:15Z

Hzankl:

{{Person
|firstname= Harald
|middlenames= Roman
|lastname= Zankl
|titles=
|email= firstname.lastname@uibk.ac.at
|homepage= http://cl-informatik.uibk.ac.at/~hzankl
|country= Austria
|university= University of Innsbruck
|department= Department of Computer Science
|role=PhD
}}

People:Harald Zankl

2009-12-18T09:46:55Z

Hzankl:

{{Person
|firstname= Harald
|middlenames= Roman
|lastname= Zankl
|titles=
|email= firstname.lastname@uibk.ac.at
|homepage= http://cl-informatik.uibk.ac.at/~hzankl
|country= Austria
|university= Innsbruck
|department= Department of Computer Science
}}

People:Harald Zankl

2009-12-18T09:46:23Z

Hzankl:

{{Person
|firstname= Harald
|middlenames= Roman
|lastname= Zankl
|titles=
|email= firstname.lastname@uibk.ac.at
|homepage= http://cl-informatik.uibk.ac.at/~hzankl
|country= Austria
|university= Innsbruck
|department= Department of Computer Science
|role= PhD
}}

Termination Competition 2008

2009-03-27T14:45:16Z

Hzankl:

From 2008 onwards, the competition will be ongoing:
submission of new problems and provers is possible anytime via...

* [http://colo5-c703.uibk.ac.at:8080/termcomp/ Termination Competition Execution Platform] ([http://lists.lri.fr/pipermail/termtools/2008-October/000511.html how to submit])

Still, there will be certain deadlines where
all data is collected and a report is produced. Upcoming deadlines are:

* (for sure) 1 November 2008
* (tentative) somewhere in May 2009 (so that a report can be presented at the Termination Workshop in June 2009)

The [Termination Problem Data Base 5.0] [http://dev.aspsimon.org/projects/termcomp/downloads/]
is used for the competition 2008.

While implementation of the execution platform is handled by the Host of the competition,
here is a separate page (a wishlist) for design issues: [[Termination_Competition_Platform]].

Complexity:Old

2008-10-30T10:47:06Z

Hzankl:

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 polynomial
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>
S -> NO | MAYBE | YES( F, F) | YES( ?, F) | YES( F, ?)
F -> O(1) | O(n^Nat) | POLY
</pre>

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.

Example: 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) upper 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 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 the sub-category concerned with "derivational complexity" and "full rewriting", we
propose to restrict our attention to non-duplicating systems. (The below given examples show
that duplicating systems in conjunction with an innermost strategy need not be of exponential
derivational complexity.)

In the following test cases we restrict to full rewriting.


test cases - derivational complexity


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

test cases - runtime complexity 
<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.

test cases - derivational complexity 
<pre>
R = {f(x) -> c(x,x)}, expected output "YES(O(n^1),O(n^1))" or "YES(?,O(n^1))"
</pre>

test cases - runtime complexity 
<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: 
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 

resolved for the competition on Nov 1, see above, for suggestion of XML input format

* 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. 

resolved

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

Complexity:Old

2008-10-29T14:00:37Z

Hzankl:

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 polynomial
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>
S -> NO | MAYBE | YES( F, F) | YES( ?, F) | YES( F, ?)
F -> O(1) | O(n^Nat) | POLY
</pre>

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.

Example: 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) upper 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 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 the sub-category concerned with "derivational complexity" and "full rewriting", we
propose to restrict our attention to non-duplicating systems. (The below given examples show
that duplicating systems in conjunction with an innermost strategy need not be of exponential
derivational complexity.)

In the following test cases we restrict to full rewriting.


test cases - derivational complexity


<pre>
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= {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>

test cases - runtime complexity 
<pre>
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 = {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= {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.

test cases - derivational complexity 
<pre>
R = {f(x) -> c(x,x)}, expected output "YES(O(n),O(n))" or "YES(?,O(n))"
</pre>

test cases - runtime complexity 
<pre>
R= {f(x) -> c(x,x), g(0) -> 0, g(s(x)) -> f(g(x))}, expected output "YES(O(n),O(n))" or "YES(?,O(n))"
</pre>

== Wishlist ==
*
* assessment of lower bounds: 
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 

resolved for the competition on Nov 1, see above, for suggestion of XML input format

* 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. 

resolved

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

News:Adding References

2008-04-08T09:04:00Z

Hzankl:

{{News
|text='''Harald''': Is there a general format which one should use when adding (one's) publications? I think that should be fixed soon in order to ensure a uniform layout.

'''Peter''': If you refer to choosing the Identifier, I would propose name+year[+a-z] for single author papers
and initials+year[+a-z] for multi author papers. If you refer to the reference itself, the usual BibTeX formats should be supported.

'''Harald''': Thx, I referred to the identifier

'''Johannes''': I am not sure I like this "references" section, because it duplicates information
(see [[Contribute]]) that is (partially) available elsewhere ([http://www.informatik.uni-trier.de/~ley/db/ DBLP]).
The logical conclusion then would be to just link to DBLP entries where this is possible,
and copy the DBLP entry format (including their naming scheme) most closely for the others.

'''Harald''': I had the same opinion first. But DBLP is a bit slow sometimes ...
|date=April 7, 2008
}}

News:Adding References

2008-04-07T18:29:44Z

Hzankl:

News:Adding References

2008-04-07T18:07:39Z

Hzankl:

News:Adding References

2008-04-07T18:05:36Z

Hzankl:

News:Adding References

2008-04-07T18:05:09Z

Hzankl:

News:Adding References

2008-04-07T17:57:27Z

Hzankl: New page: Is there a general format which one should use when adding (one's) references? I think that should be fixed soon in order to a uniform layout.

Is there a general format which one should use when adding (one's) references? I think that should be fixed soon in order to a uniform layout.

Tools:TTT2

2008-04-01T08:56:30Z

Hzankl: New page: <!-- Please fill in the data so that your tool can be added to some default categories and a simple tool page can be created. You may extend that tool page yourself af...

{{Tool
|shortname= TTT2
|longname= Tyrolean Termination Tool 2
|homepage= http://colo6-c703.uibk.ac.at/ttt2
|country= Austria
|university= Innsbruck
|developers= Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp
}}

People:Harald Zankl

2008-04-01T08:54:31Z

Hzankl:

{{Person
|firstname= Harald
|middlenames= Roman
|lastname= Zankl
|titles=
|email= firstname.lastname@uibk.ac.at
|homepage= http://cl-informatik.uibk.ac.at/~hzankl
|country= Austria
|university= Innsbruck
|department= Department of Computer Science
|role= PhD Student
}}

People:Harald Zankl

2008-04-01T08:53:56Z

Hzankl:

{{Person
|firstname= Harald
|middlenames= Roman
|lastname= Zankl
|titles=
|email= Harald dot Zankl at uibk dot ac dot at
|homepage= http://cl-informatik.uibk.ac.at/~hzankl
|country= Austria
|university= Innsbruck
|department= Department of Computer Science
|role= PhD Student
}}

People:Harald Zankl

2008-04-01T08:49:41Z

Hzankl: New page: <!-- Please fill in the data so that you can be added to some default categories and a simple user page can be created. You may extend that user page yourself after th...

{{Person
|firstname= Harald
|middlenames= Roman
|lastname= Zankl
|titles=
|email=
|homepage= cl-informatik.uibk.ac.at/~hzankl
|country= Austria
|university= Innsbruck
|department= Department of Computer Science
|role= PhD Student
}}