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 |> yNote 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 = Fto 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)) || yAlso 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.
[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.