Fuhs, C;
Kop, C;
(2012)
Polynomial Interpretations for Higher-Order Rewriting.
In: Tiwari, A, (ed.)
Proceedings of the Conference on Rewriting Techniques and Applications (RTA'12).
(pp. 176 - 192).
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
![[thumbnail of RTA12-hopolo.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
RTA12-hopolo.pdf Download (715kB) |
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 λ-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.
| Type: | Proceedings paper |
|---|---|
| Title: | Polynomial Interpretations for Higher-Order Rewriting |
| Event: | Rewriting Techniques and Applications (RTA'12) |
| ISBN-13: | 978-3-939897-38-5 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.RTA.2012.176 |
| Publisher version: | http://dx.doi.org/10.4230/LIPIcs.RTA.2012.176 |
| Additional information: | This work is licensed under the terms of the Creative Commons Attribution-NonCommercial-NoDerivativeWorks 3.0 license. You are free to share (copy, distribute and transmit the work), but you must attribute the author, you may not use this work for commercial purposes and you may not alter, transform, or build upon this work and distribute any derivative works you create under a similar license. |
| Keywords: | higher-order rewriting, termination, polynomial interpretations, weakly monotonic algebras, automation |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1410030 |
Archive Staff Only
 |
View Item |
