Override and restricted union for partial functions

TL;DR

This paper explores algebraic structures of partial functions with override and intersection operations, establishing finite axiomatizations for certain signatures and connecting them to known algebraic varieties.

Contribution

It introduces new algebraic signatures involving override and intersection, proving finite axiomatisations and linking to existing algebraic frameworks.

Findings

Finite axiomatisation of the $(ar{igvee})$ signature as a quasivariety.

Finite axiomatisation of the $(igcup,igcap)$ signature as a variety.

Connections established between these structures and distributive o-semilattices.

Abstract

The {\em override} operation $\sqcup$ 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$ is the function with domain $dom(f)\cup dom(g)$ that agrees with $f$ on $dom(f)$ and with $g$ on $dom(g) \backslash dom(f)$. Jackson and the author have shown that there is no finite axiomatisation of algebras of functions of signature $(\sqcup)$. But adding operations (such as {\em update}) to this minimal signature can lead to finite axiomatisations. For the functional signature $(\sqcup,\backslash)$ where $\backslash$ 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)$ for all functions $f$ and $g$; this is the largest domain restriction of the binary relation $f\cup g$ that gives a partial function. Now $f\cap g=f\backslash(f\backslash g)$ and $f\sqcup g=f\curlyvee(f\curlyvee g)$ for all functions $f,g$, so the signatures $(\curlyvee)$ and $(\sqcup,\cap)$ are both intermediate between $(\sqcup)$ and $(\sqcup,\backslash)$ in expressive power. We show that each is finitely axiomatised, with the former giving a proper quasivariety and the latter the variety of associative distributive o-semilattices in the sense of Cirulis.