2026-07-24T08:01:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20613 2024-08-23T05:50:29Z ddc:004 open_access

Higher-Order Constrained Dependency Pairs for (Universal) Computability Guo, Liye Hagens, Kasper Kop, Cynthia Vale, Deivid Higher-order term rewriting constrained rewriting dependency pairs 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Liye Guo and Kasper Hagens and Cynthia Kop and Deivid Vale 2024 Is Part Of LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2024.57 urn:nbn:de:0030-drops-206137 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.57 eng https://creativecommons.org/licenses/by/4.0/legalcode