Higher-Order Constrained Dependency Pairs for (Universal) Computability
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_ | 1866911971772727296 |
|---|---|
| author | Guo, Liye Hagens, Kasper Kop, Cynthia Vale, Deivid |
| author_facet | Guo, Liye Hagens, Kasper Kop, Cynthia Vale, Deivid |
| contents | Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order formalism with logical constraints built in. We also propose the concept of universal computability, which enables a form of open-world termination analysis through the use of static dependency pairs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_19379 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Higher-Order Constrained Dependency Pairs for (Universal) Computability Guo, Liye Hagens, Kasper Kop, Cynthia Vale, Deivid Logic in Computer Science Dependency pairs constitute a series of very effective techniques for the termination analysis of term rewriting systems. In this paper, we adapt the static dependency pair framework to logically constrained simply-typed term rewriting systems (LCSTRSs), a higher-order formalism with logical constraints built in. We also propose the concept of universal computability, which enables a form of open-world termination analysis through the use of static dependency pairs. |
| title | Higher-Order Constrained Dependency Pairs for (Universal) Computability |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2406.19379 |