From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912769038614528 |
|---|---|
| author | Kassing, Jan-Christoph Giesl, Jürgen |
| author_facet | Kassing, Jan-Christoph Giesl, Jürgen |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_17714 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity Kassing, Jan-Christoph Giesl, Jürgen Logic in Computer Science 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. |
| title | From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2409.17714 |