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

TL;DR

This paper develops finite algebraic axiomatisations for algebras of computable functions, including non-halting programs with control structures, extending restriction semigroups and considering equality predicates.

Contribution

It introduces extended algebraic frameworks with finite axioms for non-halting program models, including while-do and equality, overcoming previous non-axiomatisability results.

Findings

Finite axiomatisations achieved for algebras with while-do in finite state spaces.

Extended algebraic structures incorporate equality predicates.

Algebras are enrichments of restriction semigroups.

Abstract

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, {\em if-then-else} and {\em while-do} defined in terms of a Boolean algebra of conditions. It has previously been shown that there is no finite axiomatisation 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 {\em 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 axiomatisation. In the current setting such compositions are not possible, but by extending the notion of {\em if-then-else}, we are able to give finite axiomatisations of the resulting algebras of (partial) functions, with {\em while-do} in the signature if the state space is assumed finite. The axiomatisations 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.