Abstract

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.