-
Higher-Order Constrained Dependency Pairs for (Universal) Computability
Authors:
Liye Guo,
Kasper Hagens,
Cynthia Kop,
Deivid Vale
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-…
▽ More
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.
△ Less
Submitted 27 June, 2024;
originally announced June 2024.
-
A weakly monotonic, logically constrained, HORPO-variant
Authors:
Cynthia Kop
Abstract:
In this short paper, we present a simple variant of the recursive path ordering, specified for Logically Constrained Simply Typed Rewriting Systems (LCSTRSs). This is a method for curried systems, without lambda but with partially applied function symbols, which can deal with logical constraints. As it is designed for use in the dependency pair framework, it is defined as reduction pair, allowing…
▽ More
In this short paper, we present a simple variant of the recursive path ordering, specified for Logically Constrained Simply Typed Rewriting Systems (LCSTRSs). This is a method for curried systems, without lambda but with partially applied function symbols, which can deal with logical constraints. As it is designed for use in the dependency pair framework, it is defined as reduction pair, allowing weak monotonicity.
△ Less
Submitted 26 June, 2024;
originally announced June 2024.
-
On Basic Feasible Functionals and the Interpretation Method
Authors:
Patrick Baillot,
Ugo Dal Lago,
Cynthia Kop,
Deivid Vale
Abstract:
The class of basic feasible functionals $(\mathtt{BFF})$ is the analog of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $\mathtt{BFF}$ can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant form…
▽ More
The class of basic feasible functionals $(\mathtt{BFF})$ is the analog of $\mathtt{FP}$ (polynomial time functions) for type-2 functionals, that is, functionals that can take (first-order) functions as arguments. $\mathtt{BFF}$ can be defined through Oracle Turing machines with running time bounded by second-order polynomials. On the other hand, higher-order term rewriting provides an elegant formalism for expressing higher-order computation. We address the problem of characterizing $\mathtt{BFF}$ by higher-order term rewriting. Various kinds of interpretations for first-order term rewriting have been introduced in the literature for proving termination and characterizing (first-order) complexity classes. In this paper, we consider a recently introduced notion of cost-size interpretations for higher-order term rewriting and see definitions as ways of computing functionals. We then prove that the class of functionals represented by higher-order terms admitting a certain kind of cost-size interpretation is exactly $\mathtt{BFF}$.
△ Less
Submitted 25 January, 2024; v1 submitted 22 January, 2024;
originally announced January 2024.
-
Higher-Order LCTRSs and Their Termination
Authors:
Liye Guo,
Cynthia Kop
Abstract:
Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only analysis of imperative programs so far. In this paper, we present a higher-order variant of the LCTRS formalism, which can be used to analyze functional programs. Then we study the…
▽ More
Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only analysis of imperative programs so far. In this paper, we present a higher-order variant of the LCTRS formalism, which can be used to analyze functional programs. Then we study the termination problem and define a higher-order recursive path ordering (HORPO) for this new formalism.
△ Less
Submitted 25 July, 2023;
originally announced July 2023.
-
Complexity Analysis for Call-by-Value Higher-Order Rewriting
Authors:
Cynthia Kop,
Deivid Vale
Abstract:
In this short 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 briefly present a cost-size semantics to call-by-value rewriting: a class of algebraic interpretations that map terms to tuples that bound both the reductions' cost and the size of normal forms.
In this short 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 briefly present a cost-size semantics to call-by-value rewriting: a class of algebraic interpretations that map terms to tuples that bound both the reductions' cost and the size of normal forms.
△ Less
Submitted 25 July, 2023;
originally announced July 2023.
-
Certifying Higher-Order Polynomial Interpretations
Authors:
Niels van der Weide,
Deivid Vale,
Cynthia Kop
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, develo** such tools is difficult and can be…
▽ More
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, develo** 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, namely the polynomial interpretation method, that is used to prove termination. In addition, we give a program that turns the output of Wanda, a termination analysis tool for higher-order rewriting systems, into a Coq script, so that we can check whether the output is a valid proof of termination.
△ Less
Submitted 5 August, 2023; v1 submitted 23 February, 2023;
originally announced February 2023.
-
Tuple Interpretations and Applications to Higher-Order Runtime Complexity
Authors:
Cynthia Kop,
Deivid Vale
Abstract:
Tuple interpretations are a class of algebraic interpretation that subsumes both polynomial and matrix interpretations as it does not impose simple termination and allows non-linear interpretations. It was developed in the context of higher-order rewriting to study derivational complexity of algebraic functional systems. In this short paper, we continue our journey to study the complexity of highe…
▽ More
Tuple interpretations are a class of algebraic interpretation that subsumes both polynomial and matrix interpretations as it does not impose simple termination and allows non-linear interpretations. It was developed in the context of higher-order rewriting to study derivational complexity of algebraic functional systems. In this short paper, we continue our journey to study the complexity of higher-order TRSs by tailoring tuple interpretations to deal with innermost runtime complexity.
△ Less
Submitted 30 June, 2022;
originally announced June 2022.
-
Tuple Interpretations for Higher-Order Rewriting
Authors:
Deivid Vale,
Cynthia Kop
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 \emph{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 $\mathsf{nat}$ may be associated to a p…
▽ More
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 \emph{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 $\mathsf{nat}$ may be associated to a pair $(\mathsf{cost}, \mathsf{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.
△ Less
Submitted 3 May, 2021;
originally announced May 2021.
-
Cons-free Programs and Complexity Classes between LOGSPACE and PTIME
Authors:
Neil D. Jones,
Siddharth Bhaskar,
Cynthia Kop,
Jakob Grue Simonsen
Abstract:
Programming language concepts are used to give some new perspectives on a long-standing open problem: is logspace = ptime ?
Programming language concepts are used to give some new perspectives on a long-standing open problem: is logspace = ptime ?
△ Less
Submitted 6 August, 2020;
originally announced August 2020.
-
Polymorphic Higher-order Termination
Authors:
Łukasz Czajka,
Cynthia Kop
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…
▽ More
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.
△ Less
Submitted 22 April, 2019;
originally announced April 2019.
-
A static higher-order dependency pair framework
Authors:
Carsten Fuhs,
Cynthia Kop
Abstract:
We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways:
(1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applica…
▽ More
We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways:
(1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to render the framework more powerful. (5) We formulate several existing and new termination proving techniques in the form of processors within our framework.
The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.
△ Less
Submitted 4 April, 2019; v1 submitted 15 February, 2019;
originally announced February 2019.
-
The unified higher-order dependency pair framework
Authors:
Carsten Fuhs,
Cynthia Kop
Abstract:
In recent years, two higher-order extensions of the powerful dependency pair approach for termination analysis of first-order term rewriting have been defined: the static and the dynamic approach. Both approaches offer distinct advantages and disadvantages. However, a grand unifying theory is thus far missing, and both approaches lack the modularity present in the dependency pair framework commonl…
▽ More
In recent years, two higher-order extensions of the powerful dependency pair approach for termination analysis of first-order term rewriting have been defined: the static and the dynamic approach. Both approaches offer distinct advantages and disadvantages. However, a grand unifying theory is thus far missing, and both approaches lack the modularity present in the dependency pair framework commonly used in first-order rewriting. Moreover, neither approach can be used to prove non-termination.
In this paper, we aim to address this gap by defining a higher-order dependency pair framework, integrating both approaches into a shared formal setup. The framework has been implemented in the (fully automatic) higher-order termination tool WANDA.
△ Less
Submitted 23 May, 2018;
originally announced May 2018.
-
h: A Plank for Higher-order Attribute Contraction Schemes
Authors:
Cynthia Kop,
Kristoffer Rose
Abstract:
We present and formalize h, a core (or "plank") calculus that can serve as the foundation for several compiler specification languages, notably CRSX (Combinatory Reductions Systems with eXtensions), HACS (Higher-order Attribute Contraction Schemes), and TransScript. We discuss how the h ty** and formation rules introduce the necessary restrictions to ensure that rewriting is well-defined, even i…
▽ More
We present and formalize h, a core (or "plank") calculus that can serve as the foundation for several compiler specification languages, notably CRSX (Combinatory Reductions Systems with eXtensions), HACS (Higher-order Attribute Contraction Schemes), and TransScript. We discuss how the h ty** and formation rules introduce the necessary restrictions to ensure that rewriting is well-defined, even in the presence of h's powerful extensions for manipulating free variables and environments as first class elements (including in pattern matching).
△ Less
Submitted 9 November, 2017;
originally announced November 2017.
-
Cons-free Programming with Immutable Functions
Authors:
Cynthia Kop
Abstract:
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we set out to characterise the hierarchy NP $\subseteq$ NEXP $\subseteq$ NEXP$^{(2)}$ $\subseteq \cdots \subseteq$ NEXP$^{(k)}$ $\subseteq \cdots$ solely in terms of higher-typed, purely functional programs. Although the work is incomplete, we present an initial approach us…
▽ More
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we set out to characterise the hierarchy NP $\subseteq$ NEXP $\subseteq$ NEXP$^{(2)}$ $\subseteq \cdots \subseteq$ NEXP$^{(k)}$ $\subseteq \cdots$ solely in terms of higher-typed, purely functional programs. Although the work is incomplete, we present an initial approach using cons-free programs with immutable functions.
△ Less
Submitted 9 November, 2017;
originally announced November 2017.
-
Non-deterministic Characterisations
Authors:
Cynthia Kop
Abstract:
In this paper, we extend Jones' result -- that cons-free programming with $k^{th}$-order data and a call-by-value strategy characterises EXP$^k$TIME -- to a more general setting, including pattern-matching and non-deterministic choice. We show that the addition of non-determinism is unexpectedly powerful in the higher-order setting. Nevertheless, we can obtain a non-deterministic parallel to Jones…
▽ More
In this paper, we extend Jones' result -- that cons-free programming with $k^{th}$-order data and a call-by-value strategy characterises EXP$^k$TIME -- to a more general setting, including pattern-matching and non-deterministic choice. We show that the addition of non-determinism is unexpectedly powerful in the higher-order setting. Nevertheless, we can obtain a non-deterministic parallel to Jones' hierarchy result by appropriate restricting rule formation.
△ Less
Submitted 9 November, 2017;
originally announced November 2017.
-
Higher-order Cons-free Interpreters
Authors:
Cynthia Kop,
Jakob Grue Simonsen
Abstract:
Constructor rewriting systems are said to be cons-free if any constructor term occurring in the rhs of a rule must be a subterm of the lhs of the rule. Roughly, such systems cannot build new data structures during their evaluation. In earlier work by several authors, (typed) cons-free systems have been used to characterise complexity classes such as polynomial or exponential time or space by varyi…
▽ More
Constructor rewriting systems are said to be cons-free if any constructor term occurring in the rhs of a rule must be a subterm of the lhs of the rule. Roughly, such systems cannot build new data structures during their evaluation. In earlier work by several authors, (typed) cons-free systems have been used to characterise complexity classes such as polynomial or exponential time or space by varying the type orders, and the recursion forms allowed. This paper concerns the construction of interpreters for cons-free term rewriting. Due to their connection with proofs by diagonalisation, interpreters may be of use when studying separation results between complexity classes in implicit computational complexity theory. We are interested in interpreters of type order $k > 1$ that can interpret any term of strictly lower type order; while this gives us a well-known separation result E$^k$TIME $\subseteq$ E$^{k+1}$TIME, the hope is that more refined interpreters with syntactically limited constraints can be used to obtain a notion of faux diagonalisation and be used to attack open problems in complexity theory.
△ Less
Submitted 9 November, 2017;
originally announced November 2017.
-
On First-order Cons-free Term Rewriting and PTIME
Authors:
Cynthia Kop
Abstract:
In this paper, we prove that (first-order) cons-free term rewriting with a call-by-value reduction strategy exactly characterises the class of PTIME-computable functions. We use this to give an alternative proof of the result by Carvalho and Simonsen which states that cons-free term rewriting with linearity constraints characterises this class.
In this paper, we prove that (first-order) cons-free term rewriting with a call-by-value reduction strategy exactly characterises the class of PTIME-computable functions. We use this to give an alternative proof of the result by Carvalho and Simonsen which states that cons-free term rewriting with linearity constraints characterises this class.
△ Less
Submitted 13 November, 2017; v1 submitted 9 November, 2017;
originally announced November 2017.
-
Quasi-reductivity of Logically Constrained Term Rewriting Systems
Authors:
Cynthia Kop
Abstract:
This paper considers quasi-reductivity - essentially, the property that an evaluation cannot get "stuck" due to a missing case in pattern matching - in the context of term rewriting with logical constraints.
This paper considers quasi-reductivity - essentially, the property that an evaluation cannot get "stuck" due to a missing case in pattern matching - in the context of term rewriting with logical constraints.
△ Less
Submitted 8 February, 2017;
originally announced February 2017.
-
The Power of Non-Determinism in Higher-Order Implicit Complexity
Authors:
Cynthia Kop,
Jakob Grue Simonsen
Abstract:
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders, equipped with explicit non-deterministic choice. Cons-freeness roughly means that data constructors cannot occur in function bodies and all manipulation of storage space thus has to happen indirectly using the call stac…
▽ More
We investigate the power of non-determinism in purely functional programming languages with higher-order types. Specifically, we consider cons-free programs of varying data orders, equipped with explicit non-deterministic choice. Cons-freeness roughly means that data constructors cannot occur in function bodies and all manipulation of storage space thus has to happen indirectly using the call stack.
While cons-free programs have previously been used by several authors to characterise complexity classes, the work on non-deterministic programs has almost exclusively considered programs of data order 0. Previous work has shown that adding explicit non-determinism to cons-free programs taking data of order 0 does not increase expressivity; we prove that this - dramatically - is not the case for higher data orders: adding non-determinism to programs with data order at least 1 allows for a characterisation of the entire class of elementary-time decidable sets.
Finally we show how, even with non-deterministic choice, the original hierarchy of characterisations is restored by imposing different restrictions.
△ Less
Submitted 30 January, 2017; v1 submitted 19 January, 2017;
originally announced January 2017.
-
Complexity Hierarchies and Higher-order Cons-free Term Rewriting
Authors:
Cynthia Kop,
Jakob Grue Simonsen
Abstract:
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of the left-hand sides; the computational intuition is that rules cannot build new data structures. In programming language research, cons-free languages have been used to characterize hierarchies of computational complexity classes; in term rewriting, cons-free first…
▽ More
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of the left-hand sides; the computational intuition is that rules cannot build new data structures. In programming language research, cons-free languages have been used to characterize hierarchies of computational complexity classes; in term rewriting, cons-free first-order TRSs have been used to characterize the class PTIME.
We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the type order of the systems. We prove that, for every K $\geq$ 1, left-linear cons-free systems with type order K characterize E$^K$TIME if unrestricted 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 no assumptions on reduction strategy, (ii) we consequently obtain much larger classes for each type order (E$^K$TIME versus EXP$^{K-1}$TIME), and (iii) results for cons-free term rewriting systems have previously only been obtained for K = 1, and with additional syntactic restrictions besides cons-freeness and left-linearity.
Our results are among the first implicit characterizations of the hierarchy E = E$^1$TIME $\subsetneq$ E$^2$TIME $\subsetneq$ ... Our work confirms prior results that having full non-determinism (via overlap** 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 like admitting product types or non-left-linear rules.
△ Less
Submitted 4 August, 2017; v1 submitted 30 November, 2016;
originally announced November 2016.
-
Complexity Hierarchies and Higher-Order Cons-Free Rewriting
Authors:
Cynthia Kop,
Jakob Grue Simonsen
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 t…
▽ More
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 $\geq$ 1, left-linear cons-free systems with type order k characterize E$^k$TIME 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 = E$^1$TIME $\subseteq$ E$^2$TIME $\subseteq$ .... Our work confirms prior results that having full non-determinism (via overlaps of rules) does not directly allow 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.
△ Less
Submitted 29 April, 2016;
originally announced April 2016.
-
Termination of LCTRSs
Authors:
Cynthia Kop
Abstract:
Logically Constrained Term Rewriting Systems (LCTRSs) provide a general framework for term rewriting with constraints. We discuss a simple dependency pair approach to prove termination of LCTRSs. We see that existing techniques transfer to the constrained setting in a natural way.
Logically Constrained Term Rewriting Systems (LCTRSs) provide a general framework for term rewriting with constraints. We discuss a simple dependency pair approach to prove termination of LCTRSs. We see that existing techniques transfer to the constrained setting in a natural way.
△ Less
Submitted 13 January, 2016;
originally announced January 2016.
-
Complexity of Conditional Term Rewriting
Authors:
Cynthia Kop,
Aart Middeldorp,
Thomas Sternagel
Abstract:
We propose a notion of complexity for oriented conditional term rewrite systems satisfying certain restrictions. 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 wel…
▽ More
We propose a notion of complexity for oriented conditional term rewrite systems satisfying certain restrictions. 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 result of this transformation.
△ Less
Submitted 22 March, 2017; v1 submitted 25 October, 2015;
originally announced October 2015.
-
Verifying Procedural Programs via Constrained Rewriting Induction
Authors:
Carsten Fuhs,
Cynthia Kop,
Naoki Nishida
Abstract:
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle arbitrary data types, global variables, function calls and arrays, as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and pro…
▽ More
This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend transformation methods based on integer TRSs to handle arbitrary data types, global variables, function calls and arrays, as well as encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations, so in contrast to other works, we do not require an explicit specification in a separate specification language.
△ Less
Submitted 25 February, 2017; v1 submitted 30 August, 2014;
originally announced September 2014.
-
First-Order Formative Rules
Authors:
Carsten Fuhs,
Cynthia Kop
Abstract:
This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, formative rules allow drop** some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the tech…
▽ More
This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, formative rules allow drop** some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the technique.
△ Less
Submitted 30 April, 2014;
originally announced April 2014.
-
Dynamic Dependency Pairs for Algebraic Functional Systems
Authors:
Cynthia Kop,
Femke van Raamsdonk
Abstract:
We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate β-steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we define a variation of usable rules and an extension of argument filterings. All these techniqu…
▽ More
We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate β-steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we define a variation of usable rules and an extension of argument filterings. All these techniques have been implemented in the higher-order termination tool WANDA.
△ Less
Submitted 15 June, 2012; v1 submitted 11 May, 2012;
originally announced May 2012.
-
Polynomial Interpretations for Higher-Order Rewriting
Authors:
Carsten Fuhs,
Cynthia Kop
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-orde…
▽ More
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.
△ Less
Submitted 26 March, 2012;
originally announced March 2012.
