LIPIcs.RTA.2012.176.pdf
- Filesize: 0.6 MB
- 17 pages
Document
Polynomial Interpretations for Higher-Order Rewriting
Authors
-
Part of:
Volume:
23rd International Conference on Rewriting Techniques and Applications (RTA'12) (RTA 2012)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2012-05-29
Cite AsGet 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
https://doi.org/10.4230/LIPIcs.RTA.2012.176
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.
Keywords
- higher-order rewriting
- termination
- polynomial interpretations
- weakly monotonic algebras
- automation
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads