Document Open Access Logo

Polynomial Interpretations for Higher-Order Rewriting

Authors Carsten Fuhs, Cynthia Kop

PDF

File

Thumbnail PDF
PDF
LIPIcs.RTA.2012.176.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • higher-order rewriting
  • termination
  • polynomial interpretations
  • weakly monotonic algebras
  • automation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Carsten Fuhs and Cynthia Kop. Polynomial Interpretations for Higher-Order Rewriting. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 176-192, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) https://doi.org/10.4230/LIPIcs.RTA.2012.176

Author Details

Carsten Fuhs
Cynthia Kop
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact