Polynomial interpretations for higher-order rewriting

DOI10.4230/LIPICS.RTA.2012.176zbMATH Open1437.68080arXiv1203.5754OpenAlexW2241047399MaRDI QIDQ5111904FDOQ5111904

Cynthia Kop, Carsten Fuhs

Publication date: 27 May 2020

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-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.

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

Recommendations

• Normal higher-order termination
• Polymorphic higher-order recursive path orderings
• A termination ordering for higher order rewrite systems
• Termination of rewriting systems by polynomial interpretations and its implementation
• Higher-Order Orderings for Normal Rewriting

zbMATH Keywords

automationterminationpolynomial interpretationshigher-order rewritingweakly monotonic algebras

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Functional programming and lambda calculus (68N18)

Cited In (5)

• Title not available (Why is that?)
• Higher-order interpretations and program complexity
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

This page was built for publication: Polynomial interpretations for higher-order rewriting

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