Override and restricted union for partial functions

Abstract The override operation $$\sqcup $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mo>⊔</mml:mo> </mml:math> is a natural one in computer science, and has connections with other areas of mathematics such as hyperplane arrangements. For arbitrary functions f and g , $$f\sqcup g$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>f</mml:mi> <mml:mo>⊔</mml:mo> <mml:mi>g</mml:mi> </mml:mrow> </mml:math> is the function with domain $${{\,\textrm{dom}\,}}(f)\cup {{\,\textrm{dom}\,}}(g)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mrow> <mml:mspace/> <mml:mtext>dom</mml:mtext> <mml:mspace/> </mml:mrow> <mml:mo>(</mml:mo> <mml:mi>f</mml:mi> <mml:mo>)</mml:mo> <mml:mo>∪</mml:mo> <mml:mrow> <mml:mspace/> <mml:mtext>dom</mml:mtext> <mml:mspace/> </mml:mrow> <mml:mo>(</mml:mo> <mml:mi>g</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> that agrees with f on $${{\,\textrm{dom}\,}}(f)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mrow> <mml:mspace/> <mml:mtext>dom</mml:mtext> <mml:mspace/> </mml:mrow> <mml:mo>(</mml:mo> <mml:mi>f</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> and with g on $${{\,\textrm{dom}\,}}(g) \backslash {{\,\textrm{dom}\,}}(f)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mrow> <mml:mspace/> <mml:mtext>dom</mml:mtext> <mml:mspace/> </mml:mrow> <mml:mo>(</mml:mo> <mml:mi>g</mml:mi> <mml:mo>)</mml:mo> <mml:mo>\</mml:mo> <mml:mrow> <mml:mspace/> <mml:mtext>dom</mml:mtext> <mml:mspace/> </mml:mrow> <mml:mo>(</mml:mo> <mml:mi>f</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> . Jackson and the author have shown that there is no finite axiomatisation of algebras of functions of signature $$(\sqcup )$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>(</mml:mo> <mml:mo>⊔</mml:mo> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> . But adding operations (such as update ) to this minimal signature can lead to finite axiomatisations. For the functional signature $$(\sqcup ,\backslash )$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>(</mml:mo> <mml:mo>⊔</mml:mo> <mml:mo>,</mml:mo> <mml:mo>\</mml:mo> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> where $$\backslash $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mo>\</mml:mo> </mml:math> is set-theoretic difference, Cirulis has given a finite equational axiomatisation as subtraction o-semilattices. Define $$f\curlyvee g=(f\sqcup g)\cap (g\sqcup f)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>f</mml:mi> <mml:mo>⋎</mml:mo> <mml:mi>g</mml:mi> <mml:mo>=</mml:mo> <mml:mo>(</mml:mo> <mml:mi>f</mml:mi> <mml:mo>⊔</mml:mo> <mml:mi>g</mml:mi> <mml:mo>)</mml:mo> <mml:mo>∩</mml:mo> <mml:mo>(</mml:mo> <mml:mi>g</mml:mi> <mml:mo>⊔</mml:mo> <mml:mi>f</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> for all functions f and g ; this is the largest domain restriction of the binary relation $$f\cup g$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>f</mml:mi> <mml:mo>∪</mml:mo> <mml:mi>g</mml:mi> </mml:mrow> </mml:math> that gives a partial function. Now $$f\cap g=f\backslash (f\backslash g)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>f</mml:mi> <mml:mo>∩</mml:mo> <mml:mi>g</mml:mi> <mml:mo>=</mml:mo> <mml:mi>f</mml:mi> <mml:mo>\</mml:mo> <mml:mo>(</mml:mo> <mml:mi>f</mml:mi> <mml:mo>\</mml:mo> <mml:mi>g</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> and $$f\sqcup g=f\curlyvee (f\curlyvee g)$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>f</mml:mi> <mml:mo>⊔</mml:mo> <mml:mi>g</mml:mi> <mml:mo>=</mml:mo> <mml:mi>f</mml:mi> <mml:mo>⋎</mml:mo> <mml:mo>(</mml:mo> <mml:mi>f</mml:mi> <mml:mo>⋎</mml:mo> <mml:mi>g</mml:mi> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> for all functions f , g , so the signatures $$(\curlyvee )$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>(</mml:mo> <mml:mo>⋎</mml:mo> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> and $$(\sqcup ,\cap )$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>(</mml:mo> <mml:mo>⊔</mml:mo> <mml:mo>,</mml:mo> <mml:mo>∩</mml:mo> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> are both intermediate between $$(\sqcup )$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>(</mml:mo> <mml:mo>⊔</mml:mo> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> and $$(\sqcup ,\backslash )$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>(</mml:mo> <mml:mo>⊔</mml:mo> <mml:mo>,</mml:mo> <mml:mo>\</mml:mo> <mml:mo>)</mml:mo> </mml:mrow> </mml:math> in expressive power. We show that each is finitely axiomatised, with the former giving a proper quasivariety and the latter the variety of associative distributiv