An independent axiomatisation for free short-circuit logic

TL;DR

This paper introduces a simple semantics and an independent axiomatisation for free short-circuit logic, which models left-to-right evaluation without memorising atomic evaluations, and discusses related evaluation strategies and effects.

Contribution

It provides the first independent axiomatisation for free short-circuit logic and explores its semantics and evaluation strategies.

Findings

Established a simple semantics for free SCL

Developed an independent axiomatisation for free SCL

Discussed evaluation strategies and side effects

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. Free short-circuit logic is the equational logic in which compound statements are evaluated from left to right, while atomic evaluations are not memorised throughout the evaluation, i.e., evaluations of distinct occurrences of an atom in a compound statement may yield different truth values. We provide a simple semantics for free SCL and an independent axiomatisation. Finally, we discuss evaluation strategies, some other SCLs, and side effects.