Confluence of Term Rewriting Systems with Variable Binding

Add to your list(s) Download to your calendar using vCal

• Gregor Feierabend (University of Cambridge)
• Monday 02 June 2025, 14:45-15:45
• FW26, Computer Laboratory.

If you have a question about this talk, please contact Dr Meven Lennon-Bertrand.

In this talk, we will consider a generalised confluence theorem in the spirit of Aczel [1] in the context of the model of second-order abstract syntax in the category of presheaves over the category of finite cardinals [2, 3]. We will recall from Fiore et al [2, 3] that a signature with variable-binding operators induces a strong term monad, T, on this category. A rewrite rule, ρ, can then be defined to be a pair of terms in T(M)(0) for some presheaf of meta-variables, M. Every ρ inductively defines a reduction relation ⤳ ⊆ T(0) × T(0). Closely following Aczel’s approach, we will establish a coherence property for ρ and show that it yields the confluence of the reduction relation ⤳. As an application, we will examine the confluence of β-reduction in the λ-calculus.

(Joint work with Marcelo Fiore)

[1] P. Aczel, A General Church–Rosser Theorem. Unpublished note, 1978. [2] M. Fiore, Second-Order and Dependently-Sorted Abstract Syntax, In Proceedings of the 23rd Annual ACM /IEEE Symposium on Logic in Computer Science (LICS 2008), pages 57–68. IEEE Computer Society, 2008. [3] M. Fiore, G. Plotkin, and D. Turi, Abstract Syntax and Variable Binding, In Proceedings of the 14th Annual ACM /IEEE Symposium on Logic in Computer Science (LICS 1999), pages 193–202. IEEE Computer Society, 1999.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FW26, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.