Guard modules (Q1080645)

This paper presents an analysis of a version of the ''if-then-else'' operation acting together with ''or''. In more detail, consider the collection of functions \(Q=\{q|\) \(q: D\times E\to A\}\), where D and E are nonempty sets and A is an abelian monoid. For motivation, if f and g are functions (or relations) \(D\to E\), and \(\lambda\) is a subset of D, the author models the statement ''if \(d\in \lambda\) then f(d) else g(d)'' as a function \(if_{\lambda}: Q\times Q\to Q\), as follows. Let \(q(d,e)=1\) if \(f(d)=e\); similarly let \(r(d,e)=1\) if \(g(d)=e\). Now let \(A=the\) two element Boolean algebra. Then \(if_{\lambda}(q,r)(d,e)=q(d,e)\) if \(d\in \lambda\); \(if_{\lambda}(q,r)(d,e)=r(d,e)\) otherwise; \(if_{\lambda}(q,r)(d,e)=1\) if \(d\in \lambda\) and \(e=f(d)\) or d is not in \(\lambda\) and \(e=g(d)\). The collection of functions \(if_{\lambda}\) as \(\lambda\) ranges over a fixed Boolean algebra, is the formalization of ''if-then-else''. Now fix a set D and let G be the Boolean algebra of all subsets of D. The author finds a finite axiomatization of all equations in \(+\), 0 and the \(if_{\lambda}\), \(\lambda\in G\), which are valid in all structures of the form \((Q,+,0,if_{\lambda})\), where Q is the set of functions \(D\times E\to A\), where A is an abelian monoid; equivalently, one may restrict A to be the monoid of the nonnegative integers. By the addition of the equation \(x+x=x\), the author obtains an approximation of all equations valid in structures of the form \(2^{D\times E}\), where 2 is the two-element monoid with \(1+1=1.\) The proofs given are in the author's usual style; terse but elegant. Other treatments of ''if-then-else'' have been given by \textit{I. Guessarian} and \textit{J. Meseguer} (to appear), and by the reviewer and \textit{R. Tindell} [SIAM J. Comput. 12, 677-707 (1983; Zbl 0518.68010)].