Satisfiability of Short Circuit Logic

TL;DR

This paper explores the satisfiability problem in Short Circuit Logic, providing formal definitions, proving equivalences, and implementing algorithms to improve understanding and efficiency in programming language semantics.

Contribution

It introduces formal models for satisfiability in Short Circuit Logic, proving their equivalence and offering an implementation, advancing theoretical understanding of short-circuit evaluation.

Findings

Satisfiability and path-satisfiability are equivalent.

Three types of valuation paths correspond to five valuation algebras.

Side-effects influence truth values but do not affect satisfiability analysis.

Abstract

The logical connectives typically found in programming languages are similar to their mathematical counterparts, yet different due to their short-circuit behaviour -- when evaluating them, the second argument is only evaluated if the first argument is not sufficient to determine the result. Combined with the possibility of side-effects, this creates a different type of logic called Short Circuit Logic. A greater theoretical understanding of this logic can lead to more efficient programming and faster program execution. In this thesis, 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 can be discerned, there are only three corresponding 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.