Override and update are natural constructions for combining partial functions, which arise in various program specification contexts. We use an unexpected connection with combinatorial geometry to provide a complete finite system of equational axioms for the first order theory of the override and update constructions on partial functions, resolving the main unsolved problem in the area.<p></p>
Funding
The first author was partially supported by ARC Future Fellowship FT120100666.
History
Publication Date
2021-03-01Journal
Journal of Pure and Applied AlgebraVolume
225Issue
3Article Number
106532Pagination
17p. (p. 1-17)Publisher
Elsevier BVISSN
0022-4049Rights Statement
© 2021 The Authors. This manuscript version is made available under the CC-BY-NC-ND 4.0 license, whereby credit must be given to the creator, only noncommercial uses of the work are permitted and no derivatives or adaptations of the work are permitted: https://creativecommons.org/licenses/by-nc-nd/4.0/
