Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant

TL;DR

This paper explores different logical systems modeling short-circuit evaluation in programming, analyzing their axioms, semantics, and the effects of side effects and commutativity.

Contribution

It introduces and relates several short-circuit logics, providing axiomatizations and semantics for each, including non-commutative and commutative variants.

Findings

FSCL characterizes atomic side effects in evaluation.

MSCL models sequential evaluation with memorized results.

SSCL incorporates commutative sequential connectives.

Abstract

Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. Short-circuit evaluation is widely used in programming, with sequential conjunction and disjunction as primitive connectives. We study the question which logical laws axiomatize short-circuit evaluation under the following assumptions: compound statements are evaluated from left to right, each atom (propositional variable) evaluates to either true or false, and atomic evaluations can cause a side effect. The answer to this question depends on the kind of atomic side effects that can occur and leads to different "short-circuit logics". The basic case is FSCL (free short-circuit logic), which characterizes the setting in which each atomic evaluation can cause a side effect. We recall some main results and then relate FSCL to MSCL (memorizing short-circuit logic), where in the evaluation of a compound statement, the first evaluation result of each atom is memorized. MSCL can be seen as a sequential variant of propositional logic: atomic evaluations cannot cause a side effect and the sequential connectives are not commutative. Then we relate MSCL to SSCL (static short-circuit logic), the variant of propositional logic that prescribes short-circuit evaluation with commutative sequential connectives. We present evaluation trees as an intuitive semantics for short-circuit evaluation, and simple equational axiomatizations for the short-circuit logics mentioned that use negation and the sequential connectives only.