Action logic paper

• To: types, logic
• Subject: Action logic paper
• From: Vaughan Pratt <pratt@cs.stanford.edu>
• Date: Mon, 22 Oct 90 09:55:30 EDT
• Sender: meyer@theory.lcs.mit.edu

Date: Sat, 20 Oct 90 19:12:10 PDT
To: types@theory.lcs.mit.edu

Type theorists may find the following of some interest in view of its
essential use of residuation.

I've just finished "Action Logic and Pure Induction" for the
proceedings of an AI conference (JELIA), due several days ago.  I've
posted the relevant files, jelia.tex, pratt.bib, jelia.dvi, on
boole.stanford.edu, accessible via anonymous ftp in directory pub.
Feedback in the next couple of days or so from anyone with the time and
interest would be extremely welcome.  As an incentive to at least peek
at the paper here's the abstract.  Let me know of any difficulties in
retrieving it.

Thanks in anticipation.
-v


			Action Logic and Pure Induction
				 V.R. Pratt

In Floyd-Hoare logic programs are dynamic while assertions are static
(hold at states).  In action logic, an equational theory Theta_act, the
two notions become one, with programs viewed as on-the-fly assertions
whose truth is evaluated along intervals instead of at states.  This
simplifies the language of program correctness to that of regular
expressions plus retrospective implication a -> b (HAD a THEN b) and
prognostic implication b <- a (b IF-EVER a).  Whereas the equational
theory Theta_reg of regular expressions is not finitely axiomatizable,
that of Theta_act is, yet Theta_act conservatively extends Theta_reg.
The key equation is that of pure induction, (a -> a)* = (a -> a).

• Prev: Excluded middle w/o definite descriptions in theory of constructions
• Next: Op. Sem. query
• Index(es):
  • Main
  • Thread