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 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).

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] 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