Size-based termination of higher-order rewriting
From MaRDI portal
Abstract: We provide a general and modular criterion for the termination of simply-typed -calculus extended with function symbols defined by user-defined rewrite rules. Following a work of Hughes, Pareto and Sabry for functions defined with a fixpoint operator and pattern-matching, several criteria use typing rules for bounding the height of arguments in function calls. In this paper, we extend this approach to rewriting-based function definitions and more general user-defined notions of size.
Recommendations
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- Rewriting Techniques and Applications
- Normal higher-order termination
- scientific article; zbMATH DE number 2043534
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
Cites work
- A domain model characterising strong normalisation
- A lattice-theoretical fixpoint theorem and its applications
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A Machine-Oriented Logic Based on the Resolution Principle
- A Monotonic Higher-Order Semantic Path Ordering
- A note on simplification orderings
- A predicative analysis of structural recursion
- A proof of strong normalisation using domain theory
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- A system of abstract constructive ordinals
- A theory of type polymorphism in programming
- An initial algebra approach to term rewriting systems with variable binders
- An ordinal calculus for proving termination in term rewriting
- An ordinal measure based procedure for termination of functions
- Automating the dependency pair method
- Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems
- Calculating sized types
- Call-by-value Termination in the Untyped lambda-calculus
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
- Closing the gap between runtime complexity and polytime computability
- Coherence of subsumption, minimum typing and type-checking in F ≤
- Combinatory reduction systems: Introduction and survey
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- Complexity bounds for ordinal-based termination (invited talk)
- Computer Science Logic
- Constructive versions of Tarski's fixed point theorems
- Definitions by rewriting in the Calculus of Constructions
- Dependent types for program termination verification
- Derivation lengths classification of Gödel's T extending Howard's assignment
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Guarded recursive datatype constructors
- Harnessing first order termination provers using higher order dependency pairs
- Higher order dependency pairs for algebraic functional systems
- Higher-order rewrite systems and their confluence
- How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- scientific article; zbMATH DE number 1692901 (Why is no real title available?)
- scientific article; zbMATH DE number 996558 (Why is no real title available?)
- scientific article; zbMATH DE number 4045709 (Why is no real title available?)
- scientific article; zbMATH DE number 4072437 (Why is no real title available?)
- scientific article; zbMATH DE number 1189292 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 3497890 (Why is no real title available?)
- scientific article; zbMATH DE number 3501006 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 4124996 (Why is no real title available?)
- scientific article; zbMATH DE number 1223720 (Why is no real title available?)
- scientific article; zbMATH DE number 1314876 (Why is no real title available?)
- scientific article; zbMATH DE number 545277 (Why is no real title available?)
- scientific article; zbMATH DE number 627763 (Why is no real title available?)
- scientific article; zbMATH DE number 683368 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1956528 (Why is no real title available?)
- scientific article; zbMATH DE number 1543354 (Why is no real title available?)
- scientific article; zbMATH DE number 1889386 (Why is no real title available?)
- scientific article; zbMATH DE number 794240 (Why is no real title available?)
- scientific article; zbMATH DE number 3210031 (Why is no real title available?)
- scientific article; zbMATH DE number 5057388 (Why is no real title available?)
- scientific article; zbMATH DE number 3328152 (Why is no real title available?)
- scientific article; zbMATH DE number 3331288 (Why is no real title available?)
- scientific article; zbMATH DE number 3333259 (Why is no real title available?)
- scientific article; zbMATH DE number 3336816 (Why is no real title available?)
- scientific article; zbMATH DE number 3379785 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- scientific article; zbMATH DE number 3053259 (Why is no real title available?)
- Improved matrix interpretation
- Indexed types
- Inductive types and type constraints in the second-order lambda calculus
- Inductive-data-type systems
- Intensional interpretations of functionals of finite type I
- LCF considered as a programming language
- Matrix interpretations for proving termination of term rewriting
- Mechanically proving termination using polynomial interpretations
- Mechanizing and improving dependency pairs
- Minimax algebra
- Modular termination proofs for rewriting using dependency pairs
- Modularity of strong normalization in the algebraic-λ-cube
- New Computational Paradigms
- On strong normalization of the calculus of constructions with type-based termination
- On the Relation between Sized-Types Based Termination and Semantic Labelling
- On the Stability by Union of Reducibility Candidates
- On the Values of Reducibility Candidates
- On theories with a combinatorial definition of 'equivalence'
- Orderings for term-rewriting systems
- Polymorphic higher-order recursive path orderings
- Polynomials over the reals in proofs of termination : from theory to practice
- Predictive Labeling
- Proofs by induction in equational theories with constructors
- Proving termination of normalization functions for conditional expressions
- Proving termination with multiset orderings
- Quasi-interpretations. A way to control resources
- Rewriting Techniques and Applications
- Root-Labeling
- SAT Solving for Termination Analysis with Polynomial Interpretations
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Search Techniques for Rational Polynomial Orders
- Semi-continuous Sized Types and Termination
- Signature extensions preserve termination. An alternative proof via dependency pairs
- Simplifying subtyping constraints: a theory
- Termination by absence of infinite chains of dependency pairs
- Termination checking with types
- Termination of nested and mutually recursive algorithms
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Termination of rewriting systems by polynomial interpretations and its implementation
- Termination of term rewriting using dependency pairs
- Testing positiveness of polynomials
- The computability path ordering
- The consistency of arithmetics
- The Principal Type-Scheme of an Object in Combinatory Logic
- The size-change principle and dependency pairs for termination of term rewriting
- The size-change principle for program termination
- The size-change termination principle for constructor based languages
- Towards a domain theory for termination proofs
- Transforming termination by self-labelling
- Type inference with subtypes
- Type-based termination of recursive definitions
- Type-Based Termination with Sized Products
- Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
- Typed Lambda Calculi and Applications
- Types for Proofs and Programs
- Union of Reducibility Candidates for Orthogonal Constructor Rewriting
- Universality of quantum Turing machines with deterministic control
- ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
Cited in
(10)- Size of context in regenerative IL systems
- On the Relation between Sized-Types Based Termination and Semantic Labelling
- Dependency pairs termination in dependent type theory modulo rewriting
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- Semi-continuous Sized Types and Termination
- Rewriting Techniques and Applications
- Rewriting Techniques and Applications
- scientific article; zbMATH DE number 7756108 (Why is no real title available?)
- Factorize factorization
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
This page was built for publication: Size-based termination of higher-order rewriting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4577817)
