From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting

Lecture notes in computer science, pp. 206–228

Abstract

Abstract There are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems. These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool .

Authors 3

1. Jan-Christoph Kassing corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

2. Florian Frohn corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany

3. Jürgen Giesl corresponding Aachen LuFG Informatik 2

   RWTH Aachen University

   Affiliation as printed

   LuFG Informatik 2, RWTH Aachen University, Aachen, Germany