Polynomial Interpretations for Higher-Order Rewriting

C. Fuhs, C.L.M. Kop

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review


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 λ-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. © Carsten Fuhs and Cynthia Kop.
Original languageEnglish
Title of host publicationProceedings of RTA '12
EditorsA. Tiwari
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISBN (Print)9783939897385
Publication statusPublished - 2012
EventRewriting Techniques and Applications - Dagstuhl, Germany
Duration: 1 Jan 20121 Jan 2012


ConferenceRewriting Techniques and Applications


Dive into the research topics of 'Polynomial Interpretations for Higher-Order Rewriting'. Together they form a unique fingerprint.

Cite this