Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting

Jan-Christoph Kassing, Leon Spitzer, Jürgen Giesl

TL;DR

The paper develops the first dependency-pair framework tailored to strong almost-sure termination (SAST) and the expected innermost runtime complexity of probabilistic term rewrite systems (PTRSs) under innermost strategy. Central to the approach are annotated dependency pairs (ADPs), which preserve the original rule structure while marking calls that influence complexity, enabling a tight chain criterion via chain trees. A collection of processors (usable rules, dependency graph, reduction pair, knowledge propagation, probability removal, and more) enables modular, automatic upper bounds, and the method is implemented in AProVE. Evaluation on a broad PTRS benchmark shows substantial improvements over prior tools (POLO, NaTT) in proving SAST and obtaining meaningful complexity bounds, highlighting the framework's practicality and scalability for automatic PTRS analysis.

Abstract

The dependency pair (DP) framework is one of the most powerful techniques for automatic termination and complexity analysis of term rewrite systems. While DPs were extended to prove almost-sure termination of probabilistic term rewrite systems (PTRSs), automatic complexity analysis for PTRSs is largely unexplored. We introduce the first DP framework for analyzing expected complexity and for proving positive or strong almost-sure termination (SAST) of innermost rewriting with PTRSs, i.e., finite expected runtime. We implemented our framework in the tool AProVE and demonstrate its power compared to existing techniques for proving SAST.

Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting

TL;DR

The paper develops the first dependency-pair framework tailored to strong almost-sure termination (SAST) and the expected innermost runtime complexity of probabilistic term rewrite systems (PTRSs) under innermost strategy. Central to the approach are annotated dependency pairs (ADPs), which preserve the original rule structure while marking calls that influence complexity, enabling a tight chain criterion via chain trees. A collection of processors (usable rules, dependency graph, reduction pair, knowledge propagation, probability removal, and more) enables modular, automatic upper bounds, and the method is implemented in AProVE. Evaluation on a broad PTRS benchmark shows substantial improvements over prior tools (POLO, NaTT) in proving SAST and obtaining meaningful complexity bounds, highlighting the framework's practicality and scalability for automatic PTRS analysis.

Abstract

The dependency pair (DP) framework is one of the most powerful techniques for automatic termination and complexity analysis of term rewrite systems. While DPs were extended to prove almost-sure termination of probabilistic term rewrite systems (PTRSs), automatic complexity analysis for PTRSs is largely unexplored. We introduce the first DP framework for analyzing expected complexity and for proving positive or strong almost-sure termination (SAST) of innermost rewriting with PTRSs, i.e., finite expected runtime. We implemented our framework in the tool AProVE and demonstrate its power compared to existing techniques for proving SAST.

Paper Structure

This paper contains 24 sections, 17 theorems, 39 equations, 7 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Term Rewriting
  4. Probabilistic Rewriting
  5. Annotated Dependency Pairs
  6. ADP Problems
  7. ADP Framework
  8. ADP Processors
  9. Usable Rules Processor
  10. Dependency Graph Processor
  11. Reduction Pair Processor
  12. Knowledge Propagation Processor
  13. Probability Removal Processor
  14. Further Processors
  15. Evaluation
  16. ...and 9 more sections

Key Result

theorem 1

Let $\mathcal{R}$ be a PTRS. Then for all basic terms $t \in \mathcal{B}\!\mathcal{T}_\mathcal{R}$ we have and therefore $\iota_\mathcal{R} = \iota_{\langle \mathcal{A}(\mathcal{R}), \mathcal{A}(\mathcal{R}) \rangle}$.

Figures (7)

  • Figure 1: ${\mathcal{R}_{\mathsf{geo}}}$-Rewrite sequence tree starting with $\mathsf{geo}(\mathsf{0})$
  • Figure 2: ${\mathcal{A}(\mathcal{R}_{\mathsf{geo}})}$-Chain tree starting with $\mathsf{Geo}(\mathsf{0})$
  • Figure 3: Example of a solved proof tree
  • Figure 4: $\mathcal{P}_1$-dependency graph
  • Figure 5: $\mathcal{A}(\mathcal{R}_2)$-dependency graph
  • ...and 2 more figures

Theorems & Definitions (38)

  • definition 1: Runtime Complexity, $\mathrm{rc}_\mathcal{R}$ DBLP:conf/cade/HirokawaM08
  • definition 2: Asymptotic Complexities
  • definition 3: Expected Runtime Complexity, $\mathrm{erc}_{\mathcal{R}}$
  • definition 4: Strong Almost-Sure Termination, $\operatorname{\texttt{SAST}}$
  • definition 5: Annotations
  • definition 6: Annotated Dependency Pairs
  • definition 7: $\mathrel{ \xhookrightarrow{{}_{\mathsf{i}}} \!\!{}^{}_{\mathcal{P}} }$
  • definition 8: Chain Tree
  • definition 9: Exp. Derivation Length for Chain Trees, $\operatorname{edl}_{\langle \mathcal{P}, \mathcal{S} \rangle}$
  • definition 10: Exp. Derivation Height via Chain Trees, $\operatorname{edh}_{\langle \mathcal{P}, \mathcal{S} \rangle}$
  • ...and 28 more