Australian Category Seminar

Plotkin and Pitts: substitution and binders

John Powerยท26 March 2025

At the turn of the millennium, Fiore, Plotkin and Turi, aka Plotto et al, and Gabbay and Pitts, aka Andy and Jamie, claimed to give category theoretic models of binding. In fact, they modelled different phenomena, with Plotto et al really modelling substitution, which Andy and Jamie did not model. I wrote a string of papers, largely with Miki Tanaka, analysing and axiomatising Plotto et al's work, putting it into a conceptual mathematical framework. I remarked that, in abstract mathematical terms, one could unify the two bodies of work, but I have never attempted a conceptual reconciliation. At the end of the last seminar I gave on Plotto et al's work, Ross asked about Andy's work and the relationship. So I want to address Ross' question, mainly by trying to explain the motivation of, and background to, Andy's approach. I think the formal mathematical relationship is already known to most people in the group, in particular to Ross. So this is an informal seminar, explaining background and motivation rather than new mathematics.

Back