From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911775490834432 |
|---|---|
| author | Kassing, Jan-Christoph Frohn, Florian Giesl, Jürgen |
| author_facet | Kassing, Jan-Christoph Frohn, Florian Giesl, Jürgen |
| contents | 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 (PTRSs). These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_06121 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting Kassing, Jan-Christoph Frohn, Florian Giesl, Jürgen Logic in Computer Science 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 (PTRSs). These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool AProVE. |
| title | From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2310.06121 |