DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2025.20

An Innermost DP Framework for Constrained Higher-Order Rewriting

Authors: Carsten Fuhs, Liye Guo, and Cynthia Kop

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

Logically constrained simply-typed term rewriting systems (LCSTRSs) are a higher-order formalism for program analysis with support for primitive data types. The termination problem of LCSTRSs has been studied so far in the setting of full rewriting. This paper modifies the higher-order constrained dependency pair framework to prove innermost termination, which corresponds to the termination of programs under call by value. We also show that the notion of universal computability with respect to innermost rewriting can be effectively handled in the modified, innermost framework, which lays the foundation for open-world termination analysis of programs under call by value via LCSTRSs.

Cite as

Carsten Fuhs, Liye Guo, and Cynthia Kop. An Innermost DP Framework for Constrained Higher-Order Rewriting. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{fuhs_et_al:LIPIcs.FSCD.2025.20,
  author =	{Fuhs, Carsten and Guo, Liye and Kop, Cynthia},
  title =	{{An Innermost DP Framework for Constrained Higher-Order Rewriting}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{20:1--20:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.20},
  URN =		{urn:nbn:de:0030-drops-236359},
  doi =		{10.4230/LIPIcs.FSCD.2025.20},
  annote =	{Keywords: Higher-order term rewriting, constrained rewriting, innermost termination, call by value, open-world analysis, dependency pairs}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2024.57

Higher-Order Constrained Dependency Pairs for (Universal) Computability

Authors: Liye Guo, Kasper Hagens, Cynthia Kop, and Deivid Vale

Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

Abstract

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.

Cite as

Liye Guo, Kasper Hagens, Cynthia Kop, and Deivid Vale. Higher-Order Constrained Dependency Pairs for (Universal) Computability. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 57:1-57:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guo_et_al:LIPIcs.MFCS.2024.57,
  author =	{Guo, Liye and Hagens, Kasper and Kop, Cynthia and Vale, Deivid},
  title =	{{Higher-Order Constrained Dependency Pairs for (Universal) Computability}},
  booktitle =	{49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)},
  pages =	{57:1--57:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-335-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{306},
  editor =	{Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.57},
  URN =		{urn:nbn:de:0030-drops-206137},
  doi =		{10.4230/LIPIcs.MFCS.2024.57},
  annote =	{Keywords: Higher-order term rewriting, constrained rewriting, dependency pairs}
}

Search Results

Documents authored by Guo, Liye

An Innermost DP Framework for Constrained Higher-Order Rewriting

Abstract

Cite as

Higher-Order Constrained Dependency Pairs for (Universal) Computability

Abstract

Cite as

Thanks for your feedback!

Could not send message