Termination-Portal.org - User contributions [en]

PTRS Innermost

2026-06-09T12:27:14Z

JCKassing: Small fixes

The PTRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t have a finite upper bound on the expected runtime of all innermost rewrite sequences starting with t (strong almost-sure termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.
It restricts the analysis of probabilistic algorithms to a call-by-value evaluation strategy, which is one of the most used evaluation strategies in probabilistic programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has at least 2 arguments).

Formally, a probabilistic term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of probabilistic rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R innermost AST or innermost SAST?

Possible Outputs:
* "AST" followed by a termination proof, e.g., a ranking function proving innermost almost-sure termination (iAST) of R.
* "SAST" followed by a termination proof, e.g., a ranking function proving innermost strong almost-sure termination (iSAST) of R.
* "MAYBE" (indicating that the solver can neither prove iAST nor iSAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

PTRS Standard

2026-06-09T12:25:39Z

JCKassing: Small fixes

The PTRS Standard category is concerned with the question "Will every rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t have a finite upper bound on the expected runtime of all rewrite sequences starting with t (strong almost-sure termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.

Many algorithms can be made more robust by introducing probabilistic choices.
For example, in probabilistic quicksort the pivot element is chosen uniformly at random.
This variant is more robust than the standard quicksort algorithm because it achieves an expected runtime of O(n * log(⁡n))
for every input and avoids the deterministic worst-case runtime of O(n2).
However, when probabilities are introduced, programmers often quickly lose intuition about expected runtime and termination.
Therefore, automatic techniques for proving termination and establishing upper bounds on the expected runtime are needed.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has at least 2 arguments).

Formally, a probabilistic term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of probabilistic rewrite rules, see [1].

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R AST or SAST?

Possible Outputs:
* "AST" followed by a termination proof, e.g., a ranking function proving almost-sure termination (AST) of R.
* "SAST" followed by a termination proof, e.g., a ranking function proving strong almost-sure termination (SAST) of R.
* "MAYBE" (indicating that the solver can neither prove AST nor SAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

SRS Relative

2026-06-09T12:24:08Z

JCKassing: Use the transitive-reflexive closure!

The SRS Relative category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop using a certain subset of the given rewrite rules?".
In other words, if every rule has a cost which is either 0 or 1, then does every possible reduction have a finite total cost?

== Syntax & Semantic ==

Strings are terms where every function symbol has arity 1, i.e., exactly one argument.
Additionally, the same variable appears on both the left and right sides of each rule.
Formally, a relative string rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,am → bm} of finitely many rewrite rules denoted by R/S where all the occurring terms are strings.

A relative string rewrite system R/S is terminating if there exists no infinite rewrite sequence s0 →R s'0 →*S s1 →R s'1 →*S s2 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two separate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of string rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative string rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

[[Category:Categories]]

SRS Relative

2026-06-09T12:23:17Z

JCKassing: Small fixes

The SRS Relative category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop using a certain subset of the given rewrite rules?".
In other words, if every rule has a cost which is either 0 or 1, then does every possible reduction have a finite total cost?

== Syntax & Semantic ==

Strings are terms where every function symbol has arity 1, i.e., exactly one argument.
Additionally, the same variable appears on both the left and right sides of each rule.
Formally, a relative string rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,am → bm} of finitely many rewrite rules denoted by R/S where all the occurring terms are strings.

A relative string rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two separate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of string rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative string rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

[[Category:Categories]]

SRS Standard

2026-06-09T12:21:27Z

JCKassing: Small fixes

The SRS Standard category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop?".
In other words, does every computation defined by the string rewrite rules eventually reach a normal form (a string where no rule applies)?

== Syntax & Semantic ==

The syntax and the semantics of string rewrite systems are described [[Term Rewriting | here]].
Strings are terms where every function symbol has arity 1, i.e., exactly one argument.
Additionally, the same variable appears on both the left and right sides of each rule.

Formally, a string rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules where all occurring terms are strings.

A string rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s2 →R ... of strings.

== Problem ==

Input: A string rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove termination).

[[Category:Categories]]

TRS Conditional

2026-06-09T12:18:56Z

JCKassing: Small fixes

The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrite steps terminate?"
where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(t,s)' be evaluated to 'true'?

== Syntax & Semantic ==

Formally, a conditional term rewrite system is a set R = {l1 → r1 | c1,...,ln → rn | cn} of finitely many conditional rewrite rules.
A conditional rewrite rule is a rewrite rule l → r with an additional condition, a reachability constraint, that has to be satisfied to use the rewrite rule.
There are multiple different ways one can interpret these conditions, e.g., oriented, joined, and convertible.

== Problem ==

Input: A conditional term rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence of R.
* "MAYBE" (indicating that the solver cannot prove termination of R).

[[Category:Categories]]

TRS Contextsensitive

2026-06-09T12:17:24Z

JCKassing: Small fixes

The TRS Contextsensitive category is concerned with the question "Will every possible sequence of rewrites eventually stop if we prohibit to rewrite within certain arguments of function symbols".

== Category Motivation ==

Context-sensitive rewriting is a restriction of first-order term rewriting which is used, e.g., to model different evaluation strategies for the analysis of functional programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and specifically for context-sensitive rewriting [https://project-coco.uibk.ac.at/ARI/cstrs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].
Additionally, every n-ary function symbol f has a corresponding replacement map μ(f) which indicates which arguments of f may be evaluated.

A term rewrite system R is terminating w.r.t. μ if there exists no infinite rewrite sequence s0 →R s1 →R s2 →R ... that respects the replacement map μ.

== Problem ==

Input: A term rewrite system R and a replacement map μ.

Question: Does R terminate w.r.t. μ?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R w.r.t. μ.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence w.r.t. μ.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Derivational Complexity

2026-06-09T12:16:25Z

JCKassing: Small fixes

The TRS Derivational Complexity category is concerned with the question "What is the time complexity of a given TRS with relation to the size of the initial term".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
This helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the derivation height dh(t) of a term t is the supremum over all →R-rewrite sequences starting with t.
The derivational complexity of an TRS is a function that maps every natural number n
to the greatest derivation height of all objects of size at most n, i.e., dc→R (n) = sup{m | |t| <= n, dh(t) >= m}.

The goal is to find an asymptotic upper bound and lower bound on the derivational complexity dc→R (n) of a given TRS R.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

[[Category:Categories]]

TRS Equational

2026-06-09T12:15:33Z

JCKassing: Small fixes

The TRS Equational category is concerned with the question "Will every possible sequence of rewrite steps on equivalence classes terminate?".

== Syntax & Semantic ==

Formally, an equational term rewrite system is a set R = {l1 → r1,...,ln → rn} of finitely many rewrite rules together with a set S = {a1 = b1,...,am = bm} of finitely many term equations, called a ''theory''.

An equational term rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 =S ... =S s10 →R s11 =S ... =S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R where we can use the equations from S mid rewriting.

Here, a ''theory'' may be added to declarations of function symbols.

<pre>
fun ::= ( fun identifier number theory? )
theory ::= :theory [A | C | AC]
</pre>

* full rewriting modulo associativity / commutativity / associativity and commutativity

== Problem ==

Input: An equational term rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

[[Category:Categories]]

TRS Innermost

2026-06-09T12:14:02Z

JCKassing: Small fixes

The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)?

== Category Motivation ==

This category investigates termination under the innermost rewriting strategy, roughly corresponding to a call-by-value evaluation strategy in programming languages,
which is one of the most used evaluation strategies.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.
A term rewrite system R is innermost terminating if there exists no infinite rewrite sequence s0 →iR s1 →iR s2 →iR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R innermost terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving innermost termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove innermost termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Innermost Derivational Complexity

2026-06-09T12:13:18Z

JCKassing: Small fixes

The TRS Innermost Derivational Complexity category is concerned with the question "What is the time complexity of a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
This helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height idh(t) of a term t is the supremum over all innermost →iR-rewrite sequences starting with t.
The innermost derivational complexity of an TRS is a function that maps every natural number n
to the greatest derivation height of all objects of size at most n, i.e., idc→R (n) = sup{m | |t| <= n, idh(t) >= m}.

The goal is to find an asymptotic upper bound and lower bound on the innermost derivational complexity idc→R (n) of a given TRS R.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

[[Category:Categories]]

TRS Innermost Runtime Complexity

2026-06-09T12:11:18Z

JCKassing: Small fixes

The TRS Innermost Runtime Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

While derivational complexity considers arbitrary initial terms, runtime complexity restricts the initial terms to model an algorithm that is given fixed data as arguments,
which relates to the intuitive definition of time complexity.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height idh(t) of a term t is the supremum over all →iR-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The innermost runtime complexity of an TRS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., irc→R (n) = sup{m | t ∈ TB, |t| <= n, idh(t) >= m}.

The goal is to find an asymptotic upper bound and lower bound on the innermost runtime complexity irc→R (n) of a given TRS R.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost runtime complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

[[Category:Categories]]

TRS Parallel Innermost Derivational Complexity

2026-06-09T12:08:25Z

JCKassing: Small fixes

The TRS Innermost Derivational Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

TODO: clarify the difference to [[TRS Innermost Derivational Complexity | TRS Innermost Derivational Complexity]]!

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all →iR-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The innermost derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., dc→R (n) = sup{m | t ∈ TB, |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the innermost derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Relative

2026-06-09T12:06:00Z

JCKassing: Small fixes

The TRS Relative category is concerned with the question "Will every possible sequence of rewrites eventually stop using a certain subset of the given rewrite rules?".
In other words, if every rule has a cost which is either 0 or 1, then does every possible reduction have a finite total cost?

== Category Motivation ==

Relative termination isolates the rules whose usage should be finite while allowing auxiliary rules to be used freely in between and is used in different termination and complexity analysis techniques.

== Syntax & Semantic ==

Formally, a relative term rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,am → bm} of finitely many rewrite rules denoted by R/S, see [1].

A relative term rewrite system R/S is terminating if there exists no infinite rewrite sequence s0 →R s'0 →*S s1 →R s'1 →*S s2 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two separate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of term rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative term rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Runtime Complexity

2026-06-09T11:59:30Z

JCKassing: Small fixes

The TRS Runtime Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

While derivational complexity considers arbitrary initial terms, runtime complexity restricts the initial terms to model an algorithm that is given fixed data as arguments,
which relates to the intuitive definition of time complexity.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the derivation height dh(t) of a term t is the supremum over all →R-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The runtime complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., rc→R (n) = sup{m | t ∈ TB, |t| <= n, dh(t) >= m}.

The goal is to find an asymptotic upper bound and lower bound on the runtime complexity rc→R (n) of a given TRS R.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic runtime complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

[[Category:Categories]]

TRS Standard

2026-06-09T11:54:35Z

JCKassing: Fixed wrong indice

The TRS Standard category is concerned with the question "Will every possible sequence of rewrites eventually stop?".
In other words, does every computation defined by the rewrite rules eventually reach a normal form (a term where no rule applies)?

== Category Motivation ==

This category evaluates tools on termination of standard first-order term rewrite systems with unrestricted rewriting which is one of the basic problems in the competition. Many of the other termination problems are either special forms of this problem, or can be reduced to this problem.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

A term rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s2 →R ...

== Problem ==

Input: A term rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

Termination Competition 2026

2026-06-08T11:13:39Z

JCKassing: Update on the rules for the 2026 TermComp

The Termination and Complexity Competition (TermComp) 2026 will be affiliated with [https://termination-portal.org/wiki/21st_International_Workshop_on_Termination WST 2026], which takes place at [https://www.floc26.org/ FLoC 2026].

The competition will be run on the RWTH Aachen High Performance Computing Cluster.
Test runs will take place right after the submission deadline, followed by a bug/conflict reporting phase.
Bug fixes will be possible until shortly before the full run.
A live run on a subset of the benchmark collection, and a presentation of the final results will take place at WST.
Presumably, there will also be a presentation at IJCAR.



== Dates ==

* Contributions to the [https://github.com/TermCOMP/termcomp-reference Competition Rules]: June 26
* Tool and Benchmark Submission: June 26
* Full Run: July 13-17
* Live Run: July 24/25
* Presentation of the results at WST: July 25

== Competition Categories ==

The competition contains several categories for termination and complexity from the areas of term rewriting (all categories with HO/FO-TRSs, with- or without strategies) and programming languages (Logic Programming, Haskell, Java, C, integer transition systems, ...), see [[Termination Competition]] for more details on all the categories.

Proposals for new categories are welcome!

A category is only run at the competition if there are at least 2 participants, at least 40 examples
for this category in the underlying termination problem data base, and clearly defined rules in the [https://github.com/TermCOMP/termcomp-reference termination competition reference].

== Competition Procedure ==

All participants in the same category will be run on the existing problems of this category.
There might be modifications of the rules suggested by the organizer and decided by the SC.

There will be a full run on the entire benchmark collection '''before''' WST, and a live run on a subset of the benchmark collection at WST.
The timeout for the full run will be 300 seconds.
The timeout for the live run will be significantly smaller (presumably 30 seconds).
The results of the full run will be announced at WST.

Further technical information is available [[Termination Competition 2026 technical details|here]].

The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML, or CPF format. Exceptions to these rules are the [http://www.termination-portal.org/wiki/Termination_Competition_Certified_Categories_Competition certified] (see also the [http://cl-informatik.uibk.ac.at/software/cpf/ CPF-website]) and [http://cl-informatik.uibk.ac.at/users/georg/cbr/competition/ complexity] categories. See all existing [http://www.termination-portal.org/wiki/Category:Categories categories] for more details.

For those categories devoted to prove only termination or non-termination, the score of a tool is the number of non-contradictory answers minus the given penalization (if any).

A proof or answer that is known to be wrong will be penalized by -10 points, if it remains after the bugfix deadline.
The SC will decide what should be penalized, depending on the discussion among the participants.

== Registration ==

To submit a tool, please follow the instruction at [https://github.com/TermCOMP/registration this repository].
Every participant must submit at least five new '''secret''' benchmarks via email to florian.frohn@cs.rwth-aachen.de (unless the size of the benchmarks exceeds 5MB -- in that case, please get in touch to figure out another way).
Please also include a README with a (short) description of the origin of the benchmarks.
After the competition, these benchmarks will become part of TPDB.

To submit a benchmark, please follow the instruction at the [https://github.com/TermCOMP/TPDB-ARI TPDB ARI repository]

We recommend to register early, and update information as needed.

It is highly recommended that participants also subscribe to the [https://lists.rwth-aachen.de/postorius/lists/termtools.lists.rwth-aachen.de/ termtools] mailing list, because that is where announcements will be made, and where discussion takes place.

== Technical Details ==

Competition data will be presented via [https://github.com/TermCOMP/starexec-master starexec-master]
(a successor of [https://github.com/stefanvonderkrone/star-exec-presenter star-exec-presenter] developed at HTWK Leipzig).

Technical details about the execution platform are available [[Termination Competition 2026 technical details|here]].

== Contact ==

Any questions or suggestions regarding the termination competition should go to, and discussed at termtools<at>lists.rwth-aachen.de

To contact the steering committee, send an email to terminationcompetitionsc<at>lists.rwth-aachen.de.

== Steering Committee ==

* Florian Frohn (Chair and Organizer), RWTH Aachen
* Jürgen Giesl, RWTH Aachen
* Georg Moser, University of Innsbruck
* Étienne Payet, Université de La Réunion
* Akihisa Yamada
* Dieter Hofbauer, ASW Saarland

== Changes with respect to 2025 ==

These lists reflect the discussion in the community, and in the steering committee. Items are preliminary, and not officially binding.
Please do not edit this list (unless you're in the SC). Instead, send proposals to termtools or terminationcompetitionsc mailing list,
or create a new wiki page and put a link here.

Proposed changes:

* In addition to the usual tracks, we will try to organize a '''knockout tournament'''.

Adopted changes:

* We will only run categories with clearly defined rules in the [https://github.com/TermCOMP/termcomp-reference termination competition reference].
* Every participant has to submit at least five new '''secret''' benchmarks
* Demo categories will only be run on request to the steering committee, and this request has to be justified somehow (e.g., by a paper, significant tool improvements, ...). The final decision is up to the SC.
* Submissions to TPDB must have a README with a (short) description of the origin of the benchmarks.
* We will do a full run and a live run, as described above.

Termination Competition

2026-05-20T18:17:27Z

JCKassing: Update Upcoming Competition

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at 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 Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2026]] will be held during [[21st International Workshop on Termination]] at [https://www.floc26.org/ FLoC 2026], Lisbon, Portugal, July 25, 2026

== Competition Categories ==

Currently, the competition features the following categories. Since 2007 some of the categories also have [[Certified_Termination|certified categories]], where an additional certifier checks the output of the tools. Categories that were used in the past but not included in the three most recent competitions are marked with an ✖.

=== Termination of Rewriting ===

These categories consider the termination of rewrite systems, a foundational computational model used to represent symbolic computation and program transformations.
The goal is to automatically prove that no infinite rewrite sequences are possible for the given system.
Different categories capture variations of rewriting such as relative rewriting, context-sensitive rewriting, conditional rules, or restrictions on the rewriting strategy (e.g., innermost or outermost rewriting).

<div style="column-count:3; column-gap:2em;">
* [[TRS Standard|TRS Standard]]
* [[TRS Relative|TRS Relative]]
* [[TRS Contextsensitive|TRS Contextsensitive]]
* [[TRS Equational|TRS Equational]]
* [[TRS Innermost|TRS Innermost]]
* [[TRS Outermost|TRS Outermost]]
* [[TRS Conditional|TRS Conditional]]
* [[TRS Conditional - Operational Termination|TRS Conditional - Operational Termination]]
* [[SRS Standard|SRS Standard]]
* [[SRS Relative|SRS Relative]]
* [[Cycle_Rewriting|Cycle Rewriting]] ✖
* [[Higher_Order|Higher Order Rewriting]] (since 2010)
* [[ITRS|ITRS Innermost]] (since 2014)
* [[Integer Transition Systems|ITS]] (since 2014)
</div>

=== Termination of Probabilistic Rewriting ===

These categories address probabilistic rewrite systems , where rewrite rules are applied according to probability distributions.
Instead of classical termination, the goal is to prove almost-sure termination, i.e., that infinite executions occur with probability zero,
or strong almost-sure termination, i.e., that the expected runtime is finite.
This lifts termination analysis to models that capture randomized algorithms or stochastic behavior.

<div style="column-count:3; column-gap:2em;">
* [[PTRS Standard|PTRS Standard]]
* [[PTRS Innermost|PTRS Innermost]]
</div>

Currently, there are only categories regarding probabilistic rewrite systems,
but an extension to probabilistic imperative programs may be possible in future competitions.

=== Termination of Programs ===

These categories focus on proving termination of user-friendly programming languages used in industry.
The categories differ by the source programming language or program model.

<div style="column-count:3; column-gap:2em;">
* [[Logic_Programming|Termination of logic programs]]
* [[Functional_Programming|Termination of functional programs]] (since 2007)
* [[Java_Bytecode|Termination of Java Bytecode programs]] (since 2009)
* [[C_Programs|Termination of C programs]] (since 2014)
</div>

=== Complexity of Rewriting ===

These categories evaluate tools that automatically analyze the asymptotic complexity of rewrite systems .
Instead of only proving termination, the goal is to derive upper bounds on the length of rewrite sequences,
typically expressed as functions of the input size.
Different categories measure difference runtime complexities under various rewriting strategies and different restrictions on the initial start term.

<div style="column-count:3; column-gap:2em;">
* [[TRS Derivational Complexity|TRS Derivational Complexity]]
* [[TRS Innermost Derivational Complexity|TRS Innermost Derivational Complexity]]
* [[TRS Runtime Complexity|TRS Runtime Complexity]]
* [[TRS Innermost Runtime Complexity|TRS Innermost Runtime Complexity]]
* [[TRS Parallel Innermost Derivational Complexity|TRS Parallel Innermost Derivational Complexity]]
* [[Term Rewriting#Integer Transition Systems|ITS Complexity]]
</div>

=== Complexity Analysis ===

These categories focus on automatically determining time complexity bounds for programs written in user-friendly programming languages .
Tools analyze the program’s control flow, data dependencies, and loops to derive asymptotic upper bounds on runtime with respect to the input size.

<div style="column-count:3; column-gap:2em;">
* [[C_Complexity|Complexity of C programs]]
</div>

== Competition Benchmarks ==

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

We welcome problem submissions from non-participants.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== History of Termination Competitions ==

A list of all competitions that have been taken place can be found [[Termination Competition History|here]].

==== Results ====

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

Suggestions

2026-03-19T10:44:34Z

JCKassing: Updated suggestions

Suggestions to improve this web site 

TODO:

* create/fill the pages on the different categories used in the termination competition (listed here: http://www.termination-portal.org/wiki/Termination_Competition).

Termination Competition

2026-03-19T10:38:03Z

JCKassing: Added TRS Complexity pages

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at 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 Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Competition Categories ==

Currently, the competition features the following categories. Since 2007 some of the categories also have [[Certified_Termination|certified categories]], where an additional certifier checks the output of the tools. Categories that were used in the past but not included in the three most recent competitions are marked with an ✖.

=== Termination of Rewriting ===

These categories consider the termination of rewrite systems, a foundational computational model used to represent symbolic computation and program transformations.
The goal is to automatically prove that no infinite rewrite sequences are possible for the given system.
Different categories capture variations of rewriting such as relative rewriting, context-sensitive rewriting, conditional rules, or restrictions on the rewriting strategy (e.g., innermost or outermost rewriting).

<div style="column-count:3; column-gap:2em;">
* [[TRS Standard|TRS Standard]]
* [[TRS Relative|TRS Relative]]
* [[TRS Contextsensitive|TRS Contextsensitive]]
* [[TRS Equational|TRS Equational]]
* [[TRS Innermost|TRS Innermost]]
* [[TRS Outermost|TRS Outermost]]
* [[TRS Conditional|TRS Conditional]]
* [[TRS Conditional - Operational Termination|TRS Conditional - Operational Termination]]
* [[SRS Standard|SRS Standard]]
* [[SRS Relative|SRS Relative]]
* [[Cycle_Rewriting|Cycle Rewriting]] ✖
* [[Higher_Order|Higher Order Rewriting]] (since 2010)
* [[ITRS|ITRS Innermost]] (since 2014)
* [[Integer Transition Systems|ITS]] (since 2014)
</div>

=== Termination of Probabilistic Rewriting ===

These categories address probabilistic rewrite systems , where rewrite rules are applied according to probability distributions.
Instead of classical termination, the goal is to prove almost-sure termination, i.e., that infinite executions occur with probability zero,
or strong almost-sure termination, i.e., that the expected runtime is finite.
This lifts termination analysis to models that capture randomized algorithms or stochastic behavior.

<div style="column-count:3; column-gap:2em;">
* [[PTRS Standard|PTRS Standard]]
* [[PTRS Innermost|PTRS Innermost]]
</div>

Currently, there are only categories regarding probabilistic rewrite systems,
but an extension to probabilistic imperative programs may be possible in future competitions.

=== Termination of Programs ===

These categories focus on proving termination of user-friendly programming languages used in industry.
The categories differ by the source programming language or program model.

<div style="column-count:3; column-gap:2em;">
* [[Logic_Programming|Termination of logic programs]]
* [[Functional_Programming|Termination of functional programs]] (since 2007)
* [[Java_Bytecode|Termination of Java Bytecode programs]] (since 2009)
* [[C_Programs|Termination of C programs]] (since 2014)
</div>

=== Complexity of Rewriting ===

These categories evaluate tools that automatically analyze the asymptotic complexity of rewrite systems .
Instead of only proving termination, the goal is to derive upper bounds on the length of rewrite sequences,
typically expressed as functions of the input size.
Different categories measure difference runtime complexities under various rewriting strategies and different restrictions on the initial start term.

<div style="column-count:3; column-gap:2em;">
* [[TRS Derivational Complexity|TRS Derivational Complexity]]
* [[TRS Innermost Derivational Complexity|TRS Innermost Derivational Complexity]]
* [[TRS Runtime Complexity|TRS Runtime Complexity]]
* [[TRS Innermost Runtime Complexity|TRS Innermost Runtime Complexity]]
* [[TRS Parallel Innermost Derivational Complexity|TRS Parallel Innermost Derivational Complexity]]
* [[Term Rewriting#Integer Transition Systems|ITS Complexity]]
</div>

=== Complexity Analysis ===

These categories focus on automatically determining time complexity bounds for programs written in user-friendly programming languages .
Tools analyze the program’s control flow, data dependencies, and loops to derive asymptotic upper bounds on runtime with respect to the input size.

<div style="column-count:3; column-gap:2em;">
* [[C_Complexity|Complexity of C programs]]
</div>

== Competition Benchmarks ==

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

We welcome problem submissions from non-participants.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== History of Termination Competitions ==

A list of all competitions that have been taken place can be found [[Termination Competition History|here]].

==== Results ====

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

TRS Parallel Innermost Derivational Complexity

2026-03-19T10:36:30Z

JCKassing: Added TRS Parallel Innermost Derivational Complexity

The TRS Innermost Derivational Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

TODO: clarify the difference to [TRS Innermost Derivational Complexity | TRS Innermost Derivational Complexity]!

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all →iR-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The innermost derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., dc→R (n) = sup{m | t ∈ TB, |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the innermost derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Innermost Runtime Complexity

2026-03-19T10:34:45Z

JCKassing: Added TRS Innermost Runtime Complexity

The TRS Innermost Runtime Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

While derivational complexity considers arbitrary initial terms, runtime complexity restricts the initial terms to model an algorithm that is given fixed data as arguments,
which relates to the intuitive definition of time complexity.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all →iR-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The innermost runtime complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., dc→R (n) = sup{m | t ∈ TB, |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the innermost runtime complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost runtime complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Runtime Complexity

2026-03-19T10:33:01Z

JCKassing: Added TRS Runtime Complexity

The TRS Runtime Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

While derivational complexity considers arbitrary initial terms, runtime complexity restricts the initial terms to model an algorithm that is given fixed data as arguments,
which relates to the intuitive definition of time complexity.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the derivation height dh(t) of a term t is the supremum over all →R-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The runtime complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., dc→R (n) = sup{m | t ∈ TB, |t| <= n, t →Rn s}.

The goal is to find an asymptotic upper bound and lower bound on the runtime complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic runtime complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Innermost Derivational Complexity

2026-03-19T10:26:59Z

JCKassing: Added TRS Innermost Derivational Complexity

The TRS Innermost Derivational Complexity category is concerned with the question "What is the time complexity of a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
his helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all innermost →iR-rewrite sequences starting with t.
The innermost derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all objects of size at most n, i.e., dc→R (n) = sup{m | |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n^2), O(n^3), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Derivational Complexity

2026-03-19T10:23:56Z

JCKassing: Added TRS Derivational Complexity

The TRS Derivational Complexity category is concerned with the question "What is the time complexity of a given TRS with relation to the size of the initial term".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
his helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the derivation height dh(t) of a term t is the supremum over all →R-rewrite sequences starting with t.
The derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all objects of size at most n, i.e., dc→R (n) = sup{m | |t| <= n, t →Rn s}.

The goal is to find an asymptotic upper bound and lower bound on the derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

String Rewriting

2026-03-18T11:46:09Z

JCKassing: Blanked the page

Transition Systems

2026-03-18T11:43:18Z

JCKassing: No Category anymore

Syntax and semantics of the format are presented in [https://www.microsoft.com/en-us/research/publication/termcomp-proposal-pushdown-systems-as-a-model-for-programs-with-procedures/].

Termination Competition

2026-03-18T11:41:02Z

JCKassing: Added all termination category subpages

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at 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 Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Competition Categories ==

Currently, the competition features the following categories. Since 2007 some of the categories also have [[Certified_Termination|certified categories]], where an additional certifier checks the output of the tools. Categories that were used in the past but not included in the three most recent competitions are marked with an ✖.

=== Termination of Rewriting ===

These categories consider the termination of rewrite systems, a foundational computational model used to represent symbolic computation and program transformations.
The goal is to automatically prove that no infinite rewrite sequences are possible for the given system.
Different categories capture variations of rewriting such as relative rewriting, context-sensitive rewriting, conditional rules, or restrictions on the rewriting strategy (e.g., innermost or outermost rewriting).

<div style="column-count:3; column-gap:2em;">
* [[TRS Standard|TRS Standard]]
* [[TRS Relative|TRS Relative]]
* [[TRS Contextsensitive|TRS Contextsensitive]]
* [[TRS Equational|TRS Equational]]
* [[TRS Innermost|TRS Innermost]]
* [[TRS Outermost|TRS Outermost]]
* [[TRS Conditional|TRS Conditional]]
* [[TRS Conditional - Operational Termination|TRS Conditional - Operational Termination]]
* [[SRS Standard|SRS Standard]]
* [[SRS Relative|SRS Relative]]
* [[Cycle_Rewriting|Cycle Rewriting]] ✖
* [[Higher_Order|Higher Order Rewriting]] (since 2010)
* [[ITRS|ITRS Innermost]] (since 2014)
* [[Integer Transition Systems|ITS]] (since 2014)
</div>

=== Termination of Probabilistic Rewriting ===

These categories address probabilistic rewrite systems , where rewrite rules are applied according to probability distributions.
Instead of classical termination, the goal is to prove almost-sure termination, i.e., that infinite executions occur with probability zero,
or strong almost-sure termination, i.e., that the expected runtime is finite.
This lifts termination analysis to models that capture randomized algorithms or stochastic behavior.

<div style="column-count:3; column-gap:2em;">
* [[PTRS Standard|PTRS Standard]]
* [[PTRS Innermost|PTRS Innermost]]
</div>

Currently, there are only categories regarding probabilistic rewrite systems,
but an extension to probabilistic imperative programs may be possible in future competitions.

=== Termination of Programs ===

These categories focus on proving termination of actual programming languages used in industry.
The categories differ by the source programming language or program model.

<div style="column-count:3; column-gap:2em;">
* [[Logic_Programming|Termination of logic programs]]
* [[Functional_Programming|Termination of functional programs]] (since 2007)
* [[Java_Bytecode|Termination of Java Bytecode programs]] (since 2009)
* [[C_Programs|Termination of C programs]] (since 2014)
</div>

=== Complexity of Rewriting ===

These categories evaluate tools that automatically analyze the asymptotic complexity of rewrite systems .
Instead of only proving termination, the goal is to derive upper bounds on the length of rewrite sequences,
typically expressed as functions of the input size.
Different categories measure difference runtime complexities under various rewriting strategies and different restrictions on the initial start term.

<div style="column-count:3; column-gap:2em;">
* [[Term Rewriting#Runtime Complexity|TRS Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Derivational Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Derivational Complexity]]
* TRS Parallel Innermost Derivational Complexity
* [[Term Rewriting#Integer Transition Systems|ITS Complexity]]
</div>

=== Complexity Analysis ===

These categories focus on automatically determining time complexity bounds for programs written in concrete programming languages .
Tools analyze the program’s control flow, data dependencies, and loops to derive asymptotic upper bounds on runtime with respect to the input size.

<div style="column-count:3; column-gap:2em;">
* [[C_Complexity|Complexity of C programs]]
</div>

== Competition Benchmarks ==

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

We welcome problem submissions from non-participants.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== History of Termination Competitions ==

A list of all competitions that have been taken place can be found [[Termination Competition History|here]].

==== Results ====

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

Integer Transition Systems

2026-03-18T11:40:28Z

JCKassing: Added ITS Page

The Integer Transition Systems category is concerned with the question "Will every possible sequence of rewrite steps on an integer program terminate?".

== Syntax & Semantic ==

Integer Transition Systems (ITSs) are [https://project-coco.uibk.ac.at/ARI/lctrs.php LCTRSs] with the following restrictions:
* The theory is always Ints.
* Rules must comply with the following grammar:
<pre>
rule ::= (rule lhs rhs (:guard term)? (:var (vars))?)
lhs ::= (identifier identifier+)
rhs ::= (identifier term+)
</pre>
Moreover, ITSs must declare one and only one entrypoint
<pre>
entrypoint ::= (entrypoint identifier)
</pre>
where the given identifier refers to a previously declared function symbol.

The goal is to prove termination w.r.t. all well-sorted startterms of the form
<pre>
(f c_1 ... c_k)
</pre>
where f is the entrypoint and c_1,...,c_k are constants from the theory Ints (i.e., integers or Booleans).

== Problem ==

Input: An ITS R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence of R.
* "MAYBE" (indicating that the solver cannot prove termination of R).

== References ==

[[Category:Categories]]

TRS Conditional

2026-03-18T11:37:59Z

JCKassing: Added TRS Conditional Page

The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrites steps terminate?"
where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(t,s)' be evaluated to 'true'?

== Syntax & Semantic ==

Formally, a conditional term rewrite system is a set R = {l1 → r1 | c1,...,ln → rn | cn} of finitely many conditional rewrite rules.
A conditional rewrite rule is a rewrite rule l → r with an additional condition, a reachability constraint, that has to be satisfied to use the rewrite rule.
There are multiple different ways one can interpret these conditions, e.g., oriented, joined, and convertible.

== Problem ==

Input: A conditional term rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite of R.
* "MAYBE" (indicating that the solver cannot prove termination of R).

== References ==

[[Category:Categories]]

TRS Conditional - Operational Termination

2026-03-18T11:37:52Z

JCKassing: Added TRS Conditional - Operation Page

The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrites steps terminate?"
where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(t,s)' be evaluated to 'true'?

== Syntax & Semantic ==

Formally, a conditional term rewrite system is a set R = {l1 → r1 | c1,...,ln → rn | cn} of finitely many conditional rewrite rules.
A conditional rewrite rule is a rewrite rule l → r with an additional condition, a reachability constraint, that has to be satisfied to use the rewrite rule.
There are multiple different ways one can interpret these conditions, e.g., oriented, joined, and convertible.

TODO: clarify the difference to [[TRS Conditional|TRS Conditional]]!

== Problem ==

Input: A conditional term rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite of R.
* "MAYBE" (indicating that the solver cannot prove termination of R).

== References ==

[[Category:Categories]]

TRS Equational

2026-03-18T11:29:46Z

JCKassing: Added TRS Equational Page

The TRS Equational category is concerned with the question "Will every possible sequence of rewrites steps on equivalence classes terminate?".

== Syntax & Semantic ==

Formally, an equational term rewrite system is a set R = {l1 → r1,...,ln → rn} of finitely rewrite rules together a set S = {a1 = b1,...,an = bn} of finitely many term equations, called a ''theory''.

An equational term rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 =S ... =S s10 →R s11 =S ... =S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R where we can use the equations from S mid rewriting.

Here, a ''theory'' may be added to declarations of function symbols.

<pre>
fun ::= ( fun identifier number theory? )
theory ::= :theory [A | C | AC]
</pre>

* full rewriting modulo associativity / commutativity / associativity and commutativity

== Problem ==

Input: n equational term rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

== References ==

[[Category:Categories]]

TRS Contextsensitive

2026-03-18T11:25:18Z

JCKassing: Added TRS Contextsensitive Page

The TRS Contextsensitive category is concerned with the question "Will every possible sequence of rewrites eventually stop if we prohibit to rewrite within certain arguments of function symbols".

== Category Motivation ==

Context-sensitive rewriting is a restriction of first-order term rewriting which is used, e.g., to model different evaluation strategies for the analysis of functional programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and specifically for context-sensitive rewriting [https://project-coco.uibk.ac.at/ARI/cstrs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].
Additionally, every n-ary function symbbol f has a corresponding replacement map μ(f) which indicates which arguments of f may be evaluated.

A term rewrite system R is terminating w.r.t. μ if there exists no infinite rewrite sequence s0 →R s1 →R s1 →R ... that respects the replacement map μ.

== Problem ==

Input: A term rewrite system R and a replacement map μ

Question: Does R terminate w.r.t. μ?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R w.r.t. μ.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence w.r.t. μ.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

PTRS Standard

2026-03-11T10:08:02Z

JCKassing: Added missing reference

The PTRS Standard category is concerned with the question "Will every rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.

Many algorithms can be made more robust by introducing probabilistic choices.
For example, in probabilistic quicksort the pivot element is chosen uniformly at random.
This variant is more robust than the standard quicksort algorithm because it achieves an expected runtime of O(n * log(⁡n))
for every input and avoids the deterministic worst-case runtime of O(n2).
However, when probabilities are introduced, programmers often quickly lose intuition about expected runtime and termination.
Therefore, automatic techniques for proving termination and establishing upper bounds on the expected runtime are needed.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

Formally, a probabilistic term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of probabilistic rewrite rules, see [1].

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R AST or SAST?

Possible Outputs:
* "AST" followed by a termination proof, e.g., a ranking function proving almost-sure termination (AST) of R.
* "SAST" followed by a termination proof, e.g., a ranking function proving strong almost-sure termination (SAST) of R.
* "MAYBE" (indicating that the solver can neither prove AST nor SAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

PTRS Innermost

2026-03-11T10:07:37Z

JCKassing: Fixed small typo in reference

The PTRS Standard category is concerned with the question "Will every innermost rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all innermost rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.
It restricts the analysis of probabilistic algorithms to a call-by-value evaluation strategy, which is one of the most used evaluation strategies in probabilistic programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

Formally, a probabilistic term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of probabilistic rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R innermost AST or innermost SAST?

Possible Outputs:
* "iAST" followed by a termination proof, e.g., a ranking function proving innermost almost-sure termination (iAST) of R.
* "iSAST" followed by a termination proof, e.g., a ranking function proving innermost strong almost-sure termination (iSAST) of R.
* "MAYBE" (indicating that the solver can neither prove iAST nor iSAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

Probabilistic Rewriting

2026-03-11T10:05:58Z

JCKassing: Removed Categories from this page

== General ==

As in the non-probabilistic setting, we use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so probabilistic TRSs (PTRSs) are represented as S-Expressions (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.1]). The format of TRSs is explained [[Term Rewriting|here]]. To extend this format for PTRSs, rules are replaced by probabilistic rules that are defined as follows:
<pre>
prule ::= ( prule term dist cost? )
cost ::= :cost number
dist ::= ( ( term prob? )* )
prob ::= :prob number
</pre>

Some examples of valid PTRSs are shown below.

<pre>
===== P1 =====
(format PTRS)
(fun f 0)
(fun stop 0)
(prule f (( f :prob 1 ) (stop :prob 1 )))
</pre>
* P1 models a coin flip that stops once it flips heads and keeps on going if it flips tails.
<pre>
===== P2 =====
(format PTRS)
(fun g 1)
(prule (g x) (( (g (g x)) :prob 1 ) (x :prob 1 )))
</pre>
* P2 models a symmetric random walk on the numbers of f symbols in a term.
<pre>
===== P3 =====
(format PTRS)
(fun h 1)
(prule (h x) (( (h (h x)) :prob 2 ) (x :prob 1 )))
</pre>
* P3 models a biased random walk on the numbers of h symbols in a term which is biased towards nontermination.

== Probabilistic Termination ==

There are several notions of ``termination'' in the probabilistic setting.
As in ordinary term rewriting, we consider universal termination, i.e., we have no fixed start term, but consider every possible reduction.
For the formal definitions of all notions of termination, see [https://www.sciencedirect.com/science/article/pii/S0167642319301339 here].

===== Certain Termination =====

A PTRS is certainly terminating if every possible reduction eventuelly terminates.
As this boils down to termination of TRSs, we usually try to omit certainly terminating examples in the following category,
and hence, have no allowed answer for a certainly terminating PTRS.

Example: None of the PTRSs P1, P2, or P3 are certainly terminating.

===== Almost-Sure Termination (AST) =====

A PTRS is almost-surely terminating if every non-terminating reduction occurs with probability 0.

Example: While P1 and P2 are AST, P3 is not AST.

===== Positive Almost-Sure Termination (PAST) =====

A PTRS is positive almost-surely terminating if the expected derivation length of every possible reduction is finite.

Example: Only P1 is PAST, but P2 and P3 are not PAST.

===== Strong Almost-Sure Termination (SAST) =====

A PTRS is strong almost-surely terminating if for every start term t there exists a bound C_t such that
the expected derivation length of every possible reduction starting in t is at most C_t.

Example: Again only P1 is PAST, but P2 and P3 are not PAST.

Termination Competition

2026-03-11T10:03:58Z

JCKassing: Added links to some defined categories

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at 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 Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Competition Categories ==

Currently, the competition features the following categories. Since 2007 some of the categories also have [[Certified_Termination|certified categories]], where an additional certifier checks the output of the tools. Categories that were used in the past but not included in the three most recent competitions are marked with an ✖.

=== Termination of Rewriting ===

These categories consider the termination of rewrite systems, a foundational computational model used to represent symbolic computation and program transformations.
The goal is to automatically prove that no infinite rewrite sequences are possible for the given system.
Different categories capture variations of rewriting such as relative rewriting, context-sensitive rewriting, conditional rules, or restrictions on the rewriting strategy (e.g., innermost or outermost rewriting).

<div style="column-count:3; column-gap:2em;">
* [[TRS Standard|TRS Standard]]
* [[TRS Relative|TRS Relative]]
* [[Term Rewriting#TRS Contextsensitive|TRS Contextsensitive]]
* [[Term Rewriting#TRS Equational|TRS Equational]]
* [[TRS Innermost|TRS Innermost]]
* [[TRS Outermost|TRS Outermost]]
* [[Term Rewriting#TRS Conditional|TRS Conditional]]
* [[Term Rewriting#TRS Conditional - Operational Termination|TRS Conditional - Operational Termination]]
* [[SRS Standard|SRS Standard]]
* [[SRS Relative|SRS Relative]]
* [[Cycle_Rewriting|Cycle Rewriting]] ✖
* [[Higher_Order|Higher Order Rewriting]] (since 2010)
* [[ITRS|ITRS Innermost]] (since 2014)
* [[Term Rewriting#Integer Transition Systems|ITS]] (since 2014)
</div>

=== Termination of Probabilistic Rewriting ===

These categories address probabilistic rewrite systems , where rewrite rules are applied according to probability distributions.
Instead of classical termination, the goal is to prove almost-sure termination, i.e., that infinite executions occur with probability zero,
or strong almost-sure termination, i.e., that the expected runtime is finite.
This lifts termination analysis to models that capture randomized algorithms or stochastic behavior.

<div style="column-count:3; column-gap:2em;">
* [[PTRS Standard|PTRS Standard]]
* [[PTRS Innermost|PTRS Innermost]]
</div>

Currently, there are only categories regarding probabilistic rewrite systems,
but an extension to probabilistic imperative programs may be possible in future competitions.

=== Termination of Programs ===

These categories focus on proving termination of actual programming languages used in industry.
The categories differ by the source programming language or program model.

<div style="column-count:3; column-gap:2em;">
* [[Logic_Programming|Termination of logic programs]]
* [[Functional_Programming|Termination of functional programs]] (since 2007)
* [[Java_Bytecode|Termination of Java Bytecode programs]] (since 2009)
* [[C_Programs|Termination of C programs]] (since 2014)
</div>

=== Complexity of Rewriting ===

These categories evaluate tools that automatically analyze the asymptotic complexity of rewrite systems .
Instead of only proving termination, the goal is to derive upper bounds on the length of rewrite sequences,
typically expressed as functions of the input size.
Different categories measure difference runtime complexities under various rewriting strategies and different restrictions on the initial start term.

<div style="column-count:3; column-gap:2em;">
* [[Term Rewriting#Runtime Complexity|TRS Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Derivational Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Derivational Complexity]]
* TRS Parallel Innermost Derivational Complexity
* [[Term Rewriting#Integer Transition Systems|ITS Complexity]]
</div>

=== Complexity Analysis ===

These categories focus on automatically determining time complexity bounds for programs written in concrete programming languages .
Tools analyze the program’s control flow, data dependencies, and loops to derive asymptotic upper bounds on runtime with respect to the input size.

<div style="column-count:3; column-gap:2em;">
* [[C_Complexity|Complexity of C programs]]
</div>

== Competition Benchmarks ==

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

We welcome problem submissions from non-participants.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== History of Termination Competitions ==

A list of all competitions that have been taken place can be found [[Termination Competition History|here]].

==== Results ====

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

PTRS Innermost

2026-03-11T10:03:05Z

JCKassing: Added PTRS Innermost category

The PTRS Standard category is concerned with the question "Will every innermost rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all innermost rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.
It restricts the analysis of probabilistic algorithms to a call-by-value evaluation strategy, which is one of the most used evaluation strategies in probabilistic programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

Formally, a probabilistic term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of probabilistic rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R innermost AST or innermost SAST?

Possible Outputs:
* "iAST" followed by a termination proof, e.g., a ranking function proving innermost almost-sure termination (iAST) of R.
* "iSAST" followed by a termination proof, e.g., a ranking function proving innermost strong almost-sure termination (iSAST) of R.
* "MAYBE" (indicating that the solver can neither prove iAST nor iSAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [1] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

PTRS Standard

2026-03-11T09:57:07Z

JCKassing: Added PTRS Standard category

The PTRS Standard category is concerned with the question "Will every rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.

Many algorithms can be made more robust by introducing probabilistic choices.
For example, in probabilistic quicksort the pivot element is chosen uniformly at random.
This variant is more robust than the standard quicksort algorithm because it achieves an expected runtime of O(n * log(⁡n))
for every input and avoids the deterministic worst-case runtime of O(n2).
However, when probabilities are introduced, programmers often quickly lose intuition about expected runtime and termination.
Therefore, automatic techniques for proving termination and establishing upper bounds on the expected runtime are needed.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

Formally, a probabilistic term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of probabilistic rewrite rules, see [1].

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R AST or SAST?

Possible Outputs:
* "AST" followed by a termination proof, e.g., a ranking function proving outermost termination of R.
* "SAST" followed by a termination proof, e.g., a ranking function proving outermost termination of R.
* "MAYBE" (indicating that the solver cannot prove outermost termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.

[[Category:Categories]]

TRS Outermost

2026-03-11T09:11:45Z

JCKassing: Added a motivation and link to the ari format (TRS Outermost)

The TRS Outermost category is concerned with the question "Will every outermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates outermost reducible expressions eventually reach a normal form (a term where no rule applies)?

== Category Motivation ==

This category investigates termination under the outermost rewriting strategy, roughly corresponding to a call-by-name or lazy evaluation strategy.
Although it is not the most common evaluation strategy in programming languages, it is still used by some widely used languages, such as Haskell.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

An outermost rewrite step is a rewrite step that rewrites an outermost reducible expression, i.e., there is no other redex at a position above the redex we want to rewrite.
A term rewrite system R is outermost terminating if there exists no infinite rewrite sequence s0 →oR s1 →oR s2 →oR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R outermost terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving outermost termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite outermost rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove outermost termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Innermost

2026-03-11T09:08:30Z

JCKassing: Added a motivation and link to the ari format (TRS Innermost)

The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)?

== Category Motivation ==

This category investigates termination under the innermost rewriting strategy, roughly corresponding to a call-by-value evaluation strategy in programming languages,
which is one of the most used evaluation strategies.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.
A term rewrite system R is innermost terminating if there exists no infinite rewrite sequence s0 →iR s1 →iR s2 →iR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R innermost terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving innermost termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Standard

2026-03-11T09:04:19Z

JCKassing: Added a motivation and link to the ari format

The TRS Standard category is concerned with the question "Will every possible sequence of rewrites eventually stop?".
In other words, does every computation defined by the rewrite rules eventually reach a normal form (a term where no rule applies)?

== Category Motivation ==

This category evaluates tools on termination of standard first-order term rewrite systems with unrestricted rewriting which is one of the basic problems in the competition. Many of the other termination problems are either special forms of this problem, or can be reduced to this problem.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

A term rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s1 →R ...

== Problem ==

Input: A term rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

SRS Standard

2026-03-10T16:27:46Z

JCKassing: Mentioned strings in the def of SRSs

The SRS Standard category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop?".
In other words, does every computation defined by the string rewrite rules eventually reach a normal form (a string where no rule applies)?

== Syntax & Semantic ==

The syntax and the semantics of string rewrite systems are described [[Term Rewriting | here]].
Strings are terms where every function symbol has arity 1, i.e., exactly one argument.

Formally, a string rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules where all occurring terms are strings.

A string rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s1 →R ... of strings.

== Problem ==

Input: A string rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove termination).

[[Category:Categories]]

SRS Relative

2026-03-10T16:27:05Z

JCKassing: Added SRS Relative Category Page

The SRS Relative category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop using a certain subset of the given rewrite rules?".
In other words, if every rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?

== Syntax & Semantic ==

Strings are terms where every function symbol has arity 1, i.e., exactly one argument.
Formally, a relative string rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} of finitely many rewrite rules denoted by R/S where all the occuring terms are strings.

A relative string rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of string rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative string rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

[[Category:Categories]]

SRS Standard

2026-03-10T16:24:41Z

JCKassing: Added SRS Standard Category Page

The SRS Standard category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop?".
In other words, does every computation defined by the string rewrite rules eventually reach a normal form (a string where no rule applies)?

== Syntax & Semantic ==

The syntax and the semantics of string rewrite systems are described [[Term Rewriting | here]].
Strings are terms where every function symbol has arity 1, i.e., exactly one argument.

Formally, a string rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

A string rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s1 →R ... of strings.

== Problem ==

Input: A string rewrite system R.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove termination).

[[Category:Categories]]

TRS Relative

2026-03-09T17:12:38Z

JCKassing: Fixed some typos

The TRS Relative category is concerned with the question "Will every possible sequence of rewrites eventually stop using a certain subset of the given rewrite rules?".
In other words, ifevery rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?

== Syntax & Semantic ==

Formally, a relative term rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} of finitely many rewrite rules denoted by R/S, see [1].

A relative term rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of term rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative term rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Outermost

2026-03-09T17:11:44Z

JCKassing: Added TRS Outermost Category Page

The TRS Outermost category is concerned with the question "Will every outermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates outermost reducible expressions eventually reach a normal form (a term where no rule applies)?

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

An outermost rewrite step is a rewrite step that rewrites an outermost reducible expression, i.e., there is no other redex at a position above the redex we want to rewrite.
A term rewrite system R is outermost terminating if there exists no infinite rewrite sequence s0 →oR s1 →oR s2 →oR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R outermost terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving outermost termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite outermost rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove outermost termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Innermost

2026-03-09T17:09:10Z

JCKassing: Added TRS Innermost Category Page

The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)?

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.
A term rewrite system R is innermost terminating if there exists no infinite rewrite sequence s0 →iR s1 →iR s2 →iR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R innermost terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving innermost termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost rewrite sequence.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

TRS Relative

2026-03-09T09:48:02Z

JCKassing: Added TRS Relative Category Page

The TRS Relative category is concerned with the question "Will every possible sequence of rewrites eventually stop using a certain subset of the given rewrite rules?".
In other words, ifevery rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?

== Syntax & Semantic ==

Formally, a relative term rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} of finitely many rewrite rules denoted by R/S, see [1].

A relative term rewrite system R is terminating if there exists no infinite rewrite sequence s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of term rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative term rewrite system R/S.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination).

== References ==

* [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[[Category:Categories]]

Termination Competition

2026-03-09T09:31:03Z

JCKassing: Added Link to new TRS Standard category page

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at 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 Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Competition Categories ==

Currently, the competition features the following categories. Since 2007 some of the categories also have [[Certified_Termination|certified categories]], where an additional certifier checks the output of the tools. Categories that were used in the past but not included in the three most recent competitions are marked with an ✖.

=== Termination of Rewriting ===

These categories consider the termination of rewrite systems, a foundational computational model used to represent symbolic computation and program transformations.
The goal is to automatically prove that no infinite rewrite sequences are possible for the given system.
Different categories capture variations of rewriting such as relative rewriting, context-sensitive rewriting, conditional rules, or restrictions on the rewriting strategy (e.g., innermost or outermost rewriting).

<div style="column-count:3; column-gap:2em;">
* [[TRS Standard|TRS Standard]]
* [[Term Rewriting#TRS Relative|TRS Relative]]
* [[Term Rewriting#TRS Contextsensitive|TRS Contextsensitive]]
* [[Term Rewriting#TRS Equational|TRS Equational]]
* [[Term Rewriting#TRS Innermost|TRS Innermost]]
* [[Term Rewriting#TRS Outermost|TRS Outermost]]
* [[Term Rewriting#TRS Conditional|TRS Conditional]]
* [[Term Rewriting#TRS Conditional - Operational Termination|TRS Conditional - Operational Termination]]
* [[Term Rewriting#SRS Standard|SRS Standard]]
* [[Term Rewriting#SRS Relative|SRS Relative]]
* [[Cycle_Rewriting|Cycle Rewriting]] ✖
* [[Higher_Order|Higher Order Rewriting]] (since 2010)
* [[ITRS|ITRS Innermost]] (since 2014)
* [[Term Rewriting#Integer Transition Systems|ITS]] (since 2014)
</div>

=== Termination of Probabilistic Rewriting ===

These categories address probabilistic rewrite systems , where rewrite rules are applied according to probability distributions.
Instead of classical termination, the goal is to prove almost-sure termination, i.e., that infinite executions occur with probability zero,
or strong almost-sure termination, i.e., that the expected runtime is finite.
This lifts termination analysis to models that capture randomized algorithms or stochastic behavior.

<div style="column-count:3; column-gap:2em;">
* [[Probabilistic Rewriting#PTRS Standard|PTRS Standard]] (since 2024)
* [[Probabilistic Rewriting#PTRS Innermost|PTRS Innermost]] (since 2024)
</div>

Currently, there are only categories regarding probabilistic rewrite systems,
but an extension to probabilistic imperative programs may be possible in future competitions.

=== Termination of Programs ===

These categories focus on proving termination of actual programming languages used in industry.
The categories differ by the source programming language or program model.

<div style="column-count:3; column-gap:2em;">
* [[Logic_Programming|Termination of logic programs]]
* [[Functional_Programming|Termination of functional programs]] (since 2007)
* [[Java_Bytecode|Termination of Java Bytecode programs]] (since 2009)
* [[C_Programs|Termination of C programs]] (since 2014)
</div>

=== Complexity of Rewriting ===

These categories evaluate tools that automatically analyze the asymptotic complexity of rewrite systems .
Instead of only proving termination, the goal is to derive upper bounds on the length of rewrite sequences,
typically expressed as functions of the input size.
Different categories measure difference runtime complexities under various rewriting strategies and different restrictions on the initial start term.

<div style="column-count:3; column-gap:2em;">
* [[Term Rewriting#Runtime Complexity|TRS Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Derivational Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Derivational Complexity]]
* TRS Parallel Innermost Derivational Complexity
* [[Term Rewriting#Integer Transition Systems|ITS Complexity]]
</div>

=== Complexity Analysis ===

These categories focus on automatically determining time complexity bounds for programs written in concrete programming languages .
Tools analyze the program’s control flow, data dependencies, and loops to derive asymptotic upper bounds on runtime with respect to the input size.

<div style="column-count:3; column-gap:2em;">
* [[C_Complexity|Complexity of C programs]]
</div>

== Competition Benchmarks ==

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

We welcome problem submissions from non-participants.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== History of Termination Competitions ==

A list of all competitions that have been taken place can be found [[Termination Competition History|here]].

==== Results ====

The results of (almost) all competitions are available [https://termcomp.github.io/ here]