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 evaluation 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 connectives & and | are available. Some typical axioms: ¬x & F = x & F and x & F = F & x (using some standard axioms, these two 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 [10], this is generalized to other `Fully evaluated left-sequential logics' (FELs), including Memorizing FEL.

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], satisfiability 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, and in [9] another one that is based on two- and three-valued Conditional logic defined by Guzmánn and Squier (1990). In [8] and [9], the case that atoms can also evaluate to the truth value 'undefined' is also considered (including evaluation trees that take this third truth value into account).

References with brief characterization:

[1] Bergstra, J. A. and Ponse, A., 2011. Proposition algebra (pdf), ACM Transactions on Computational Logic, 12(3), Article 21 (36 pp). https://doi.org/10.1145/1929954.1929958.
>> This paper introduces proposition algebra. Review by Miguel Palomino (at MathSciNet).

[2] Bergstra, J. A., Ponse, A., and Staudt, D. J. C., 2013. 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] Bergstra, J. A. and Ponse, A., 2012. Proposition algebra and short-circuit logic (pdf). In F. Arbab and M. Sirjani (Eds.), Proceedings of the 4th International Conference on Fundamentals of Software Engineering (FSEN 2011), Tehran. LNCS 7141, pages 15-31, Springer-Verlag.
>> This paper contains a discussion about Hoare-McCarthy algebras (HMAs). An HMA provides another semantics for proposition algebra and short-circuit logic.

[4] Staudt, D. J. C., 2012. 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] Bergstra, J. A. and Ponse, A., 2017. 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] Ponse, A. and Staudt, D. J. C., 2018 An independent axiomatisation for free short-circuit logic (pdf). Journal of Applied Non-Classical Logics, 28(1):35-71. 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] Veld, S. in 't, 2015. Satisfiability of Short Circuit Logic. BSc Thesis in Mathematics and Computer Science, University of Amsterdam, October 2015. Available at arXiv:1510.05162 [cs.LO], 17 Oct 2015.
>> (Abstract:) 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 (pdf). Journal of Applied Non-Classical Logics, 31(3-4), 234-278. 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.

[9] Bergstra, J. A. and Ponse, A., 2023. Conditional logic as a short-circuit logic, arXiv:2304.14821 [cs.LO], version 2: 28 September 2023.
>> An SCL in between Memorizing SCL and Static SCL is introduced, based on two- and three-valued Conditional logic by Guzmánn and Squier (1990).

[10] Ponse, A. and Staudt, D. J. C., 2024. Fully evaluated left-sequential logics, arXiv.2403.14576 [cs.LO], 21 March 2024.
>> This paper introduces a family of fully evaluated, left-sequential logics (FELs), starting from Free FEL and its complete axiomatization as described in [4]. Moreover, for each FEL, except Static FEL, its three-valued variant is also considered. Submitted for publication.

Return to Research

  Last modified: June 3, 2024