Non-commutative propositional logic with short-circuit evaluation. Issue 3 (2nd October 2021)

• Record Type: Journal Article
• Authors: Bergstra, Jan A.; Ponse, Alban; Staudt, Daan J. C.
• Is Part Of: Journal of applied non-classical logics. Volume 31:Issue 3/4(2021)
• Page Start: 234
• Page End: 278
• Publication Date: 2021-10-02
• Subjects: Non-commutative conjunction -- conditional composition -- sequential connectives -- short-circuit evaluation -- side effect; Nonclassical mathematical logic -- Periodicals; Wiskundige logica; Logic; Periodicals; 511.3105
• DOI: 10.1080/11663081.2021.2010954
• Languages: English
• ISSNs: 1166-3081

Abstract

Abstract : Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first is insufficient to determine the value of the expression. Compound statements are evaluated from left to right. Short-circuit evaluation is widely used in programming, with negation and sequential conjunction and disjunction as primitives. We study the question of which laws axiomatise short-circuit evaluation. In MSCL (memorising short-circuit logic), atoms (propositional variables) evaluate to true or false, and in the evaluation of a compound statement, the first evaluation result of each atom is memorised. Hence, MSCL is 'Non-commutative propositional logic with short-circuit evaluation' and atomic evaluations cannot cause a side effect. Next, we consider the case that atoms can also evaluate to the truth value 'undefined'. For two- and three-valued MSCL, we present evaluation trees as an intuitive semantics and provide complete independent equational axiomatisations.