Cynthia Kop

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

Absolutely!

Bibliographical references

1. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
2. 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.
3. 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.
4. (perhaps) J.C. van de Pol. Termination of Higher-order Rewrite Systems. PhD thesis, University of Utrecht, 1996.