Search Results

Documents authored by Kop, Cynthia

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}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.30
Certifying Higher-Order Polynomial Interpretations

Authors: Niels van der Weide, Deivid Vale, and Cynthia Kop

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually halts its execution and produces an output. Several tools have been developed to check whether higher-order rewriting systems are terminating. However, developing such tools is difficult and can be error-prone. In this paper, we present a way of certifying termination proofs of higher-order term rewriting systems. We formalize a specific method that is used to prove termination, namely the polynomial interpretation method. In addition, we give a program that processes proof traces containing a high-level description of a termination proof into a formal Coq proof script that can be checked by Coq. We demonstrate the usability of this approach by certifying higher-order polynomial interpretation proofs produced by Wanda, a termination analysis tool for higher-order rewriting.
Cite as

Niels van der Weide, Deivid Vale, and Cynthia Kop. Certifying Higher-Order Polynomial Interpretations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vanderweide_et_al:LIPIcs.ITP.2023.30,
  author =	{van der Weide, Niels and Vale, Deivid and Kop, Cynthia},
  title =	{{Certifying Higher-Order Polynomial Interpretations}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{30:1--30:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.30},
  URN =		{urn:nbn:de:0030-drops-184051},
  doi =		{10.4230/LIPIcs.ITP.2023.30},
  annote =	{Keywords: higher-order rewriting, Coq, termination, formalization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.15
Cost-Size Semantics for Call-By-Value Higher-Order Rewriting

Authors: Cynthia Kop and Deivid Vale

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
Higher-order rewriting is a framework in which higher-order programs can be described by transformation rules on expressions. A computation occurs by transforming an expression into another using such rules. This step-by-step computation model induced by rewriting naturally gives rise to a notion of complexity as the number of steps needed to reduce expressions to a normal form, i.e., an expression that cannot be reduced further. The study of complexity analysis focuses on the development of automatable techniques to provide bounds to this number. In this paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy, so as to model call-by-value programs. We provide a cost-size semantics: a class of algebraic interpretations to map terms to tuples which bound both the reduction cost and the size of normal forms.
Cite as

Cynthia Kop and Deivid Vale. Cost-Size Semantics for Call-By-Value Higher-Order Rewriting. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.FSCD.2023.15,
  author =	{Kop, Cynthia and Vale, Deivid},
  title =	{{Cost-Size Semantics for Call-By-Value Higher-Order Rewriting}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.15},
  URN =		{urn:nbn:de:0030-drops-179993},
  doi =		{10.4230/LIPIcs.FSCD.2023.15},
  annote =	{Keywords: Call-by-Value Evaluation, Complexity Theory, Higher-Order Rewriting}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2022.1
Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk)

Authors: Cynthia Kop

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
This paper discusses a number of methods to prove termination of higher-order term rewriting systems, with a particular focus on large systems. In first-order term rewriting, the dependency pair framework can be used to split up a large termination problem into multiple (much) smaller components that can be solved individually. This is important because a large problem may take exponentially longer to solve in one go than solving each of its components. Unfortunately, while there are higher-order versions of several of these methods, they often fail to simplify a problem enough. Here, we will explore some of these techniques and their limitations, and discuss what else can be done to incrementally build a termination proof for higher-order systems.
Cite as

Cynthia Kop. Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting (Invited Talk). In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kop:LIPIcs.FSCD.2022.1,
  author =	{Kop, Cynthia},
  title =	{{Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{1:1--1:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.1},
  URN =		{urn:nbn:de:0030-drops-162827},
  doi =		{10.4230/LIPIcs.FSCD.2022.1},
  annote =	{Keywords: Termination, Modularity, Higher-order term rewriting, Dependency Pairs, Algebra Interpretations}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.31
Tuple Interpretations for Higher-Order Complexity

Authors: Cynthia Kop and Deivid Vale

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to tuples of natural numbers and higher-order terms to functions between those tuples. Tuples may carry information relevant to the type; for instance, a term of type nat may be associated to a pair ⟨ cost, size ⟩ representing its evaluation cost and size. This class of interpretations results in a more fine-grained notion of complexity than runtime or derivational complexity, which makes it particularly useful to obtain complexity bounds for higher-order rewriting systems. We show that rewriting systems compatible with tuple interpretations admit finite bounds on derivation height. Furthermore, we demonstrate how to mechanically construct tuple interpretations and how to orient β and η reductions within our technique. Finally, we relate our method to runtime complexity and prove that specific interpretation shapes imply certain runtime complexity bounds.
Cite as

Cynthia Kop and Deivid Vale. Tuple Interpretations for Higher-Order Complexity. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.FSCD.2021.31,
  author =	{Kop, Cynthia and Vale, Deivid},
  title =	{{Tuple Interpretations for Higher-Order Complexity}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{31:1--31:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.31},
  URN =		{urn:nbn:de:0030-drops-142692},
  doi =		{10.4230/LIPIcs.FSCD.2021.31},
  annote =	{Keywords: Complexity, higher-order term rewriting, many-sorted term rewriting, polynomial interpretations, weakly monotonic algebras}
}
Document
System Description
DOI: 10.4230/LIPIcs.FSCD.2020.36
WANDA - a Higher Order Termination Tool (System Description)

Authors: Cynthia Kop

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Wanda is a fully automatic termination analysis tool for higher-order term rewriting. In this paper, we will discuss the methodology used in Wanda. Most pertinently, this includes a higher-order dependency pair framework and a variation of the higher-order recursive path ordering, as well as some non-termination analysis techniques and delegation to a first-order tool. Additionally, we will discuss Wanda’s internal rewriting formalism, and how to use Wanda in practice for systems in two different formalisms. We also present experimental results that consider both formalisms.
Cite as

Cynthia Kop. WANDA - a Higher Order Termination Tool (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kop:LIPIcs.FSCD.2020.36,
  author =	{Kop, Cynthia},
  title =	{{WANDA - a Higher Order Termination Tool}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.36},
  URN =		{urn:nbn:de:0030-drops-123587},
  doi =		{10.4230/LIPIcs.FSCD.2020.36},
  annote =	{Keywords: higher-order term rewriting, termination, automatic analysis, dependency pair framework, higher-order recursive path ordering}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.12
Polymorphic Higher-Order Termination

Authors: Łukasz Czajka and Cynthia Kop

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System F_omega. This enables a direct interpretation of rewrite rules which make essential use of impredicative polymorphism. In addition, our generalisation eases the applicability of the method in the non-polymorphic setting by allowing for the encoding of inductive data types. As an illustration of the potential of our method, we prove termination of a substantial fragment of full intuitionistic second-order propositional logic with permutative conversions.
Cite as

Łukasz Czajka and Cynthia Kop. Polymorphic Higher-Order Termination. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czajka_et_al:LIPIcs.FSCD.2019.12,
  author =	{Czajka, {\L}ukasz and Kop, Cynthia},
  title =	{{Polymorphic Higher-Order Termination}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.12},
  URN =		{urn:nbn:de:0030-drops-105193},
  doi =		{10.4230/LIPIcs.FSCD.2019.12},
  annote =	{Keywords: termination, polymorphism, higher-order rewriting, permutative conversions}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.23
Complexity Hierarchies and Higher-Order Cons-Free Rewriting

Authors: Cynthia Kop and Jakob Grue Simonsen

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the computational intuition is that rules cannot build new data structures. It is well-known that cons-free programming languages can be used to characterize computational complexity classes, and that cons-free first-order term rewriting can be used to characterize the set of polynomial-time decidable sets. We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the order of the types used in the systems. We prove that, for every k >= 1, left-linear cons-free systems with type order k characterize E^kTIME if arbitrary evaluation is used (i.e., the system does not have a fixed reduction strategy). The main difference with prior work in implicit complexity is that (i) our results hold for non-orthogonal term rewriting systems with possible rule overlaps with no assumptions about reduction strategy, (ii) results for such term rewriting systems have previously only been obtained for k = 1, and with additional syntactic restrictions on top of cons-freeness and left-linearity. Our results are apparently among the first implicit characterizations of the hierarchy E^1TIME != E^2TIME != .... Our work confirms prior results that having full non-determinism (via overlaps of rules) does not directly allow for characterization of non-deterministic complexity classes like NE. We also show that non-determinism makes the classes characterized highly sensitive to minor syntactic changes such as admitting product types or non-left-linear rules.
Cite as

Cynthia Kop and Jakob Grue Simonsen. Complexity Hierarchies and Higher-Order Cons-Free Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.FSCD.2016.23,
  author =	{Kop, Cynthia and Grue Simonsen, Jakob},
  title =	{{Complexity Hierarchies and Higher-Order Cons-Free Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.23},
  URN =		{urn:nbn:de:0030-drops-59972},
  doi =		{10.4230/LIPIcs.FSCD.2016.23},
  annote =	{Keywords: higher-order term rewriting, implicit complexity, cons-freeness, ETIME hierarchy}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.223
Conditional Complexity

Authors: Cynthia Kop, Aart Middeldorp, and Thomas Sternagel

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We propose a notion of complexity for oriented conditional term rewrite systems. This notion is realistic in the sense that it measures not only successful computations but also partial computations that result in a failed rule application. A transformation to unconditional context-sensitive rewrite systems is presented which reflects this complexity notion, as well as a technique to derive runtime and derivational complexity bounds for the latter.
Cite as

Cynthia Kop, Aart Middeldorp, and Thomas Sternagel. Conditional Complexity. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 223-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.RTA.2015.223,
  author =	{Kop, Cynthia and Middeldorp, Aart and Sternagel, Thomas},
  title =	{{Conditional Complexity}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{223--240},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  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.RTA.2015.223},
  URN =		{urn:nbn:de:0030-drops-51999},
  doi =		{10.4230/LIPIcs.RTA.2015.223},
  annote =	{Keywords: conditional term rewriting, complexity}
}
Document
DOI: 10.4230/LIPIcs.RTA.2012.176
Polynomial Interpretations for Higher-Order Rewriting

Authors: Carsten Fuhs and Cynthia Kop

Published in: LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012)

Abstract
The termination method of weakly monotonic algebras, which has been defined for higher-order rewriting in the HRS formalism, offers a lot of power, but has seen little use in recent years. We adapt and extend this method to the alternative formalism of algebraic functional systems, where the simply-typed lambda-calculus is combined with algebraic reduction. Using this theory, we define higher-order polynomial interpretations, and show how the implementation challenges of this technique can be tackled. A full implementation is provided in the termination tool Wanda.
Cite as

Carsten Fuhs and Cynthia Kop. Polynomial Interpretations for Higher-Order Rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 176-192, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{fuhs_et_al:LIPIcs.RTA.2012.176,
  author =	{Fuhs, Carsten and Kop, Cynthia},
  title =	{{Polynomial Interpretations for Higher-Order Rewriting}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12)},
  pages =	{176--192},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Tiwari, Ashish},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.176},
  URN =		{urn:nbn:de:0030-drops-34924},
  doi =		{10.4230/LIPIcs.RTA.2012.176},
  annote =	{Keywords: higher-order rewriting, termination, polynomial interpretations, weakly monotonic algebras, automation}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.203
Higher Order Dependency Pairs for Algebraic Functional Systems

Authors: Cynthia Kop and Femke van Raamsdonk

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
We extend the termination method using dynamic dependency pairs to higher order rewriting systems with beta as a rewrite step, also called Algebraic Functional Systems (AFSs). We introduce a variation of usable rules, and use monotone algebras to solve the constraints generated by dependency pairs. This approach differs in several respects from those dealing with higher order rewriting modulo beta (e.g. HRSs).
Cite as

Cynthia Kop and Femke van Raamsdonk. Higher Order Dependency Pairs for Algebraic Functional Systems. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 203-218, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.RTA.2011.203,
  author =	{Kop, Cynthia and van Raamsdonk, Femke},
  title =	{{Higher Order Dependency Pairs for Algebraic Functional Systems}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{203--218},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.203},
  URN =		{urn:nbn:de:0030-drops-31177},
  doi =		{10.4230/LIPIcs.RTA.2011.203},
  annote =	{Keywords: higher order rewriting, termination, dynamic dependency pairs}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact