Higher-order rewrite systems and their confluence

DOI10.1016/S0304-3975(97)00143-6zbMath0895.68078OpenAlexW1975808446MaRDI QIDQ1127334

Tobias Nipkow, Richard Mayr

Publication date: 13 August 1998

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

Full work available at URL: https://doi.org/10.1016/s0304-3975(97)00143-6

zbMATH Keywords

higher-order rewrite systems

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (37)

Soundness and completeness proofs by coinductive methods ⋮ Nominal rewriting ⋮ Confluence Competition 2015 ⋮ Higher-order superposition for dependent types ⋮ Contextual Natural Deduction ⋮ Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ Size-based termination of higher-order rewriting ⋮ Normal Higher-Order Termination ⋮ Higher-order narrowing with convergent systems ⋮ Unifying sets and programs via dependent types ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ How to prove decidability of equational theories with second-order computation analyser SOL ⋮ Formally verified animation for RoboChart using interaction trees ⋮ Superposition for higher-order logic ⋮ Decreasing diagrams and relative termination ⋮ Pure pattern calculus à la de Bruijn ⋮ Capture-avoiding substitution as a nominal algebra ⋮ Checking overlaps of nominal rewriting rules ⋮ The variable containment problem ⋮ Development closed critical pairs ⋮ On proving confluence modulo equivalence for Constraint Handling Rules ⋮ Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules ⋮ Infinitary combinatory reduction systems ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions ⋮ Unnamed Item ⋮ Inductive-data-type systems ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ Shallow confluence of conditional term rewriting systems ⋮ Cut Elimination, Substitution and Normalisation ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Nominal Confluence Tool ⋮ Confluence by critical pair analysis revisited ⋮ ON THE TERMINATION OF RUSSELL’S DESCRIPTION ELIMINATION ALGORITHM ⋮ Higher-order substitutions ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems ⋮ Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Uses Software

• Isabelle
• ML
• HOL
• Automath

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Computing in systems described by equations
• The undecidability of the second-order unification problem
• Confluence of the lambda calculus with left-linear algebraic rewriting
• Combinatory reduction systems: Introduction and survey
• Isabelle. A generic theorem prover
• Combinators, \(\lambda\)-terms and proof theory
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• The variable containment problem
• Linear unification of higher-order patterns
• Adding algebraic rewriting to the untyped lambda calculus (extended abstract)
• Confluence and superdevelopments
• A termination ordering for higher order rewrite systems
• Towards a domain theory for termination proofs
• The Clausal Theory of Types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Higher-order rewrite systems and their confluence