2015

  1. Proving Non-Termination by Finite Automata
    Jörg Endrullis, and Hans Zantema
    In: 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

  1. SAT Compilation for Termination Proofs via Semantic Labelling
    Alexander Bau, Jörg Endrullis, and Johannes Waldmann
    In: 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}
}

    Digital Object Identifier

2011

  1. Lazy Productivity via Termination
    Jörg Endrullis, and Dimitri Hendriks
    Theoretical 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
  2. Levels of Undecidability in Rewriting
    Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen, and Hans Zantema
    Information 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

  1. Local Termination: Theory and Practice
    Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann
    Logical 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
  2. Transforming Outermost into Context-Sensitive Rewriting
    Jörg Endrullis, and Dimitri Hendriks
    Logical 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

  1. From Outermost to Context-Sensitive Rewriting
    Jörg Endrullis, and Dimitri Hendriks
    In: 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
  2. Local Termination
    Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann
    In: 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
  3. Degrees of Undecidability in Term Rewriting
    Jörg Endrullis, Herman Geuvers, and Hans Zantema
    In: 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

  1. Matrix Interpretations for Proving Termination of Term Rewriting
    Jörg Endrullis, Johannes Waldmann, and Hans Zantema
    Journal 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

  1. Root Stabilisation Using Dependency Pairs
    Jörg Endrullis, and Jeroen Ketema
    In: 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}
}

    Digital Object Identifier

2006

  1. Matrix Interpretations for Proving Termination of Term Rewriting
    Jörg Endrullis, Johannes Waldmann, and Hans Zantema
    In: 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
  2. Decomposing Terminating Rewrite Relations
    Jörg Endrullis, Dieter Hofbauer, and Johannes Waldmann
    In: 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}
}

    Digital Object Identifier