Termination-Portal.org - User contributions [en]

Tools:Oops

2011-02-22T15:27:33Z

Fab:

{{Tool
|shortname=Oops
|longname=Oops
|homepage=http://verify.rwth-aachen.de/emmes/Oops/Oops-0.0.1.tar.gz
|country=Germany
|university=RWTH Aachen
|developers=[[People:Fabian Emmes|Fabian Emmes]], [[People:Lars Noschinski|Lars Noschinski]]
|publication=
}}



= Oops =

Oops is no real complexity analyzer. Its main purpose was to mark unsuitable examples in the runtime [[complexity]] categories during the [[Termination Competition 2010]]. Many thanks to Georg Moser for the fitting name.

For runtime complexity, one does not analyze the derivation length of arbitrary terms (as one does in derivational complexity), but only of terms with exactly one defined symbol. For some systems this leads to much better intuition about the complexity of the described functions, but for others this definition yields strange results. For example applicative systems only have one defined symbol (the apply symbol), whereas the rest are just constants. Starting only with one apply symbol (as runtime complexity requires), one is most likely not able to build the derivation sequences the author of the example intended.

Furthermore, for such examples where all constructor symbols are constants, there are only finitely many basic terms. This makes asymptotic complexity analysis pointless, as one cannot build arbitrary large start terms.

We identified the following situations, in which we can conclude constant complexity. The strategy of oops is just to identify these situations and return an upper bound of O(1) if successful.

* All constructor symbols of the system are constants. This implies that there are only finitely many basic terms. If all of those terms are terminating, we can conclude constant runtime complexity. The termination of the terms proved by testing doing all possible evaluations of those terms.
* A similar situation occurs if all defined symbols are constants. Again we have only finitely many basic terms which can be tested.
* A third case is if the left-hand sides of all rules contain at least two defined symbols. Since every basic term has exactly one defined symbol, no rule can be applied to any basic term. This way, we can directly conclude O(1), without testing any terms for termination.

Complexity

2010-07-22T09:56:36Z

Fab: Updated Participating Teams of Past and Upcoming Competitions

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

Tools:Oops

2010-07-21T10:22:52Z

Fab: initial homepage

{{Tool
|shortname=Oops
|longname=Oops
|homepage=http://verify.rwth-aachen.de/emmes/oops.tar.gz
|country=Germany
|university=RWTH Aachen
|developers=[[People:Fabian Emmes|Fabian Emmes]], [[People:Lars Noschinski|Lars Noschinski]]
|publication=
}}



= Oops =

Oops is no real complexity analyzer. Its main purpose was to mark unsuitable examples in the runtime [[complexity]] categories during the [[Termination Competition 2010]]. Many thanks to Georg Moser for the fitting name.

For runtime complexity, one does not analyze the derivation length of arbitrary terms (as one does in derivational complexity), but only of terms with exactly one defined symbol. For some systems this leads to much better intuition about the complexity of the described functions, but for others this definition yields strange results. For example applicative systems only have one defined symbol (the apply symbol), whereas the rest are just constants. Starting only with one apply symbol (as runtime complexity requires), one is most likely not able to build the derivation sequences the author of the example intended.

Furthermore, for such examples where all constructor symbols are constants, there are only finitely many basic terms. This makes asymptotic complexity analysis pointless, as one cannot build arbitrary large start terms.

We identified the following situations, in which we can conclude constant complexity. The strategy of oops is just to identify these situations and return an upper bound of O(1) if successful.

* All constructor symbols of the system are constants. This implies that there are only finitely many basic terms. If all of those terms are terminating, we can conclude constant runtime complexity. The termination of the terms proved by testing doing all possible evaluations of those terms.
* A similar situation occurs if all defined symbols are constants. Again we have only finitely many basic terms which can be tested.
* A third case is if the left-hand sides of all rules contain at least two defined symbols. Since every basic term has exactly one defined symbol, no rule can be applied to any basic term. This way, we can directly conclude O(1), without testing any terms for termination.

People:Fabian Emmes

2009-07-15T15:54:52Z

Fab:

{{Person
|firstname=Fabian
|middlenames=
|lastname=Emmes
|titles=
|email=emmes@informatik.rwth-aachen.de
|homepage=http://verify.rwth-aachen.de/emmes/
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Research and Teaching Assistant
}}

People:Fabian Emmes

2009-07-15T15:54:11Z

Fab:

{{Person
|firstname=Fabian
|middlenames=
|lastname=Emmes
|titles=
|email=emmes@informatik.rwth-aachen.de
|homepage=http://verify.rwth-aachen.de/emmes/
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Research and Teaching Assistant in the Department of Research Group Computer Science 2 (RWTH Aachen, Germany)
}}

Functional Programming

2009-07-15T15:52:06Z

Fab: Added some information about haskell termination and the competition format

Within the Termination Competition, there is a category on Functional Programming
where the object is to prove termination of Haskell functions automatically.

Currently, the Termination Problems Data Base contains 1676 functions from the Haskell Prelude,
and AProVE shows termination of 1294 of them.

== Termination of Haskell Functions ==

This category compares tools that automatically analyze termination of Haskell programs. If one considers a whole Haskell program, termination corresponds to finishing the computation in finite time on every possible input.
Since Haskell uses lazy/on-demand evaluation, this notion is not directly useful for analysis of single functions. Consider for example a program containing:

<pre>map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = (f x):(map f xs)

bot :: a -> b
bot = bot

zeros :: [Integer]
zeros = 0:zeros

strange :: (Integer -> Integer) -> Integer
strange f
| f 23 == 42 = strange f
| otherwise = 5</pre>

Intuitively a specific function evaluation (where the value of every argument is supplied) is terminating if the Haskell evaluation strategy needs finitely many steps to compute the result completely. This means, that evaluation does not stop when reaching a term headed by a constructor: it will continue evaluating the arguments of this constructor. Hence, the function zeros is considered non-terminating.

When analyzing the termination behavior of a function itself (without specific arguments), the picture gets slightly more complicated. If one allows arbitrary arguments, then nearly every Haskell function will not finish in finitely many steps. Even a function as head would need to be considered non-terminating if one would allow non-terminating arguments: head bot will obviously not terminate. Hence, this idea is not useful. Instead one regards a function as terminating, if it finishes in a finite number of steps whenever it is called with terminating arguments. This can be written formally as follows:

'''Definition: (Termination of Haskell Expressions)''' The set of terminating Haskell expressions is defined as the smallest set, such that t is in this set iff:
* t does not start an infinite evaluation sequence, and
* if t evaluates to an expression c t1 ... tn where c is a constructor then t1 ... tn must also be terminating expressions, and
* if t evaluates to an expression f t1 ... tn where f is a function symbol and the type of t is α -> β, then f t1 ... tn t' must be terminating for every terminating expression t'.

This means that in the above program the expression <tt>map</tt> would be considered terminating, while the expression <tt>\f -> map f zeros</tt> would be non-terminating. On the other hand head <tt>zeros</tt> is obviously nonterminating. The expression <tt>\x -> if x == 23 then 42 else 5</tt> is terminating, while the function <tt>strange</tt> is not. This is because by the third point in the definition one needs to analyze strange called with any terminating argument (like our lambda expression) which would result in a non-terminating behavior.

The semantics of "termination" (in the context of the competition)
is discussed e.g. in http://lists.lri.fr/pipermail/termtools/2006-March/000179.html

== The Problem Format ==

Every input for the FP category is a file containing a Haskell module with exactly the compiler pragma <tt>htermination</tt>, that specifies the start term. The start term is any Haskell expression containing no free variables. Function names, constructors etc. bound in the module itself can be used.
<pre>{-# htermination (foldr1 :: (a -> a -> a) -> (List a) -> a) #-}

import qualified Prelude

data MyBool = MyTrue | MyFalse
data List a = Cons a (List a) | Nil

foldr1 :: (a -> a -> a) -> (List a) -> a
foldr1 f (Cons x Nil) = x
foldr1 f (Cons x xs) = f x (foldr1 f xs)</pre>

== Implementations ==

The termination analyzer AProVE has a web front end http://aprove.informatik.rwth-aachen.de/eval/Haskell/

People:Fabian Emmes

2008-04-02T14:24:26Z

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

{{Person
|firstname=Fabian
|middlenames=
|lastname=Emmes
|titles=
|email=fabian.emmes@rwth-aachen.de
|homepage=
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Student 
}}