![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > SANDWICH Seminar (Computer Laboratory) > Confluence of Term Rewriting Systems with Variable Binding
Confluence of Term Rewriting Systems with Variable BindingAdd 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. This talk is included in these lists:Note that ex-directory lists are not shown. |
Other listsCellular Genetic Disease Seminar Martin Centre Research Seminar Series – 44th Annual Series of Lunchtime Lectures Quantum Matter SeminarOther talksTitle TBC Robust and replicable effects of ageing on resting state brain electrophysiology measured with MEG Morning Coffee MIP A scientists guide to the art of radiation therapy and Neurosurgery for the oncologist Title TBC |