Reference. Action logic and pure induction

Vaughan Pratt · Logics in AI · 1991 · kleene-algebra · DOI
In Floyd-Hoare logic, programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a→b (had a then b) and postimplication b←a (b if-ever a). Unlike REG, ACT is finitely based, makes a∗ reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a→a)∗ = a→a.

Cite
Cite as @prattActionLogicPure1991 (helia, typst) · \cite{prattActionLogicPure1991} (LaTeX)
BibTeX
bibtex · 18 lines
@incollection{prattActionLogicPure1991,
 title = {Action logic and pure induction},
 author = {Pratt, Vaughan},
 year = {1991},
 isbn = {978-3-540-53686-4 978-3-540-46982-7},
 doi = {10.1007/BFb0018436},
 url = {http://link.springer.com/10.1007/BFb0018436},
 urldate = {2024-07-10},
 booktitle = {Logics in {AI}},
 editor = {Siekmann, J. and Goos, G. and Hartmanis, J. and Van Eijck, J.},
 volume = {478},
 pages = {97--120},
 publisher = {Springer Berlin Heidelberg},
 address = {Berlin, Heidelberg},
 note = {Series Title: Lecture Notes in Computer Science},
 language = {en},
 abstract = {In Floyd-Hoare logic, programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a→b (had a then b) and postimplication b←a (b if-ever a). Unlike REG, ACT is finitely based, makes a∗ reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a→a)∗ = a→a.}
}
hayagriva YAML (typst)
yaml · 26 lines
prattActionLogicPure1991:
  type: anthos
  title: Action logic and pure induction
  author: Pratt, Vaughan
  date: 1991
  editor:
  - Siekmann, J.
  - Goos, G.
  - Hartmanis, J.
  - Van Eijck, J.
  page-range: 97-120
  url:
    value: http://link.springer.com/10.1007/BFb0018436
    date: 2024-07-10
  serial-number:
    doi: 10.1007/BFb0018436
    isbn: 978-3-540-53686-4 978-3-540-46982-7
  note: 'Series Title: Lecture Notes in Computer Science'
  abstract: In Floyd-Hoare logic, programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a→b (had a then b) and postimplication b←a (b if-ever a). Unlike REG, ACT is finitely based, makes a∗ reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a→a)∗ = a→a.
  parent:
    type: anthology
    title: Logics in {AI}
    publisher:
      name: Springer Berlin Heidelberg
      location: Berlin, Heidelberg
    volume: 478
Download: prattActionLogicPure1991.bib · prattActionLogicPure1991.yml
Cited by (4)

Regular expression containment: Coinductive axiomatization and computational interpretation henglein_regular_2011POPL · 2011
We present a new sound and complete axiomatization of regular expression containment. It consists of the conventional axiomatization of concatenation, alternation, empty set and (the singleton set containing) the empty string as an idempotent semiring, the fixed- point rule E* = 1 + E × E* for Kleene-star, and a general coinduction rule as the only additional rule. Our axiomatization gives rise to a natural computational interpretation of regular expressions as simple types that represent parse trees, and of containment proofs as coercions. This gives the axiom- atization a Curry-Howard-style constructive interpretation: Containment proofs do not only certify a language-theoretic contain- ment, but, under our computational interpretation, constructively transform a membership proof of a string in one regular expression into a membership proof of the same string in another regular expression. We show how to encode regular expression equivalence proofs in Salomaa’s, Kozen’s and Grabmayer’s axiomatizations into our containment system, which equips their axiomatizations with a computational interpretation and implies completeness of our axiomatization. To ensure its soundness, we require that the computational interpretation of the coinduction rule be a hereditarily total function. Hereditary totality can be considered the mother of syn- tactic side conditions: it “explains” their soundness, yet cannot be used as a conventional side condition in its own right since it turns out to be undecidable. We discuss application of regular expressions as types to bit coding of strings and hint at other applications to the wide-spread use of regular expressions for substring matching, where classical automata-theoretic techniques are a priori inapplicable. Neither regular expressions as types nor subtyping interpreted coercively are novel per se. Somewhat surprisingly, this seems to be the first investigation of a general proof-theoretic framework for the latter in the context of the former, however.
PDF · DOI · pldb

Type Logics in Grammar buszkowskiTypeLogicsGrammar2003Trends in Logic · 2003
DOI

Kleene algebra with tests kozen1997kleeneTOPLAS · 1997
We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.
PDF · DOI · pldb

Towards Kleene Algebra with recursion leis_towards_1992CSL · 1992
We extend Kozen’s theory KA of Kleene Algebra to axiomatize parts of the equational theory of context-free languages, using a least fixed-point operator μ instead of Kleene’s iteration operator*.
DOI
Cites 31 works (2 here)
With notes (2)

Linear logic girard_linear_1987TCS · 1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI

Categories for the Working Mathematician maclane_19711971
Web
External (29)
prattActionLogicPure1991 reference entries/refs/prattActionLogicPure1991/prattActionLogicPure1991.hel