Termination of rewrite relations on -terms based on Girard's notion of reducibility

DOI10.1016/J.TCS.2015.07.045zbMATH Open1332.68103arXiv1509.00649OpenAlexW1791042548MaRDI QIDQ896904FDOQ896904

Authors: Frédéric Blanqui 

Publication date: 15 December 2015

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of $$-reduction in the polymorphic $lambda$-calculus, to prove the termination of various kinds of rewrite relations on $lambda$-terms, including rewriting modulo some equational theory and rewriting with matching modulo $$$eta$, by using the notion of computability closure. This provides a powerful termination criterion for various higher-order rewriting frameworks, including Klop's Combinatory Reductions Systems with simple types and Nipkow's Higher-order Rewrite Systems.

Full work available at URL: https://arxiv.org/abs/1509.00649

Recommendations

• Termination of combined (rewrite and λ-calculus) systems
• Size-based termination of higher-order rewriting
• Normal higher-order termination
• Computability Closure: Ten Years Later
• Rewriting Techniques and Applications

zbMATH Keywords

types\(\lambda\)-calculusrewritingterminationGirard's reducibilitymatching modulo \(\beta\eta\)[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=patterns+%EF%BF%BD%EF%BF%BD+la+Miller&go=Go patterns �� la Miller]rewriting modulo

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Cites Work

• The Matita Interactive Theorem Prover
• Constructive versions of Tarski's fixed point theorems
• A lattice-theoretical fixpoint theorem and its applications
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The typed lambda-calculus is not elementary recursive
• Combinatory reduction systems: Introduction and survey
• Termination of term rewriting using dependency pairs
• Title not available (Why is that?)
• Proving termination with multiset orderings
• Polynomial Interpretations for Higher-Order Rewriting
• Orderings for term-rewriting systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• On Computable Numbers, with an Application to the Entscheidungsproblem
• On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
• Complete Sets of Reductions for Some Equational Theories
• Title not available (Why is that?)
• Title not available (Why is that?)
• The calculus of constructions
• Title not available (Why is that?)
• Polymorphic higher-order recursive path orderings
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Intensional interpretations of functionals of finite type I
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Title not available (Why is that?)
• Higher-order rewrite systems and their confluence
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proofs of strong normalisation for second order classical natural deduction
• Title not available (Why is that?)
• Counterexamples to termination for the direct sum of term rewriting systems
• Title not available (Why is that?)
• Constructing recursion operators in intuitionistic type theory
• First-class patterns
• Parallel reductions in \(\lambda\)-calculus
• Adding algebraic rewriting to the untyped lambda calculus
• Decidability of higher-order matching
• Title not available (Why is that?)
• Completion of a Set of Rules Modulo a Set of Equations
• Title not available (Why is that?)
• Explicit substitutions
• Title not available (Why is that?)
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Title not available (Why is that?)
• Type-based termination of recursive definitions
• The Theory of Calculi with Explicit Substitutions Revisited
• Generalized sufficient conditions for modular termination of rewriting
• Title not available (Why is that?)
• Polymorphic rewriting conserves algebraic strong normalization
• Title not available (Why is that?)
• Modularity of strong normalization in the algebraic-λ-cube
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Functionals defined by recursion
• Inductive-data-type systems
• Lambda calculus with patterns
• Higher-Order Orderings for Normal Rewriting
• Abstract data type systems
• The rewriting calculus. II
• Title not available (Why is that?)
• Title not available (Why is that?)
• An initial algebra approach to term rewriting systems with variable binders
• Semantic types
• Termination checking with types
• Proofs of the normalization and Church-Rosser theorems for the typed \(\lambda\)-calculus
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Dependent types for program termination verification
• The rewriting calculus. I
• Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associative-commutative theories
• The computability path ordering
• Relating Higher-order and First-order Rewriting
• The Computability Path Ordering: The End of a Quest
• Computability Closure: Ten Years Later
• On the Relation between Sized-Types Based Termination and Semantic Labelling
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Definitions by rewriting in the Calculus of Constructions
• Title not available (Why is that?)
• Higher Order   Matching is Undecidable
• Linear unification of higher-order patterns
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
• A Characterization of Medial as Rewriting Rule
• On the Stability by Union of Reducibility Candidates
• Termination of combined (rewrite and λ-calculus) systems
• Rewriting Techniques and Applications
• Rewriting Techniques and Applications

Cited In (7)

• Title not available (Why is that?)
• Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
• Computability Closure: Ten Years Later
• Size-based termination of higher-order rewriting
• Theory and practice of second-order rewriting: foundation, evolution, and SOL
• How to prove decidability of equational theories with second-order computation analyser SOL
• Title not available (Why is that?)

Uses Software

• Coq
• Matita
• Automath
• Agda

This page was built for publication: Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q896904)