Higher-order term rewriting
Cynthia Kop (Radboud University)
Some material will be available here.
In this lecture, I will discuss higher-order term rewriting, a way to combine the benefits of term rewriting and the lambda calculus. I will present some of the considerations (such as typing, polymorphism and matching), some applications, and show how the basic analysis techniques for confluence and termination extend from first-order to higher-order term rewriting systems.
Outline of the lecture
The lecture will focus on (untyped) CRSs, but explain why typing is useful later. I will discuss a simple version of the higher-order recursive path order for termination, and orthogonality for confluence. Each of the different topics will be interleaved with exercises.
Exercises or experiments
- Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
- J.W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121(1-2):279–308, 1993.
- J. Jouannaud and A. Rubio. The higher-order recursive path ordering. In Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS ’99), IEEE, pages 402–411, 1999.
- (perhaps) J.C. van de Pol. Termination of Higher-order Rewrite Systems. PhD thesis, University of Utrecht, 1996.