Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity

Jan-Christoph Kassing, Jürgen Giesl

TL;DR

This work extends the dependency-pairs paradigm to probabilistic term rewriting, establishing sufficient criteria under which innermost termination and its complexity notions coincide with full rewriting and corresponding expected complexities. It formalizes PTRS notions, defines AST/PAST/SAST and edc/erc, and proves criteria ensuring transfer of termination properties across evaluation strategies (innermost, leftmost-innermost, and full). The authors implement these criteria in AProVE, demonstrate practical applicability, and derive modularity results for PTRSs under disjoint unions and signature extensions, including a detailed discussion of spareness and the limits of left-linearity removal. Collectively, the results advance automated verification of probabilistic programs modeled by PTRSs and provide concrete guidance for modular termination/complexity proofs. The findings have practical impact on certifying termination properties and runtime bounds for probabilistic rewrite-based specifications, with implications for tool support and modular reasoning in probabilistic programming verification.

Abstract

There are many evaluation strategies for term rewrite systems, but automatically proving termination or analyzing complexity is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies (full) termination or when runtime complexity and innermost runtime complexity coincide. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination w.r.t. innermost rewriting in order to prove (full) almost-sure termination of probabilistic term rewrite systems. These criteria can be applied for both termination and complexity analysis in the probabilistic setting. We implemented and evaluated our new contributions in the tool AProVE. Moreover, we also use our new results to investigate the modularity of probabilistic termination properties.

From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity

TL;DR

This work extends the dependency-pairs paradigm to probabilistic term rewriting, establishing sufficient criteria under which innermost termination and its complexity notions coincide with full rewriting and corresponding expected complexities. It formalizes PTRS notions, defines AST/PAST/SAST and edc/erc, and proves criteria ensuring transfer of termination properties across evaluation strategies (innermost, leftmost-innermost, and full). The authors implement these criteria in AProVE, demonstrate practical applicability, and derive modularity results for PTRSs under disjoint unions and signature extensions, including a detailed discussion of spareness and the limits of left-linearity removal. Collectively, the results advance automated verification of probabilistic programs modeled by PTRSs and provide concrete guidance for modular termination/complexity proofs. The findings have practical impact on certifying termination properties and runtime bounds for probabilistic rewrite-based specifications, with implications for tool support and modular reasoning in probabilistic programming verification.

Abstract

There are many evaluation strategies for term rewrite systems, but automatically proving termination or analyzing complexity is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies (full) termination or when runtime complexity and innermost runtime complexity coincide. We adapt these criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination w.r.t. innermost rewriting in order to prove (full) almost-sure termination of probabilistic term rewrite systems. These criteria can be applied for both termination and complexity analysis in the probabilistic setting. We implemented and evaluated our new contributions in the tool AProVE. Moreover, we also use our new results to investigate the modularity of probabilistic termination properties.
Paper Structure (26 sections, 51 theorems, 107 equations, 10 figures, 1 table)

This paper contains 26 sections, 51 theorems, 107 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Termination
  4. Complexity
  5. Probabilistic Term Rewriting
  6. Probabilistic Term Rewriting
  7. Probabilistic Notions of Termination
  8. Relating Positive and Strong Almost-Sure Termination
  9. Relating Variants of Probabilistic Termination and Expected Complexity
  10. From $\mathtt{PSN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{i}\:$}}{{\rightarrow}}}}_{\mathcal{P}}}$ to $\mathtt{PSN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{P}}}$
  11. From $\mathtt{wPSN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{P}}}$ to $\mathtt{PSN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{P}}}$
  12. From $\mathtt{PSN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{li}\:$}}{{\rightarrow}}}}_{\mathcal{P}}}$ to $\mathtt{PSN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{P}}}$
  13. Improving Applicability
  14. Attempting to Remove Left-Linearity by Simultaneous Rewriting
  15. Weakening Right-Linearity to Spareness
  16. ...and 11 more sections

Key Result

Theorem 2.2

If a TRS $\mathcal{R}$ is OR, then:

Figures (10)

  • Figure 1: Relations between the different termination properties for TRSs
  • Figure 2: Corresponding RST for the $\mathrel{{\stackrel{\raisebox{3.4pt}{\tiny $\mathbf{f}\:$}}{{\rightrightarrows}}}}_{\mathcal{P}_{\mathsf{rw}}}$-rewrite sequence in \ref{['example:PTRS-random-walk-lifting-sequence']}.
  • Figure 3: Relations between the different termination properties for PTRSs
  • Figure 4: Relations for expected complexity
  • Figure 5: Tree $\mathfrak{T}_x$ in the Construction of $\Phi(\_)$
  • ...and 5 more figures

Theorems & Definitions (116)

  • Theorem 2.2: From $\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{i}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$ to ${\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{R}}} }$ (1), ODonnell77
  • Theorem 2.3: From $\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{i}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$ to ${\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{R}}} }$ (2), Gramlich1995AbstractRB
  • Theorem 2.4: From $\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{i}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$ to ${\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{R}}} }$ (3), Gramlich1995AbstractRB
  • Theorem 2.6: From $\mathtt{WN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$ to ${\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{R}}} }$, Gramlich1995AbstractRB
  • Theorem 2.7: From $\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{li}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$ to $\mathtt{SN}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{i}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$, KRISHNARAO2000141
  • Theorem 2.9: From $\operatorname{rc}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{i}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$ to $\operatorname{rc}_{\mathrel{{\stackrel{\raisebox{2pt}{$\mathbf{f}\:$}}{{\rightarrow}}}}_{\mathcal{R}}}$, frohn_analyzing_nodate
  • Definition 3.1: Lifting
  • Example 3.2
  • Definition 3.3: $|\mu|_{\to}$, $|\mu|_{\mathcal{P}}$
  • Example 3.4
  • ...and 106 more