2026-07-20T10:41:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3492 2024-03-06T10:34:17Z ddc:004 open_access

Polynomial Interpretations for Higher-Order Rewriting Fuhs, Carsten Kop, Cynthia higher-order rewriting termination polynomial interpretations weakly monotonic algebras automation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Carsten Fuhs and Cynthia Kop 2012 Is Part Of LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2012.176 urn:nbn:de:0030-drops-34924 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.176 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode