University of Cambridge > Talks.cam > SANDWICH Seminar (Computer Laboratory) > Confluence of Term Rewriting Systems with Variable Binding

Confluence of Term Rewriting Systems with Variable Binding

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity