English

Override and restricted union for partial functions

Logic 2021-06-29 v1

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 ff and gg, fgf\sqcup g is the function with domain dom(f)dom(g)dom(f)\cup dom(g) that agrees with ff on dom(f)dom(f) and with gg on dom(g)\dom(f)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 fg=(fg)(gf)f\curlyvee g=(f\sqcup g)\cap (g\sqcup f) for all functions ff and gg; this is the largest domain restriction of the binary relation fgf\cup g that gives a partial function. Now fg=f\(f\g)f\cap g=f\backslash(f\backslash g) and fg=f(fg)f\sqcup g=f\curlyvee(f\curlyvee g) for all functions f,gf,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.

Cite

@article{arxiv.2106.14398,
  title  = {Override and restricted union for partial functions},
  author = {Tim Stokes},
  journal= {arXiv preprint arXiv:2106.14398},
  year   = {2021}
}
R2 v1 2026-06-24T03:39:06.738Z