From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/649 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: CATS Categorical model for Floyd-Hoare logic? Date: Sat, 14 Feb 1998 20:41:25 +0000 Message-ID: <199802142041.MAA21284@coraki.Stanford.EDU> References: <199802140140.RAA11783@blackhawk.kestrel.edu> NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241017095 26703 80.91.229.2 (29 Apr 2009 14:58:15 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 14:58:15 +0000 (UTC) To: categories@mta.ca Original-X-From: cat-dist Sun Feb 15 11:18:55 1998 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.8.8/8.8.8) id KAA30139 for categories-list; Sun, 15 Feb 1998 10:07:52 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f In-reply-to: Your message of "Fri, 13 Feb 1998 17:40:06 -0800." <199802140140.RAA11783@blackhawk.kestrel.edu> Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 28 Xref: news.gmane.org gmane.science.mathematics.categories:649 Archived-At: >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