Publications on Termination
2015
- Proving Non-Termination by Finite AutomataJörg Endrullis, and Hans ZantemaIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2015), pp. 160–176, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)paper
Summary
We present a new technique to prove non-termination of term rewriting. The basic idea is tofind a non-empty regular language of terms that is weakly closed under rewriting and does not containnormal forms. It is automated by representing the language by a tree automaton with a fixednumber of states, and expressing the mentioned requirements in a SAT formula. Satisfiabilityof this formula implies non-termination. Our approach succeeds for many examples where allearlier techniques fail, for instance for the S-rule from combinatory logic.
See research for an overview of my research on termination.
Bibtex
@inproceedings{termination:automata:2015, author = {Endrullis, J\"{o}rg and Zantema, Hans}, title = {{Proving Non-termination by Finite Automata}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2015)}, volume = {36}, pages = {160--176}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2015}, doi = {10.4230/LIPIcs.RTA.2015.160}, keywords = {rewriting, termination, automata}, type = {conference} }
Digital Object Identifier
10.4230/LIPIcs.RTA.2015.160
2013
- SAT Compilation for Termination Proofs via Semantic LabellingAlexander Bau, Jörg Endrullis, and Johannes WaldmannIn: Proc. Workshop on Termination (WST 2007) (2013)paper
Bibtex
@inproceedings{termination:sat:compilation:2014, author = {Bau, Alexander and Endrullis, J\"{o}rg and Waldmann, Johannes}, title = {{SAT compilation for Termination Proofs via Semantic Labelling}}, booktitle = {Proc.\ Workshop on Termination (WST~2007)}, year = {2013}, keywords = {rewriting, termination}, type = {workshop} }
2011
- Lazy Productivity via TerminationJörg Endrullis, and Dimitri HendriksTheoretical Computer Science , 412 (28) , pp. 3203–3225 (2011)paper
Bibtex
@article{productivity:termination:2011, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri}, title = {{Lazy Productivity via Termination}}, journal = {Theoretical Computer Science}, volume = {412}, number = {28}, pages = {3203--3225}, year = {2011}, doi = {10.1016/j.tcs.2011.03.024}, keywords = {rewriting, infinitary rewriting, productivity, termination}, type = {journal} }
Digital Object Identifier
10.1016/j.tcs.2011.03.024
- Levels of Undecidability in RewritingJörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, and Hans ZantemaInformation and Computation , 209 (2) , pp. 227–245 (2011)paper
Summary
Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.
In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.
Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.
This paper is an extended version of Degrees of Undecidability in Term Rewriting (CSL 2009).
Bibtex
@article{rewriting:undecidability:levels:2011, author = {Endrullis, J\"{o}rg and Geuvers, Herman and Simonsen, Jakob Grue and Zantema, Hans}, title = {{Levels of Undecidability in Rewriting}}, journal = {Information and Computation}, volume = {209}, number = {2}, pages = {227--245}, year = {2011}, doi = {10.1016/j.ic.2010.09.003}, keywords = {rewriting, undecidability, termination, confluence}, type = {journal} }
Digital Object Identifier
10.1016/j.ic.2010.09.003
2010
- Local Termination: Theory and PracticeJörg Endrullis, Roel C. de Vrijer, and Johannes WaldmannLogical Methods in Computer Science , 6 (3) (2010)paper
Bibtex
@article{termination:local:2010, author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C. and Waldmann, Johannes}, title = {{Local Termination: Theory and Practice}}, journal = {Logical Methods in Computer Science}, volume = {6}, number = {3}, year = {2010}, doi = {10.2168/LMCS-6(3:20)2010}, keywords = {rewriting, termination, automata}, type = {journal} }
Digital Object Identifier
10.2168/LMCS-6(3:20)2010
- Transforming Outermost into Context-Sensitive RewritingJörg Endrullis, and Dimitri HendriksLogical Methods in Computer Science , 6 (2) (2010)paper
Summary
We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on `context extension', each outermost rewrite step is modeled by exactly one step in the transformed system. This transformation turns out to be complete for the class of left-linear TRSs. The second transformation is called `dynamic labeling' and results in smaller sized context-sensitive TRSs. Here each modeled step is adjoined with a small number of auxiliary steps. As a result state-of-the-art termination methods for context-sensitive rewriting become available for proving termination of outermost rewriting. Both transformations have been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the annual termination competition.
This is an extended version of the paper From Outermost to Context-Sensitive Rewriting (RTA 2009).
See research for an overview of my research on termination.
Bibtex
@article{termination:outermost:2010, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri}, title = {{Transforming Outermost into Context-Sensitive Rewriting}}, journal = {Logical Methods in Computer Science}, volume = {6}, number = {2}, year = {2010}, doi = {10.2168/LMCS-6(2:5)2010}, keywords = {rewriting, termination, automata}, type = {journal} }
Digital Object Identifier
10.2168/LMCS-6(2:5)2010
2009
- From Outermost to Context-Sensitive RewritingJörg Endrullis, and Dimitri HendriksIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2009), pp. 305–319, Springer (2009)paper
Summary
We define a transformation from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. For the class of left-linear TRSs the transformation is complete. Thereby state-of-the-art termination methods and automated termination provers for context-sensitive rewriting become available for proving termination of outermost rewriting. The translation has been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the last edition of the annual termination competition.
An extended version of this paper is available from Transforming Outermost into Context-Sensitive Rewriting (Logical Methods in Computer Science 2010).
See research for an overview of my research on termination.
Bibtex
@inproceedings{termination:outermost:2009, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri}, title = {{From Outermost to Context-Sensitive Rewriting}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2009)}, volume = {5595}, pages = {305--319}, publisher = {Springer}, series = {LNCS}, year = {2009}, doi = {10.1007/978-3-642-02348-4\_22}, keywords = {rewriting, termination, automata}, type = {conference} }
Digital Object Identifier
10.1007/978-3-642-02348-4_22
- Local TerminationJörg Endrullis, Roel C. de Vrijer, and Johannes WaldmannIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2009), pp. 270–284, Springer (2009)paper
Bibtex
@inproceedings{termination:local:2009, author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C. and Waldmann, Johannes}, title = {{Local Termination}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2009)}, volume = {5595}, pages = {270--284}, publisher = {Springer}, series = {LNCS}, year = {2009}, doi = {10.1007/978-3-642-02348-4\_19}, keywords = {rewriting, termination, automata}, type = {conference} }
Digital Object Identifier
10.1007/978-3-642-02348-4_19
- Degrees of Undecidability in Term RewritingJörg Endrullis, Herman Geuvers, and Hans ZantemaIn: Proc. Conf. on Computer Science Logic (CSL 2009), pp. 255–270, Springer (2009)paper
Summary
Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed.
In this paper we give an overview of how the main properties of first-order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms.
Most uniform properties are \( \Pi^0_2 \)-complete. The particular problem of local confluence turns out to be \( \Pi^0_2 \)-complete for ground terms, but only \( \Sigma^0_1 \)-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be \( \Pi^1_1 \)-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy.
We refer to Levels of Undecidability in Rewriting (Information and Computation 2011) for an extended journal version of this paper.
Bibtex
@inproceedings{rewriting:undecidability:degrees:2009, author = {Endrullis, J\"{o}rg and Geuvers, Herman and Zantema, Hans}, title = {{Degrees of Undecidability in Term Rewriting}}, booktitle = {Proc.\ Conf.\ on Computer Science Logic (CSL~2009)}, volume = {5771}, pages = {255--270}, publisher = {Springer}, series = {LNCS}, year = {2009}, doi = {10.1007/978-3-642-04027-6\_20}, keywords = {rewriting, undecidability, termination, confluence}, type = {conference} }
Digital Object Identifier
10.1007/978-3-642-04027-6_20
2008
- Matrix Interpretations for Proving Termination of Term RewritingJörg Endrullis, Johannes Waldmann, and Hans ZantemaJournal of Automated Reasoning , 40 (2-3) , pp. 195–220 (2008)paper
Summary
We present a new method for automatically proving termination of term rewriting using matrix interpretation (weighted automata with natural numbers as weights). It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows us to prove termination and relative termination.
A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.
This is an extended version of the paper Matrix Interpretations for Proving Termination of Term Rewriting (IJCAR 2006).
See research for an overview of my research on termination.
Bibtex
@article{termination:matrix:2008, author = {Endrullis, J\"{o}rg and Waldmann, Johannes and Zantema, Hans}, title = {{Matrix Interpretations for Proving Termination of Term Rewriting}}, journal = {Journal of Automated Reasoning}, volume = {40}, number = {2-3}, pages = {195--220}, year = {2008}, doi = {10.1007/s10817-007-9087-9}, keywords = {rewriting, termination}, type = {journal} }
Digital Object Identifier
10.1007/s10817-007-9087-9
2007
- Root Stabilisation Using Dependency PairsJörg Endrullis, and Jeroen KetemaIn: Proc. Workshop on Termination (WST 2007), pp. 17–21 (2007)paper
Bibtex
@inproceedings{termination:root:2007, author = {Endrullis, J\"{o}rg and Ketema, Jeroen}, title = {{Root Stabilisation Using Dependency Pairs}}, booktitle = {Proc.\ Workshop on Termination (WST~2007)}, pages = {17--21}, year = {2007}, keywords = {rewriting, infinitary rewriting, termination}, type = {workshop} }
2006
- Matrix Interpretations for Proving Termination of Term RewritingJörg Endrullis, Johannes Waldmann, and Hans ZantemaIn: Proc. Int. Joint Conf. on Automated Reasoning (IJCAR 2006), pp. 574–588, Springer (2006)paper
Summary
We present a new method for automatically proving termination of term rewriting using matrix interpretation (weighted automata with natural numbers as weights). It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular non-total well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows to prove termination and relative termination. A modification of the latter in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation.
By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver. Our implementation performs well on the Termination Problem Data Base: better than 5 out of 6 tools that participated in the 2005 termination competition in the category of term rewriting.
An extended journal version of this paper is available from Matrix Interpretations for Proving Termination of Term Rewriting (Journal of Automated Reasoning 2008).
See research for an overview of my research on termination.
Bibtex
@inproceedings{termination:matrix:2006, author = {Endrullis, J\"{o}rg and Waldmann, Johannes and Zantema, Hans}, title = {{Matrix Interpretations for Proving Termination of Term Rewriting}}, booktitle = {Proc.\ Int.\ Joint Conf.\ on Automated Reasoning (IJCAR~2006)}, volume = {4130}, pages = {574--588}, publisher = {Springer}, series = {LNCS}, year = {2006}, doi = {10.1007/11814771\_47}, keywords = {rewriting, termination, automata}, type = {conference} }
Digital Object Identifier
10.1007/11814771_47
- Decomposing Terminating Rewrite RelationsJörg Endrullis, Dieter Hofbauer, and Johannes WaldmannIn: Proc. Workshop on Termination (WST 2006), pp. 39–43 (2006)paper
Summary
In this paper we are concerned with automatically proving termination of string rewriting systems (or word rewriting systems). We introduce an efficient technique for constructing automata that serve as certificates of match-boundedness, and thereby termination. Previously constructions have either been inefficient or incomplete:
- Match-Bounded String Rewriting Systems by Alfons Geser, Dieter Hofbauer and Johannes Waldmann. The construction in this paper is complete but very inefficient.
- On tree automata that certify termination of left-linear term rewriting systems by Alfons Geser, Dieter Hofbauer, Johannes Waldmann and Hans Zantema. The construction in this paper is efficient but incomplete. We present the first automata construction for matchbounded string rewriting that is both efficient and complete. Here completenss means that the algorithm always terminates if the system is matchbounded.
See research for an overview of my research on termination.
Bibtex
@inproceedings{termination:matchbounds:2006, author = {Endrullis, J\"{o}rg and Hofbauer, Dieter and Waldmann, Johannes}, title = {{Decomposing Terminating Rewrite Relations}}, booktitle = {Proc.\ Workshop on Termination (WST~2006)}, pages = {39--43}, year = {2006}, keywords = {rewriting, termination, automata}, type = {workshop} }