Termination-Portal.org - User contributions [en]

WST

2012-09-30T22:47:17Z

Georg.moser:

The International Workshop on Termination (WST) has been held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), Paris (2007), and Leipzig (2009).
WST traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* Joint Workshop on Termination (WST) and on Foundational and Practical Aspects of Resource Analysis (FOPARA), August 28-31, Bertinoro, Italy.

Information about previous workshops can be found online:
* [http://cl-informatik.uibk.ac.at/users/georg/events/wst2012 12th International Workshop on Termination, Obergurgl, February 19-23, 2012]
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

Complexity

2012-06-28T11:01:41Z

Georg.moser:

<pre>
This page is outdated and no longer maintained.
</pre>

An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition complexity competition].

----

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
discussion and rules page; aficionados
may be interested in the techniques page.

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

[[Category:Categories]]

Complexity

2012-06-08T12:08:56Z

Georg.moser:

<pre>
This page is outdated an no longer maintained.
</pre>

An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition complexity competition].

----

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
discussion and rules page; aficionados
may be interested in the techniques page.

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

[[Category:Categories]]

Complexity:Old

2012-06-08T12:05:40Z

Georg.moser: Replaced content with "<pre> This page is no longer maintained. </pre> The entry point to the complexity category is here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complex..."

<pre>
This page is no longer maintained.
</pre>

The entry point to the complexity category is here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition].

Complexity

2012-06-08T12:00:14Z

Georg.moser:

<pre>
This page is outdated an no longer maintained.
</pre>

An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition complexity competition].

----

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
discussion and rules page; aficionados
may be interested in the techniques page.

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity

2012-06-08T11:59:59Z

Georg.moser:

<pre>
This page is outdated an no longer maintained.
</pre>

An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition].

----

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
discussion and rules page; aficionados
may be interested in the techniques page.

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity:Techniques

2012-06-08T11:59:00Z

Georg.moser:

<pre>
This page is outdated an no longer maintained.
</pre>

An up to date version of the content of this page can now be found here:
[http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition].

----

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 center" border="1" style="text-align:left"
|-
! width="350"|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 center" border="1" style="text-align:left"
|-
! width="350"|Method
! 2008
! 2009
! 2010
|-
| Arctic Interpretation
| ---
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Match Bounds
| ---
| [[Tools:CaT]]
|-
| Matrix Interpretation Triangular
| [[Tools:TCT]]
| [[Tools:CaT]], [[Tools:TCT]]
| [[Tools:AProVE]]
|-
| Matrix Interpretation Non-Triangular
| ---
| ---
|-
| Modular (Relative) Complexity Analysis
| ---
| [[Tools:CaT]]
|-
| Polynomial Interpretations
| ---
| ---
| [[Tools:AProVE]]
|-
| Polynomial Path Orders
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Rewriting Right Hand Sides
| ---
| ---
|-
| Root Labeling
| ---
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Weak Dependency Pairs
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Dependency Tuples
|
|
| [[Tools:AProVE]]
|}

Complexity:Rules

2012-06-08T11:58:09Z

Georg.moser:

<pre>
This page is outdated an no longer maintained.
</pre>

An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition].

----

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
==== Testbeds ====

All authors of complexity tools that participated in the last
complexity competition agreed upon
the following selection of examples from the TPDB. For simplicity,
we decided on
using the same testbed for full and innermost rewriting. However, we
decided on
two separate testbeds for derivational and runtime complexity
analysis. The testbeds
are described below in detail, additionally a list of
problems for TPDB version 8.0 is provided for [[File:RC-8.0.txt|RC]] and [[File:DC-8.0.txt|DC]]. For the
individual
subcategories RC, RCi, DC and DCi all strategy and start-term
annotations should be overwritten
appropriately. Thus we simply ignore for instance
context-sensitive strategies.

===== Derivational Complexity =====
For derivational complexity analysis we restrict the TPDB as follows:
# keep only one instance of duplicated problems (modulo strategy annotations). A list of the TRSs that appear multiple times in the current TPDB version 8.0 can be found [[File:duplicates-8.0.txt|here]].
# remove all problems with relative, theory or conditional annotations. The reason for this is that none of the tools can handle those problems currently.

===== Runtime Complexity =====
For runtime complexity analysis, we further restrict the testbed for derivational complexity analysis as follows:
# remove all examples as determined by the tool Oops that participated in the competition of 2010. A list of these examples for TPDB version 8.0 can be found [[File:Oops-8.0.txt|here]]. This step aims at eliminating trivial problems that
## admit only 0-ary constructors, or
## admit only 0-ary defined function symbols, or
## admit only rules with nested defined function symbols on left-hand sides, thus all basic terms are normal forms.
# remove higher-order examples from following folder, as here the notion of runtime complexity is inapropriate:
## AotoYamada_05,
## Applicative_05,
## Applicative_AG01_innermost,
## Applicative_first_order_05, and
## Mixed_HO_10.

==== Selection function ====
On the above described testbeds, a randomly chosen subset that is actually used in the competition is determined as follows.
Here 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'':
#:* 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'').
# In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F''. 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''. That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity:Rules

2012-06-08T11:57:53Z

Georg.moser:

<pre>
This page is outdated an no longer maintained.
</pre>

An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].

----

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
==== Testbeds ====

All authors of complexity tools that participated in the last
complexity competition agreed upon
the following selection of examples from the TPDB. For simplicity,
we decided on
using the same testbed for full and innermost rewriting. However, we
decided on
two separate testbeds for derivational and runtime complexity
analysis. The testbeds
are described below in detail, additionally a list of
problems for TPDB version 8.0 is provided for [[File:RC-8.0.txt|RC]] and [[File:DC-8.0.txt|DC]]. For the
individual
subcategories RC, RCi, DC and DCi all strategy and start-term
annotations should be overwritten
appropriately. Thus we simply ignore for instance
context-sensitive strategies.

===== Derivational Complexity =====
For derivational complexity analysis we restrict the TPDB as follows:
# keep only one instance of duplicated problems (modulo strategy annotations). A list of the TRSs that appear multiple times in the current TPDB version 8.0 can be found [[File:duplicates-8.0.txt|here]].
# remove all problems with relative, theory or conditional annotations. The reason for this is that none of the tools can handle those problems currently.

===== Runtime Complexity =====
For runtime complexity analysis, we further restrict the testbed for derivational complexity analysis as follows:
# remove all examples as determined by the tool Oops that participated in the competition of 2010. A list of these examples for TPDB version 8.0 can be found [[File:Oops-8.0.txt|here]]. This step aims at eliminating trivial problems that
## admit only 0-ary constructors, or
## admit only 0-ary defined function symbols, or
## admit only rules with nested defined function symbols on left-hand sides, thus all basic terms are normal forms.
# remove higher-order examples from following folder, as here the notion of runtime complexity is inapropriate:
## AotoYamada_05,
## Applicative_05,
## Applicative_AG01_innermost,
## Applicative_first_order_05, and
## Mixed_HO_10.

==== Selection function ====
On the above described testbeds, a randomly chosen subset that is actually used in the competition is determined as follows.
Here 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'':
#:* 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'').
# In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F''. 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''. That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity

2012-06-08T11:57:29Z

Georg.moser:

<pre>
This page is outdated an no longer maintained.
</pre>

An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition].

----

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity:Old

2012-06-08T11:56:53Z

Georg.moser:

<pre>
This page is no longer maintained.
</pre>

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:
# Derivational Complexity (DC),
# innermost Derivational Complexity (iDC),
# Runtime Complexity (RC), and
# innermost Runtime Complexity (iRC)

== Syntax/Semantics for Input/Output ==

As competition semantics, we propose to focus on polynomial
bounds.

=== Input Format ===
Problems will be given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based
respectively.
In particluar, this allows the upload of one single tool for all categories the authors want to participate in.

=== Output Format ===
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 to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

=== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

== Participation ==

=== Requirements ===
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.

=== Participants ===

Insert your name here if you intend to participate:

==== Competition 2009 ====
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)

==== Competition 2008 ====
* M. Avanzini, G. Moser, A. Schnabl (TCT)
* M. Korp, C. Sternagel, H. Zankl (CaT)

== Complexity proof techniques ==

A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]

== Discussion ==

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

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

Scoring (proposals):

* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===

* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

[[Category:Categories]]

Complexity

2012-06-08T11:52:13Z

Georg.moser:

<pre>
This page is outdated an no longer maintained. An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition].
</pre>

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity:Old

2012-06-08T11:48:33Z

Georg.moser:

<pre>
This page is no longer maintained. The entry point to the complexity category is here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competiton].or the time beeing.
</pre>

== 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:
# Derivational Complexity (DC),
# innermost Derivational Complexity (iDC),
# Runtime Complexity (RC), and
# innermost Runtime Complexity (iRC)

== Syntax/Semantics for Input/Output ==

As competition semantics, we propose to focus on polynomial
bounds.

=== Input Format ===
Problems will be given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based
respectively.
In particluar, this allows the upload of one single tool for all categories the authors want to participate in.

=== Output Format ===
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 to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

=== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

== Participation ==

=== Requirements ===
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.

=== Participants ===

Insert your name here if you intend to participate:

==== Competition 2009 ====
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)

==== Competition 2008 ====
* M. Avanzini, G. Moser, A. Schnabl (TCT)
* M. Korp, C. Sternagel, H. Zankl (CaT)

== Complexity proof techniques ==

A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]

== Discussion ==

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

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

Scoring (proposals):

* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===

* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

[[Category:Categories]]

Complexity:Old

2012-06-08T11:48:22Z

Georg.moser:

<pre>
This page is no longer maintained.
The entry point to the complexity category is here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competiton].or the time beeing.
</pre>

== 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:
# Derivational Complexity (DC),
# innermost Derivational Complexity (iDC),
# Runtime Complexity (RC), and
# innermost Runtime Complexity (iRC)

== Syntax/Semantics for Input/Output ==

As competition semantics, we propose to focus on polynomial
bounds.

=== Input Format ===
Problems will be given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based
respectively.
In particluar, this allows the upload of one single tool for all categories the authors want to participate in.

=== Output Format ===
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 to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

=== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

== Participation ==

=== Requirements ===
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.

=== Participants ===

Insert your name here if you intend to participate:

==== Competition 2009 ====
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)

==== Competition 2008 ====
* M. Avanzini, G. Moser, A. Schnabl (TCT)
* M. Korp, C. Sternagel, H. Zankl (CaT)

== Complexity proof techniques ==

A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]

== Discussion ==

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

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

Scoring (proposals):

* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===

* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

[[Category:Categories]]

News:Complexity Wiki Moved

2012-06-08T11:47:06Z

Georg.moser: Created page with " <!-- Please insert the corresponding information below so that the news page can be generated automatically. Line breaks are allowed! You may use MediaWiki syntax h..."

The complexity wiki has been moved to the [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity competition] at
the University of Innsbruck.

{{News
|text=Complexity Wiki Moved
|date=June 8, 2012
}}

Termination Competition

2012-06-08T11:42:27Z

Georg.moser:

= 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].

== Upcoming Competition ==

The [[Termination_Competition_2012|Termination Competition 2012]] is a satellite event of [http://ijcar.cs.manchester.ac.uk/ IJCAR] (June 26 - July 1).

== 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)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity of rewrite systems] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
Planned extensions:
* [[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:

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715&cid=4874 results]

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

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722&cid=285 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991&cid=4881 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

Termination Competition

2012-06-08T11:41:44Z

Georg.moser:

= 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].

== Upcoming Competition ==

The [[Termination_Competition_2012|Termination Competition 2012]] is a satellite event of [http://ijcar.cs.manchester.ac.uk/ IJCAR] (June 26 - July 1).

== 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 of rewrite systems [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
Planned extensions:
* [[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:

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715&cid=4874 results]

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

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722&cid=285 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991&cid=4881 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

Termination Competition

2012-06-08T11:40:50Z

Georg.moser:

= 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].

== Upcoming Competition ==

The [[Termination_Competition_2012|Termination Competition 2012]] is a satellite event of [http://ijcar.cs.manchester.ac.uk/ IJCAR] (June 26 - July 1).

== 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)
* [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/] (since 2008)
* [[Java_Bytecode|termination of java bytecode programs]] (since 2009)
* [[Higher_Order|termination of higher order rewriting]] (since 2010)
Planned extensions:
* [[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:

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715&cid=4874 results]

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

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722&cid=285 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991&cid=4881 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

Complexity:Techniques

2012-06-08T11:39:35Z

Georg.moser:

<pre>
This page is outdated an no longer maintained. An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].
</pre>

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 center" border="1" style="text-align:left"
|-
! width="350"|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 center" border="1" style="text-align:left"
|-
! width="350"|Method
! 2008
! 2009
! 2010
|-
| Arctic Interpretation
| ---
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Match Bounds
| ---
| [[Tools:CaT]]
|-
| Matrix Interpretation Triangular
| [[Tools:TCT]]
| [[Tools:CaT]], [[Tools:TCT]]
| [[Tools:AProVE]]
|-
| Matrix Interpretation Non-Triangular
| ---
| ---
|-
| Modular (Relative) Complexity Analysis
| ---
| [[Tools:CaT]]
|-
| Polynomial Interpretations
| ---
| ---
| [[Tools:AProVE]]
|-
| Polynomial Path Orders
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Rewriting Right Hand Sides
| ---
| ---
|-
| Root Labeling
| ---
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Weak Dependency Pairs
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Dependency Tuples
|
|
| [[Tools:AProVE]]
|}

Complexity:Rules

2012-06-08T11:38:47Z

Georg.moser:

<pre>
This page is outdated an no longer maintained. An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].
</pre>

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
==== Testbeds ====

All authors of complexity tools that participated in the last
complexity competition agreed upon
the following selection of examples from the TPDB. For simplicity,
we decided on
using the same testbed for full and innermost rewriting. However, we
decided on
two separate testbeds for derivational and runtime complexity
analysis. The testbeds
are described below in detail, additionally a list of
problems for TPDB version 8.0 is provided for [[File:RC-8.0.txt|RC]] and [[File:DC-8.0.txt|DC]]. For the
individual
subcategories RC, RCi, DC and DCi all strategy and start-term
annotations should be overwritten
appropriately. Thus we simply ignore for instance
context-sensitive strategies.

===== Derivational Complexity =====
For derivational complexity analysis we restrict the TPDB as follows:
# keep only one instance of duplicated problems (modulo strategy annotations). A list of the TRSs that appear multiple times in the current TPDB version 8.0 can be found [[File:duplicates-8.0.txt|here]].
# remove all problems with relative, theory or conditional annotations. The reason for this is that none of the tools can handle those problems currently.

===== Runtime Complexity =====
For runtime complexity analysis, we further restrict the testbed for derivational complexity analysis as follows:
# remove all examples as determined by the tool Oops that participated in the competition of 2010. A list of these examples for TPDB version 8.0 can be found [[File:Oops-8.0.txt|here]]. This step aims at eliminating trivial problems that
## admit only 0-ary constructors, or
## admit only 0-ary defined function symbols, or
## admit only rules with nested defined function symbols on left-hand sides, thus all basic terms are normal forms.
# remove higher-order examples from following folder, as here the notion of runtime complexity is inapropriate:
## AotoYamada_05,
## Applicative_05,
## Applicative_AG01_innermost,
## Applicative_first_order_05, and
## Mixed_HO_10.

==== Selection function ====
On the above described testbeds, a randomly chosen subset that is actually used in the competition is determined as follows.
Here 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'':
#:* 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'').
# In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F''. 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''. That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity

2012-06-08T11:38:24Z

Georg.moser:

<pre>
This page is outdated an no longer maintained. An up to date version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].
</pre>

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity:Techniques

2012-06-08T11:35:35Z

Georg.moser:

== News Flash ==

This page is seriously outdated. An up-to-date version can be found here:
[http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/]

----

his 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 center" border="1" style="text-align:left"
|-
! width="350"|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 center" border="1" style="text-align:left"
|-
! width="350"|Method
! 2008
! 2009
! 2010
|-
| Arctic Interpretation
| ---
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Match Bounds
| ---
| [[Tools:CaT]]
|-
| Matrix Interpretation Triangular
| [[Tools:TCT]]
| [[Tools:CaT]], [[Tools:TCT]]
| [[Tools:AProVE]]
|-
| Matrix Interpretation Non-Triangular
| ---
| ---
|-
| Modular (Relative) Complexity Analysis
| ---
| [[Tools:CaT]]
|-
| Polynomial Interpretations
| ---
| ---
| [[Tools:AProVE]]
|-
| Polynomial Path Orders
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Rewriting Right Hand Sides
| ---
| ---
|-
| Root Labeling
| ---
| [[Tools:CaT]], [[Tools:TCT]]
|-
| Weak Dependency Pairs
| [[Tools:TCT]]
| [[Tools:TCT]]
|-
| Dependency Tuples
|
|
| [[Tools:AProVE]]
|}

Complexity:Rules

2012-06-08T11:34:00Z

Georg.moser:

This page is outdated, and an updated version of the content of this page can now be found here: [1].

----

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
==== Testbeds ====

All authors of complexity tools that participated in the last
complexity competition agreed upon
the following selection of examples from the TPDB. For simplicity,
we decided on
using the same testbed for full and innermost rewriting. However, we
decided on
two separate testbeds for derivational and runtime complexity
analysis. The testbeds
are described below in detail, additionally a list of
problems for TPDB version 8.0 is provided for [[File:RC-8.0.txt|RC]] and [[File:DC-8.0.txt|DC]]. For the
individual
subcategories RC, RCi, DC and DCi all strategy and start-term
annotations should be overwritten
appropriately. Thus we simply ignore for instance
context-sensitive strategies.

===== Derivational Complexity =====
For derivational complexity analysis we restrict the TPDB as follows:
# keep only one instance of duplicated problems (modulo strategy annotations). A list of the TRSs that appear multiple times in the current TPDB version 8.0 can be found [[File:duplicates-8.0.txt|here]].
# remove all problems with relative, theory or conditional annotations. The reason for this is that none of the tools can handle those problems currently.

===== Runtime Complexity =====
For runtime complexity analysis, we further restrict the testbed for derivational complexity analysis as follows:
# remove all examples as determined by the tool Oops that participated in the competition of 2010. A list of these examples for TPDB version 8.0 can be found [[File:Oops-8.0.txt|here]]. This step aims at eliminating trivial problems that
## admit only 0-ary constructors, or
## admit only 0-ary defined function symbols, or
## admit only rules with nested defined function symbols on left-hand sides, thus all basic terms are normal forms.
# remove higher-order examples from following folder, as here the notion of runtime complexity is inapropriate:
## AotoYamada_05,
## Applicative_05,
## Applicative_AG01_innermost,
## Applicative_first_order_05, and
## Mixed_HO_10.

==== Selection function ====
On the above described testbeds, a randomly chosen subset that is actually used in the competition is determined as follows.
Here 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'':
#:* 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'').
# In accordance to the above described partitioning, we define a probability distribution ''p'' on ''F''. 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''. That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity

2012-06-08T11:33:14Z

Georg.moser:

This page is outdated, and an updated version of the content of this page
can now be found here: [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].

----

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity

2012-06-08T11:32:41Z

Georg.moser:

This page is outdated, and an updated version of the content of this page
can now be found [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/].

----

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| x
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| x
|-
! [http://aprove.informatik.rwth-aachen.de/ AProVE]
| [[Tools:AProVE]]
| The AProVE Team
| ---
| ---
| x
|-
! Oops
| [[Tools:Oops]]
| Fabian Emmes, Lars Noschinski
| ---
| ---
| x
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

WST

2011-11-02T08:39:15Z

Georg.moser:

The International Workshop on Termination (WST) has been held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), Paris (2007), and Leipzig (2009).
WST traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [http://cl-informatik.uibk.ac.at/users/georg/events/wst2012 12th International Workshop on Termination, Obergurgl, February 19-23, 2012]

Information about previous workshops can be found online:
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

WST

2011-10-21T20:16:52Z

Georg.moser:

The International Workshop on Termination (WST) has been held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), Paris (2007), and Leipzig (2009).
WST traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* [http://cl-informatik.uibk.ac.at/users/georg/events/wst2012 12th International Workshop on Termination, Obergurgl, February 19-24, 2012]

Information about previous workshops can be found online:
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

WST

2011-04-15T14:08:49Z

Georg.moser:

The International Workshop on Termination (WST) has been held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), Paris (2007), and Leipzig (2009).
WST traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilisation of ideas from term rewriting and from the different programming language communities.

Upcoming events:
* 12th International Workshop on Termination, Obergurgl, February 19-24, 2012

Information about previous workshops can be found online:
* [http://imada.sdu.dk/~petersk/WST2010/ 11th International Workshop on Termination, Edinburgh, 2010]
* [http://www.imn.htwk-leipzig.de/wst09/ 10th International Workshop on Termination, Leipzig, 2009]
* [http://www.lsv.ens-cachan.fr/rdp07/wst.html 9th International Workshop on Termination, Paris, 2007]
* [http://www.easychair.org/FLoC-06/WST.html 8th International Workshop on Terminaton, Seattle, 2006]
* [http://www-i2.informatik.rwth-aachen.de/WST04/ 7th International Workshop on Terminaton, Aachen, 2004]
* [http://www.dsic.upv.es/~rdp03/wst/ 6th International Workshop on Terminaton, Valencia, 2003]
* [http://www.cs.tau.ac.il/~nachumd/wst/index.html 5th International Workshop on Terminaton, Utrecht, 2001]
* [http://verify.rwth-aachen.de/giesl/WST99.html 4th International Workshop on Terminaton, Dagstuhl, 1999]
* [http://www-i2.informatik.rwth-aachen.de/giesl/WST97/main.html 3rd International Workshop on Termination, Ede, 1997]
* 2nd International Workshop on Termination, La Bresse, 1995
* 1st International Workshop on Termination, St. Andrews, 1993
Independently from WST, there are meetings on Certified Termination : [[WScT]]

Complexity

2010-06-22T14:40:34Z

Georg.moser: /* Important Dates */

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010 (but see email to termtools)
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| ?
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| ?
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| ?
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity

2010-06-22T14:40:14Z

Georg.moser: /* Important Dates */

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| July 14, 2010
|-
! style="text-align:left"|Problem Submission
| July 2, 2010
|-
! style="text-align:left"|Competition
| July 16, 2010
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| ?
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| ?
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| ?
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity:Old

2010-06-22T14:35:16Z

Georg.moser:

<pre>
This page is no longer maintained, but kept for the time beeing.
</pre>

The entry point to the complexity category is here: [[Complexity]]

== 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:
# Derivational Complexity (DC),
# innermost Derivational Complexity (iDC),
# Runtime Complexity (RC), and
# innermost Runtime Complexity (iRC)

== Syntax/Semantics for Input/Output ==

As competition semantics, we propose to focus on polynomial
bounds.

=== Input Format ===
Problems will be given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based
respectively.
In particluar, this allows the upload of one single tool for all categories the authors want to participate in.

=== Output Format ===
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 to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

=== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

== Participation ==

=== Requirements ===
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.

=== Participants ===

Insert your name here if you intend to participate:

==== Competition 2009 ====
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)

==== Competition 2008 ====
* M. Avanzini, G. Moser, A. Schnabl (TCT)
* M. Korp, C. Sternagel, H. Zankl (CaT)

== Complexity proof techniques ==

A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]

== Discussion ==

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

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

Scoring (proposals):

* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===

* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

[[Category:Categories]]

Complexity:Old

2010-06-22T14:33:41Z

Georg.moser:

<pre>
This page is no longer maintained
</pre>

The entry point to the complexity category is here: [[Complexity]]

== 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:
# Derivational Complexity (DC),
# innermost Derivational Complexity (iDC),
# Runtime Complexity (RC), and
# innermost Runtime Complexity (iRC)

== Syntax/Semantics for Input/Output ==

As competition semantics, we propose to focus on polynomial
bounds.

=== Input Format ===
Problems will be given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based
respectively.
In particluar, this allows the upload of one single tool for all categories the authors want to participate in.

=== Output Format ===
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 to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

=== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

== Participation ==

=== Requirements ===
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.

=== Participants ===

Insert your name here if you intend to participate:

==== Competition 2009 ====
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)

==== Competition 2008 ====
* M. Avanzini, G. Moser, A. Schnabl (TCT)
* M. Korp, C. Sternagel, H. Zankl (CaT)

== Complexity proof techniques ==

A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]

== Discussion ==

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

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

Scoring (proposals):

* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===

* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

[[Category:Categories]]

Complexity:Old

2010-06-22T14:32:56Z

Georg.moser:

<pre>
This page is no longer maintained, see the new entry point to the complexity
category: [[Complexity]]
</pre>

This page is to record the current status of discussion
on the proposed Complexity Category of the Termination 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:
# Derivational Complexity (DC),
# innermost Derivational Complexity (iDC),
# Runtime Complexity (RC), and
# innermost Runtime Complexity (iRC)

== Syntax/Semantics for Input/Output ==

As competition semantics, we propose to focus on polynomial
bounds.

=== Input Format ===
Problems will be given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based
respectively.
In particluar, this allows the upload of one single tool for all categories the authors want to participate in.

=== Output Format ===
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 to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

=== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

== Participation ==

=== Requirements ===
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.

=== Participants ===

Insert your name here if you intend to participate:

==== Competition 2009 ====
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)

==== Competition 2008 ====
* M. Avanzini, G. Moser, A. Schnabl (TCT)
* M. Korp, C. Sternagel, H. Zankl (CaT)

== Complexity proof techniques ==

A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]

== Discussion ==

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

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

Scoring (proposals):

* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===

* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

[[Category:Categories]]

News:Complexity Wiki Updated

2010-06-22T14:31:23Z

Georg.moser:

{{News
|text=The wiki for the complexity category has been thoroughly re-designed, see [[Complexity]]
|date=June 22, 2010
}}

News:Complexity Wiki Updated

2010-06-22T14:30:36Z

Georg.moser: Created page with '<!-- Please insert the corresponding information below so that the news page can be generated automatically. Line breaks are allowed! You may use MediaWiki syntax here …'

{{News
|text=The wiki for the complexity category has been thoroughly re-designed, see [[Complexity]]
|date=Jun 22
}}

Complexity:Rules

2010-06-22T14:25:13Z

Georg.moser: /* Problem Sets and Problem Selection */

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
* We propose to run subcategories DC and iDC on the following families from TPDB, after
the selection function defined below has been applied. (Note that this is essentially the
current TPDB minus the families with "innermost" annotations.)
These families were already successfully applied for the 2009 competition.

<pre>
AG01; AotoYamada_05; Applicative_05; Applicative_first_order_05; AProVE_04; AProVE_06; AProVE_07; AProVE_08; Beerendonk_07; Bouchare_06; CiME_04; Der95; Endrullis_06; Gebhardt_06; GTSSK07;
HirokawaMiddeldorp_04; Mixed_SRS; Mixed_TRS; Rubio_04; Secret_05_SRS; Secret_05_TRS; Secret_06_SRS; Secret_06_TRS; Secret_07_SRS; Secret_07_TRS; SK90; Strategy_removed_AG01; Strategy_removed_CSR_05;
Strategy_removed_mixed_05; TCT_09; Trafo_06; Transformed_CSR_04; Various_04; Waldmann_06; Waldmann_06_SRS; Waldmann_07_size11; Waldmann_07_size12; Zantema_04; Zantema_05; Zantema_06;AProVE_09_Inductive
</pre>

* For categories RC and iRC, we propose to run the competition on the above families
minus the SRS related families. These families were already successfully applied for the
2009 competition.

* Family "TCT_09" should be replaced by two (much larger) families DC and RC, collected problems for derivational and runtime complexity
analyis, respectively.

* GM: Please indicate wishes for additional families till 27. 6. 2010

==== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity:Rules

2010-06-22T14:21:38Z

Georg.moser: /* Problem Sets and Problem Selection */

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
We propose to run subcategories DC and iDC on the following families from TPDB, after
the selection function defined below has been applied. (Note that this is essentially the
current TPDB minus the families with "innermost" annotations.)
These families were already successfully applied for the 2009 competition.

<pre>
AG01; AotoYamada_05; Applicative_05; Applicative_first_order_05; AProVE_04; AProVE_06; AProVE_07; AProVE_08; Beerendonk_07; Bouchare_06; CiME_04; Der95; Endrullis_06; Gebhardt_06; GTSSK07;
HirokawaMiddeldorp_04; Mixed_SRS; Mixed_TRS; Rubio_04; Secret_05_SRS; Secret_05_TRS; Secret_06_SRS; Secret_06_TRS; Secret_07_SRS; Secret_07_TRS; SK90; Strategy_removed_AG01; Strategy_removed_CSR_05;
Strategy_removed_mixed_05; Trafo_06; Transformed_CSR_04; Various_04; Waldmann_06; Waldmann_06_SRS; Waldmann_07_size11; Waldmann_07_size12; Zantema_04; Zantema_05; Zantema_06;AProVE_09_Inductive
</pre>

For categories RC and iRC, we propose to run the competition on the above families
minus the SRS related families. These families were already successfully applied for the
2009 competition.

==== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity:Rules

2010-06-22T14:19:15Z

Georg.moser: /* Problem Sets and Problem Selection */

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
We propose to run subcategories DC and iDC on the following families from TPDB, after
the selection function defined below has been applied. (Note that this is essentially the
current TPDB minus the families with "innermost" annotations.)
These families were already successfully applied for the 2009 competition.

<pre>
AG01; AotoYamada_05; Applicative_05; Applicative_first_order_05; AProVE_04; AProVE_06; AProVE_07;
AProVE_08; Beerendonk_07; Bouchare_06; CiME_04; Der95; Endrullis_06; Gebhardt_06; GTSSK07;
HirokawaMiddeldorp_04; Mixed_SRS; Mixed_TRS; Rubio_04; Secret_05_SRS; Secret_05_TRS; Secret_06_SRS;
Secret_06_TRS; Secret_07_SRS; Secret_07_TRS; SK90; Strategy_removed_AG01; Strategy_removed_CSR_05;
Strategy_removed_mixed_05; Trafo_06; Transformed_CSR_04; Various_04; Waldmann_06; Waldmann_06_SRS;
Waldmann_07_size11; Waldmann_07_size12; Zantema_04; Zantema_05; Zantema_06;AProVE_09_Inductive
</pre>

For categories RC and iRC, we propose to run the competition on the above families
minus the SRS related families. These families were already successfully applied for the
2009 competition.

==== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity:Rules

2010-06-22T14:09:53Z

Georg.moser: /* Concrete syntax */

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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. 

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

* GM: I don't like the format "POLY(k)" mainly due to presentation reasons: Our first format used exactly this and in presentations I immediately got the question
what "POLY(k)" should mean. Since "O(k)" is used I don't get this question. With respect to the lower-bound: I agree that "O(k)" should be replaced by
"Omega(k)". So let's do that. But I don't see a chance to change this for the upcoming competition ...

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
We propose to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

==== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity:Rules

2010-06-22T14:05:10Z

Georg.moser: /* Scoring (proposals) */

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

* GM: For clarification: I suppose you want to use the following order: POLY >= O(n^7) >= O(n^6) etc. to name an example. And I would insist
on the use of a virtual prover: getting 0 points although an answer has been given I don't like

=== Concrete syntax ===
* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
We propose to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

==== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity:Rules

2010-06-22T14:01:52Z

Georg.moser: /* Lower Bounds */

The purpose of this page is to provide a place for ongoing discussions
on the rules, and to describe the current rules itself.

== Discussion ==
=== 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.

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

(GM: I don't see a problem with that: "YES" indicates that the prover has found a proof. In the case you mention, a proof for non-termination.)

=== Scoring (proposals) ===
* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===
* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

== Rules of the Competition ==
=== Input Format ===
Problems are given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification]. where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based respectively.

=== Output Format ===
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.

=== 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 Sets and Problem Selection ===
We propose to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

==== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

Complexity

2010-05-25T08:36:38Z

Georg.moser: new structure

This page provides general information on the complexity category;
(potential) tool authors or others that may want to join the discussion
on various aspects of the category can also go directly to the
[[Complexity:Rules|discussion and rules page]]; aficionados
may be interested in the [[Complexity:Techniques|techniques page]].

== Introduction ==

It is a challenging topic to automatically determine upper and lower bounds on
the complexity of term rewrite systems (TRSs for short).
Here complexity of a TRS basically refers to the maximal length of derivations,
measured in the size of the initial terms.
Still, depending on rewrite strategies and restrictions on the
set of allowed starting terms, various notions of complexity exist.
The current focus of the competition is on providing
polynomial upper bounds to the complexity of TRSs.
Presumably the competition will be extended to lower bounds soon.

== Overview of the Complexity Category ==
Currently, depending on considered set of starting terms and strategy,
the competition is divided into four categories:

{| class="wikitable center"
|-
! !! Derivational Complexity !! Runtime Complexity
|-
! style="text-align:left"|Full Rewriting
| DC
| RC
|-
! style="text-align:left"|Innermost Rewriting
| iDC
| iRC
|}

Derivational complexity and runtime complexity differ in the sense that for
derivational complexity, no restrictions on the set of considered starting terms is put.
For runtime complexity however, only basic terms (i.e. terms where arguments
are formed from constructor symbols) are taken into account.
See for example [http://dx.doi.org/10.1007/978-3-540-71070-7_32 (Hirokawa, Moser, 2008)]
[http://arxiv.org/abs/0907.5527 (Moser, 2009)]
for further reading on the notion of runtime
complexity.

Furthermore, we distinguish between complexities
induced by full rewriting as opposed to complexities induced by
innermost rewriting.

== Overview of the Competition ==
The complexity category is part of the termination competition since 2008.
The competition is currently hosted at [http://termcomp.uibk.ac.at/termcomp/home.seam],
where you can find results of the competitions from
[http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 2008]
and [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 2009].

=== Important Dates ===
{| class="wikitable center"
|-
! !! Deadline/Date
|-
! style="text-align:left"|Tool Submission
| TBA
|-
! style="text-align:left"|Problem Submission
| TBA
|-
! style="text-align:left"|Competition
| TBA
|}

=== Participate ===
If you want to participate in the competition,
go to the [http://termcomp.uibk.ac.at/ Termination Competition Portal], create an account and add your tool.
Documentation concerning this process can be found
[http://termcomp.uibk.ac.at/termcomp/help/register.seam?cid=8144 here].

Kindly note that in order to participate, your tool needs to be
[http://www.opensource.org/ open source].

==== Participating Teams of Past and Upcoming Competitions ====
Here you can find a list (sorted by tool name) of participants of past competitions
and supposed participants of the upcoming competition.

{| class="wikitable center" border="0" style="text-align:center"
|-
! Tool !! Internal Page !! text-align="left"|Authors !! 2008 !! 2009 !! 2010
|-
! [http://www.imn.htwk-leipzig.de/~waldmann/ Matchbox]
| [[Tools:Matchbox]]
| J. Waldmann
| ---
| x
| ?
|-
! [http://cl-informatik.uibk.ac.at/software/tct TCT]
| [[Tools:TCT]]
| M. Avanzini, G. Moser, A. Schnabl
| x
| x
| ?
|-
! [http://cl-informatik.uibk.ac.at/software/ttt2 CaT]
| [[Tools:CaT]]
| M. Korp, C. Sternagel, H. Zankl
| x
| x
| ?
|-
|}

An overview of the proof techniques applied by the participants in past competitions can be found [[Complexity_Techniques|here]].

== Past Winners ==
In 2008, [[Tools:CaT|CaT]] was the winner of both derivational complexity categories, whereas
for runtime complexity only [[Tools:TCT|TCT]] participated.
In 2009, all categories where ruled by [[Tools:CaT|CaT]]. Congratulations!

For detailed information on the testsuites employed and the actual results of the
tools see the [http://termcomp.uibk.ac.at termcomp] pages.

== Overview of the Competition Rules ==
Problems are given in the new TPDB-format, see
[http://www.termination-portal.org/wiki/XTC_Format_Specification] and
are selected randomly from the newest version of the Termination Problem Database.

In the selection process, emphasis is put onto selecting problems that
could not be automatically verified in past competitions, c.f. page [[Complexity:Rules#Problem Sets and Problem Selection|problem selection]]
for details.
Tools are ranked not only by number of succeeded runs, but in the scoring
also the preciseness of the bounds is taken into account. See page [[Complexity:Rules#scoring|scoring]] for further details.

Unfortunately the database is currently somehow biased towards termination problems.
We encourage everybody to submit new problems to the TPDB that are interesting from a complexity
related perspective. (In submission please indicate that these examples should go into the complexity benchmark.)

Complexity:Old

2010-05-25T08:34:24Z

Georg.moser: moved Complexity to Complexity:Old

This page is to record the current status of discussion
on the proposed Complexity Category of the Termination 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:
# Derivational Complexity (DC),
# innermost Derivational Complexity (iDC),
# Runtime Complexity (RC), and
# innermost Runtime Complexity (iRC)

== Syntax/Semantics for Input/Output ==

As competition semantics, we propose to focus on polynomial
bounds.

=== Input Format ===
Problems will be given in the newly TPDB-format, cf.
[http://www.termination-portal.org/wiki/XTC_Format_Specification], where
the XML-element ''problem'' will have the type ''complexity'' given.
Further, depending on the category DC, iDC, RC and iRC, the attributes
''strategy'' and ''startterm'' will be set to FULL/INNERMOST and full/constructor-based
respectively.
In particluar, this allows the upload of one single tool for all categories the authors want to participate in.

=== Output Format ===
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 to run subcategories DC and iDC
on all TRS and SRS families from the newly organised TPDB, after
the selection function defined below has been applied.
For categories RC and iRC, we propose to run the competition on all TRS families
after application of the selection function stated below:

=== 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 RC, iRC and 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 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''). That is, we want to consider 40% examples that could be solved automatically in last years competition, and 60% of examples that could not be solved automatically. Additionally for DC we want to exclude duplicating TRS as those admit exponential derivational complexity. Based on the probability distribution ''p'' we define the extended selection function ''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.

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>

== Participation ==

=== Requirements ===
In order to participate in the competition, the '''sources''' of your tool have to be '''publicly available'''.

=== Participants ===

Insert your name here if you intend to participate:

==== Competition 2009 ====
* M. Avanzini, G. Moser, A. Schnabl ([http://cl-informatik.uibk.ac.at/software/tct TCT])
* J. Waldmann ([[Tools:Matchbox]]) (derivational complexity for full rewriting)

==== Competition 2008 ====
* M. Avanzini, G. Moser, A. Schnabl (TCT)
* M. Korp, C. Sternagel, H. Zankl (CaT)

== Complexity proof techniques ==

A list of the complexity proof techniques applied by the participants of the competition can be found at [[Complexity_Techniques]]

== Discussion ==

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

(JW: I don't like the looks of an answer starting "YES" and indicating non-termination. See "BOUNDS" proposal below.)

Scoring (proposals):

* as for the upper bound the lower bound certificate should be ranked and both ranks could be compared lexicographically (with the upper bound as the primary criterion)

* JW prefers: don't define some artificial total order on the bounds. The natural partial ordering is given by the inclusion relation on the sets of functions that are described by the bounds. This inclusion can be computed from
<PRE>
(low1, up1) "is better than" (low2, up2) iff low1 >= low2 and up1 <= up2
</PRE>Then for each problem, answer A gets awarded k points if A is strictly better than k of the answers, where "no answer" counts as BOUNDS(LIN,INF), and "strictly better = better and not equal".
This would imply that if all answers are identical, then no-one gets a point.
Perhaps we want to add one virtual prover that always says"BOUNDS(LIN,INF)" -
so anyone who gives a better answer, gets at least one point.

=== Concrete syntax ===

* 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

* JW: I'm not giving up ... one more reason against the O(n^k) syntax: 3. it cannot be used for lower bounds, as we would need Omega instead of Oh. (The other two reasons are: 2. needlessly complicated, and 1. n is an undefined variable)

* proposal to replace YES/NO/MAYBE by BOUNDS: http://dev.aspsimon.org/bugzilla/show_bug.cgi?id=85#c4

LN: I'd like to support this notation. But I think "?" for an unknown bound is unnecessary. It can always be replaced by POLY(0) for the lower
bound and INF for the upper bound. [[User:Noschinski|Noschinski]] 13:26, 13 February 2010 (UTC)

[[Category:Categories]]

Complexity

2010-05-25T08:34:24Z

Georg.moser: moved Complexity to Complexity:Old

#REDIRECT [[Complexity:Old]]

News:XTC Format Specification

2009-02-24T14:31:15Z

Georg.moser: New page: <!-- Please insert the corresponding information below so that the news page can be generated automatically. Line breaks are allowed! You may use MediaWiki syntax here to link to...

{{News
|text=XTC Format Specification: [[XTC_Format_Specification]]
|date=February 24, 2009
}}

Complexity:Old

2008-10-30T09:41:09Z

Georg.moser: /* Problem selection */

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^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-28T19:48:12Z

Georg.moser: /* Syntax/Semantics for Input/Output */

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

Complexity:Old

2008-10-28T19:00:55Z

Georg.moser: /* Syntax/Semantics for Input/Output */

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 earlier proposal on 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

Complexity:Old

2008-10-28T18:46:05Z

Georg.moser: /* Syntax/Semantics for Input/Output */

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, we propose to use an XML input format in the future,
that extends the earlier proposal on an XML 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

Complexity:Old

2008-10-28T15:37:28Z

Georg.moser: /* Syntax/Semantics for Input/Output */

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, we propose to use an XML input format in the future,
that extends the earlier proposal on an XML 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>
<status>POLYNOMIAL|EXPONENTIAL</status>
</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