Hopefully this is my last question for a while. Has there been work on a categorical model for "while programs" (or, equivalently, assembly language) and Floyd-Hoare logic? In the obvious model, objects are predicates on a store, and arrows are code sequences mapping stores to stores that satisfy the postcondition assuming the precondition. I'm interested to know: (1) What is the structure of this category? Does it have products, sums, etc? What program constructs do they correspond to? (2) What is the correct equality on arrows? I would think that we want the finest equality that yields nice structure. Then we can collapse afterward to obtain coarser categories. David
Has there been work on a categorical model for "while programs" (or, equivalently, assembly language) and Floyd-Hoare logic?
The first such was developed by Arbib and Manes in the mid-70's. Manes went on to develop the theory in great detail, writing a near-book-length article on it a decade later, not sure where it appeared. (1) What is the structure of this category? As I recall it was an additive (semiadditive?) category, with sequential composition represent by composition, and choice by sum within homsets. The objects were predicates, the arrows were programs (aka predicate transformers). Does it have products, sums, etc? What program constructs do they correspond to? Not sure about products, but it certainly had sums. which was how if-then-else was handled. (2) What is the correct equality on arrows? My recollection is that it was fully abstract: the correct equality is equality. Vaughan Pratt
participants (2)
-
David Espinosa -
Vaughan Pratt