Axiomatization of if-then-else over possibly non-halting programs and tests

TL;DR

This paper develops a formal axiomatization for the if-then-else construct in programming languages that may include non-halting programs and tests, using algebraic structures called $C$-sets and $C$-algebras.

Contribution

It introduces the concept of $C$-sets for abstract tests and provides a complete axiomatization when tests form an ada, including equality tests with agreeable $C$-sets.

Findings

Complete axiomatization for $C$-sets over non-halting programs.

Representation of $C$-sets via subdirect products.

Axiomatization of equality tests with agreeable $C$-sets.

Abstract

In order to study the axiomatization of the if-then-else construct over possibly non-halting programs and tests, this paper introduces the notion of $C$-sets by considering the tests from an abstract $C$-algebra. When the $C$-algebra is an ada, the axiomatization is shown to be complete by obtaining a subdirect representation of $C$-sets. Further, this paper considers the equality test with the if-then-else construct and gives a complete axiomatization through the notion of agreeable $C$-sets.