A Pebbling Comonad for Finite Rank and Variable Logic, and an Application to the Equirank-variable Homomorphism Preservation Theorem
Thomas Paine · Electronic Notes in Theoretical Computer Science · 2020
In this paper we recast the proof of Rossman's equirank homomorphism preservation theorem using comonadic formulations of bounded quantifier rank and variable count (and dually tree width and tree-depth), and work towards generalisation of it that simultaneously preserves quantifier rank and variable count. Along the way, we give an exposition of the required comonads, showing how their properties arise.