A recursive path ordering for higher-order terms in η-long β-normal form

DOI10.1007/3-540-61464-8_46MaRDI QIDQ5055855zbMATH OpenOpenAlexFDO

Authors Jean-Pierre Jouannaud, Albert Rubio

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61464-8_46

Mathematics Subject Classification ID

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

Recommendations

• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• A termination ordering for higher order rewrite systems
• Polymorphic higher-order recursive path orderings
• Higher-Order Orderings for Normal Rewriting
• Normal higher-order termination

Cites work

• scientific article; zbMATH DE number 2185672 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• A termination ordering for higher order rewrite systems
• Higher-order unification, polymorphism, and subsorts
• Orderings for term-rewriting systems
• Termination of combined (rewrite and λ-calculus) systems

Cited in

(9)

• The Computability Path Ordering: The End of a Quest
• Normal higher-order termination
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• The embedding path order for \(\lambda\)-free higher-order terms
• A termination ordering for higher order rewrite systems
• A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
• Higher-Order Orderings for Normal Rewriting
• A Lambda-Free Higher-Order Recursive Path Order
• Cutting a proof into bite-sized chunks: incrementally proving termination in higher-order term rewriting (invited talk)

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A recursive path ordering for higher-order terms in η-long β-normal form

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