Algebraic properties of if-then-else and commutative three-valued tests.

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. [ABSTRACT FROM AUTHOR]