Predicate Fibration and Hoare Logic

Program logic is fibred logic. Predicates over a type form a poset, execution reindexes predicates by pullback, and a Hoare triple is the single inequality relating a precondition to the pulled-back postcondition. Seeing this as an instance of an indexed category places the logic of programs inside the same machinery as fibrations.

The predicate fibration

Let . The predicate indexed category is , sending a set to ordered pointwise, , and sending to the reindexing . Each fibre is the powerset lattice of ; reindexing is pullback of predicates along a map.

Definition of the Hoare triple

The Hoare triple for an execution , a precondition on and a postcondition on is defined by . The precondition sits below the pullback of the postcondition along , so every state satisfying is carried by into one satisfying .

Remark on the hyperdoctrine instance

is a hyperdoctrine / indexed category, a functor into the ordered structures . Applying the total-category construction glues the fibres into one category whose objects are and whose morphisms are the valid triples, so Hoare logic becomes reasoning in the total category of the fibration.

References

• Bart Jacobs, “Categorical Logic and Type Theory”, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1999)
• F. William Lawvere, “Adjointness in Foundations”, Dialectica 23 (1969), pp. 281-296