**Research:**(since 2009)

*Proposition algebra*and*Short-circuit logic*, with Jan Bergstra**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 |> 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.