Polynomial interpretations for higher-order rewriting

DOI10.4230/LIPICS.RTA.2012.176MaRDI QIDQ5111904zbMATH OpenOpenAlexFDO

Authors Carsten Fuhs, Cynthia Kop

Publication date 27 May 2020

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

zbMATH Keywords

automationterminationpolynomial interpretationshigher-order rewritingweakly monotonic algebras

Mathematics Subject Classification ID

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

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.

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

Cited in

(7)

• scientific article; zbMATH DE number 7559278 (Why is no real title available?)
• Higher-order interpretations and program complexity
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• scientific article; zbMATH DE number 7379291 (Why is no real title available?)
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Simplifying algebraic functional systems
• Theory of higher order interpretations and application to basic feasible functions

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)