Equational Bases for If–Then–Else
Alan H. Mekler, Evelyn M. Nelson · SIAM Journal on Computing · 1987
Four formalizations of the instruction if–then–else are considered. Let K be an equational class of algebras. Assume the language has constants $ \bot $ in case II, T, F, $ \bot $ in case III and T in case IV. Any equational class with $ \bot $ is assumed to be strict, i.e. satisfies $F(\_, \bot ,\_) = \bot $ for all functions f Form the classes I $K^d $, II $K^{d \bot } $, III $K^t $ and IV $K^{t'} $ by adding an operation $[,,,]$ in cases I and II defined by \[ {\text{I}}\quad [x,y,z,w] = \left\{ \begin{gathered} z\quad {\text{if }}x = y, \hfill \\ w\quad {\text{else}} \hfill \\ \end{gathered} \right.\qquad {\text{II}}\quad [x,y,z,w] = \left\{ \begin{gathered} z\quad {\text{if }}x = y e \bot \hfill \\ w\quad {\text{if }} \bot e x e y e \bot , \hfill \\ \bot \quad {\text{else,}} \hfill \\ \end{gathered} \right. \]and by adding an operation $[,,]$ in cases III and IV defined by \[ {\text{III}}\quad [x,y,z] = \left\{ \begin{gathered} y\quad {\text{if }}x = T, \hfill \\ z\quad {\text{if }}x = F \hfill \\ \bot \quad {\text{else}}, \hfill \\ \end{gathered} \right.{\text{ and IV }}[x,y,z] = \left\{ \begin{gathered} y\quad {\text{if }}x = T, \hfill \\ z\quad {\text{else}}{\text{.}} \hfill \\ \end{gathered} \right. \] (In case III only the one point algebra and those algebras in which T, F,$ \bot $ are distinct are used to form $K'$.) In all four cases a finite basis for the equational theory of $K^x (x = d,d \bot ,t,t')$ relative to the equational theory of K are given. For $K^d $ such a basis was previously known. If the word problem for K is decidable then so is the equational theory of $K^x $. For $K^d $, as was previously known, the converse holds, but for $K^t $ the implication does not always reverse.