Alban Ponse - Proposition algeba and SCL

Research: Proposition algebra and Short-circuit logic, with Jan Bergstra (since 2009) and Daan Staudt (since 2012)

Our paper Proposition Algebra, published as [1], is based on Hoare's ternary connective P <| Q |> R, the so-called "conditional" (in Latex: \triangleleft and \triangleright, respectively). Expressions evaluate to either true or false, just as in propositional logic (PL). In the expression P <| Q |> R, first Q is evaluated; upon result true evaluation continues with P, and upon false with R. Observe that evaluaton is here a deterministic, sequential process. With constants T for true and F for false, the common propositional connectives are definable:

    ¬ x = F <| x |> T
  x ∧ y = y <| x |> F
  x ∨ y = T <| x |> y

Note that this definition enforces left-sequential evaluation of the binary connectives, this type of evaluation is also called short-circuit evaluation: the second argument is only evaluated is the first argument does not suffice to determine the value of the expression.

Propositional logic (PL) is axiomatized by these five axioms:

  x <| T |> y = x
  x <| F |> y = y
  T <| x |> y = T <| y |> x
  x <| (y <| z |> u) |> v = (x <| y |> v) <| z |> (x <| u |> v)
  (x <| y |> z) <| y |> F = x <| y |> F

(see [2] for a proof). Note that the third axiom expresses x ∨ y = y ∨ x, and that the fourth axiom defines a distribution property of the conditional. The fifth axiom implies that a second occurrence of y yields the same evaluation result as the first occurrence does (this is typically not valid in a setting with side-effects). Note that in his original 1985-paper, Hoare used eleven axioms to characterize PL (including the fourth axiom).

A most basic and natural set of axioms for Hoare's conditional connective is this one:

  x <| T |> y = x
  x <| F |> y = y
  T <| x |> F = x
  x <| (y <| z |> u) |> v = (x <| y |> v) <| z |> (x <| u |> v)

These four axioms define Free valuation congruence and we call each model that satisfies these four axioms a Proposition algebra. More valuation congruences can be defined by adding axioms. For example, adding

  x <| y |> (z <| u |> (v <| y |> w)) = x <| y |> (z <| u |> w)

yields Memorizing valuation congruence, and adding

  F  <| x |> F = F

to these five axioms yields a set of six axioms that axiomatizes Static valuation congruence. As proved in [2], this set of axioms is equivalent to the above set of five axioms that axiomatizes PL.

In programming, left-sequential evaluation is usually prescribed by so-called logical operators such as && that prescribes short-circuit conjunction, and || prescribing short-circuit disjunction. A typical example:

  (b ~= 0) && (a/b > 18.5)

(this clearly shows that && is not intended to be commutative).

A short-circuit logic (SCL) is a logic that implies all identities valid in free valuation congruence that are expressed with T, F, ¬, && and || only. In this manner, each valuation congruence defines its associated SCL as the smallest set of such identities.

In [4], Daan Staudt introduced evaluation trees as a very simple semantics for Free SCL (comparable to truth tables for propositional logic) and provided a complete, equational axiomatization of Free SCL. Moreover, fully evaluated left-sequential connectives, notation & and |, respectively, can be defined with short-circuit connectives and the constants T and F in the following way:

  x & y = (x || (y && F)) && y
  x | y = (x && (y || T)) || y

Also in [4], a complete equational axiomatization is provided for the case in which only the connectivess & and | are available. Some typical axioms: ¬x & F = x & F and x & F = F & x (using some standard axioms, these two axioms can be compressed into the single axiom x & F = F & ¬x, where both sides yield F and take the side effect of x into account). In [5], evaluation trees for repetition-proof, contractive, memorizing, and static evaluation congruence (see [1]) are defined, thus providing a simple and elegant semantical framework for sequential evaluation for proposition algebra. In [6], an independent axiomatization for Free SCL is provided and side effects are discussed. In [7] satisfyablility in the context of short-circuit logic is studied, leading to some interesting results. Finally, in [8] we study propositional logic with short-circuit evaluation and distinguish a non-commutative variant.

Introductory slide deck about SCL (29 slides), presented 4 November 2013 in the Minor Programming at UvA.
Introductory slide deck about evaluation trees (18 slides), presented 9 September 2015 at the Festschrift Symposium in Honour of Prof. Ernst-Rüdiger Olderog at the Carl von Ossietzky University of Oldenburg.

References with brief characterization:

[1] J.A. Bergstra and A. Ponse. Proposition Algebra (pdf), ACM Transactions on Computational Logic, 12(3), Article 21 (36 pp), 2011.
>> This paper introduces proposition algebra. ( Link to ACM ToCL page.) A nice review by Miguel Palomino is available here (at MathSciNet).

[2] J.A. Bergstra, A. Ponse, and D.J.C. Staudt. Short-circuit Logic, arXiv:1010.3674 version 4 [cs.LO], March 12, 2013.
>> This paper introduces short-circuit logic and contains some elementary completeness results.

[3] J.A. Bergstra and A. Ponse. Proposition algebra and short-circuit logic (pdf). Published in F. Arbab and M. Sirjani (editors), Proceedings of the 4th International Conference on Fundamentals of Software Engineering (FSEN 2011), Tehran, LNCS 7141, pages 15-31, Springer-Verlag, 2012.
>> This paper contains a discussion about Hoare-McCarthy algebras (HMAs). An HMA provides another semantics for proposition algebra and short-circuit logic.

[4] D.J.C. Staudt. Completeness for Two Left-Sequential Logics. MSc thesis Logic, University of Amsterdam, May 2012. Available at arXiv:1206.1936v1 [cs.LO].
>> This work introduces Evaluation trees as a more simple semantics of Free SCL (FSCL) and Free fully evaluated left-sequential logic (FFEL). Normal forms for FSCL and FFEL are defined and used to prove completeness results.

[5] J.A. Bergstra and A. Ponse. Evaluation trees for proposition algebra, arXiv:1504.08321 version 3 [cs.LO], 28 Aug 2017.
>> In this paper, evaluation trees for most other valuation congruences introduced in [1] are defined by simple transformations on Staudt's evaluation trees [4].

[6] A. Ponse and D.J.C. Staudt. An independent axiomatisation for free short-circuit logic. Journal of Applied Non-Classical Logics, 28(1):35-71, 2018. Online version, DOI: https://doi.org/10.1080/11663081.2018.1448637. Also available at arXiv:1707.05718v3 [cs.LO], 30 July 2018 (v1: 17 July 2017).
>> An independent axiomatization for FSCL and side effects are discussed.

[7] Sander in 't Veld. Satisfiability of Short Circuit Logic, arXiv:1510.05162 [cs.LO], 17 Oct 2015.
>> Formula satisfiability in the context of Short Circuit Logic is discussed. A formal definition of evaluation based on valuation algebras is presented, alongside an alternative definition based on valuation paths. The accompanying satisfiability and "path-satisfiability" are then proven to be equivalent, and an implementation of path-satisfiability is given. Although five types of valuation algebras are discerned, these correspond to only three types of valuation paths. From this, conclusions are drawn about satisfiability and side-effects; the manner in which side-effects alter truth values is relevant when analysing satisfiability, but the side-effects themselves are not.

[8] Bergstra, J. A., Ponse, A., and Staudt, D. J. C., 2021. Non-commutative propositional logic with short-circuit evaluation. Journal of Applied Non-Classical Logics, 31(3-4), 234-278. PDF. https://doi.org/10.1080/11663081.2021.2010954.
>> This paper is about short-circuit logic without atomic side effects, in particular about a non-commutative variant of sequential propositional logic.