Algebraic properties of If-Then-Else and commutative three-valued tests

Abstract

This paper establishes a finite axiomatization of possibly non-halting computer programs and tests, with the if-then-else operation. The model is a two-sorted algebra, with one sort being the programs and the other being the tests. The main operation on programs is composition, and 1 and 0 represent the programs skip and loop (i.e. never halts) respectively. Programs are modeled as partial functions on some state space X, with tests modeled as partial predicates on X. The operations on the tests are the usual logical connectives T and F. In addition, there is the hybrid operation of if-then-else, and the test-valued operation H on programs which is true when a program halts, and undefined otherwise. The halting operation H implies that operations of domain D and domain join may also be expressed. When tests are assumed to be possibly non-halting, the evaluation strategy of the logical connectives affects the result. Here we model parallel evaluation, as opposed to the common sequential (or short-circuit) evaluation strategy. For example, we view α β as false if either α or β is false, even if the other does not halt.