Sound and Complete Equational Reasoning over Comodels
Dirk Pattinson, Lutz Schröder · Electronic Notes in Theoretical Computer Science · 2015
Comodels of Lawvere theories, i.e. models in Set op , model state spaces with algebraic access operations. Standard equational reasoning is known to be sound but incomplete for comodels. We give two sound and complete calculi for equational reasoning over comodels: an inductive calculus for equality-on-the-nose, and a coinductive/inductive calculus for equality modulo bisimulation which captures bisimulations syntactically through non-wellfounded proofs.