Monoids with tests and the algebra of possibly non-halting programs

• Presents algebraic systems modelling partial maps and deterministic programs.
• Systems can express composition, if-then-else, program comparison and others.
• The family of computable functions is a model in each case.
• Axioms are complete for equational reasoning in loop-free deterministic computation.
• Includes discussion of looping and natural open problems.

We study the algebraic theory of computable functions, which can be viewed as arising from possibly non-halting computer programs or algorithms, acting on some state space, equipped with operations of composition, if-then-else and while-do defined in terms of a Boolean algebra of conditions. It has previously been shown that there is no finite axiomatization of algebras of partial functions under these operations alone, and this holds even if one restricts attention to transformations (representing halting programs) rather than partial functions, and omits while-do from the signature. In the halting case, there is a natural “fix”, which is to allow composition of halting programs with conditions, and then the resulting algebras admit a finite axiomatization. In the current setting such compositions are not possible, but by extending the notion of if-then-else, we are able to give finite axiomatizations of the resulting algebras of (partial) functions, with while-do in the signature if the state space is assumed finite. The axiomatizations are extended to consider the partial predicate of equality. All algebras considered turn out to be enrichments of the notion of a (one-sided) restriction semigroup.