Categorical model for Floyd-Hoare logic?

Categorical model for Floyd-Hoare logic?

[Paul Taylor]

I see Roy Crole has already answered this question on my behalf.
The paper to which he refers is called "An Exact Interpretation of While"
and is "while-1993.dvi.gz" on my page at Hypatia
	http://hypatia.dcs.qmw.ac.uk/author/TaylorP

Manes' appraoach, as I recall, looks a bit like matrix algebra,
with finite addition replaced by infinite union.  From a programming
point of view this seems to me like replacing a WHILE program (which
doesn't know a priori how many times it is going to go round) with
an infinite SWITCH/CASE statement indexed by the number of iterations.

My motication (in 1987 this was) was that it only takes finitely many
characters to write the program, so its semantics should be given
in a finitary form.  The bit of the (categorical) diagram which does
the work is a coequaliser, and Barry Jay observed independently that
this says in categorical language that the WHILE program is the
"universal loop invariant".

The coequaliser is not the whole story.  It does not say when to exit
the loop: some modifications to the diagram using pullbacks are needed.
Nor will coequalisers in any old category do (cd the need for at least
distributive and preferably extensive categories for if-then-else).
I spent a long time trying to formulate the need for "stable" coequalisers
correctly, but this never worked.  It was necessary to fall back on
stability of the formation of transitive or equivalence closures.

There is a completely rewritten account of my work on WHILE programs
in Section 6.4 of my book (not yet, I'm afraid, finished).

The category theory does not match up quite as nicely as one would like
("full abstraction") for WHILE or even IF-THEN-ELSE.  (The interpretation
is sound, but what I know about it falls short of the equivalence
which exists, for example, between lambda calculus and CCCs).

My treatment of Floyd-Hoare logic is done in the greatest detail for
what I call the direct declarative language (with assignments but no
conditionals or loops).  This is integrated with the categorical 
account of algebraic or finite-product theories.  I now think I can
motivate the definition of category and product EASIER on the basis
of programming than from traditional mathematics.

Floyd-Hoare logic & algebraic theories are in Chapter IV, conditionals
in Section 5.5.

Paul

PS Yes, I know I've got to get this book finished. There are just not
enough hours in the day!