×

The axiomatization of override and update. (English) Zbl 1194.03020

Summary: There are only very few natural ways in which arbitrary functions can be combined. One composition operator is override: for arbitrary functions \(f\) and \(g\), \(f\triangleright g\) is the function with domain \(\text{dom}(f)\cup \text{dom}(g)\) that behaves like \(f\) on \(\text{dom}(f)\) and like \(g\) on \(\text{dom}(g)\setminus \text{dom}(f)\). Another operator is update: \(f[g]\) has the same domain as \(f\), behaves like \(f\) on \(\text{dom}(f)\setminus \text{dom}(g)\), and like \(g\) on \(\text{dom}(f)\cap \text{dom}(g)\). These operators are widely used, especially within computer science, where for instance \(f[g]\) may denote the new state that results when in state \(f\) the updates given as \(g\) are applied. It is therefore surprising that thus far no axiomatization of these operators has been proposed in the literature. As an auxiliary operator we consider the minus operator: \(f-g\) is the restriction of \(f\) to the domain \(\text{dom}(f)\setminus \text{dom}(g)\). The update operator can be defined in terms of override and minus. We present five equations that together constitute a sound and complete axiomatization of override and minus. As part of our completeness proof, we infer a large number of useful derived laws using the proof assistant Isabelle. With the help of the SMT solver Yices, we establish independence of the axioms. Thus, our axiomatization is also minimal. Finally, we establish that override and minus are functionally complete in the sense that any operation on general functions that corresponds to a valid coloring of a Venn diagram can be described using just these two operations.

MSC:

03B35 Mechanization of proofs and logical operations
03C05 Equational classes, universal algebra in model theory
08A02 Relational systems, laws of composition
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Z; Isabelle/HOL; Yices
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] de Bakker, J., Mathematical Theory of Program Correctness (1980), Prentice Hall: Prentice Hall Englewood Cliffs · Zbl 0452.68011
[2] Balbes, R.; Dwinger, P., Distributive Lattices (1974), University of Missouri Press: University of Missouri Press Columbia · Zbl 0321.06012
[3] Berendsen, J.; Vaandrager, F., Compositional abstraction in real-time model checking, (Cassez, F.; Jard, C., Formal Modeling and Analysis of Timed Systems: … FORMATS. Formal Modeling and Analysis of Timed Systems: … FORMATS, Lecture Notes in Computer Science, vol. 5215 (2007), Springer: Springer Berlin), 233-249, Tech. Rep. ICIS-R07027, Radboud University, Nijmegen, an extended abstract appeared · Zbl 1171.68545
[4] Birkhoff, G., On the structure of abstract algebras, Proceedings of the Cambridge Philosophical Society, 31, 4, 433-454 (1935) · JFM 61.1026.07
[5] Chang, C. C.; Keisler, H. J., Model Theory, Studies in Logic and the Foundations of Mathematics, vol. 73 (1990), North-Holland: North-Holland Amsterdam · Zbl 0697.03022
[6] Damm, W.; Josko, B.; Hungar, H.; Pnueli, A., A compositional real-time semantics of STATEMATE designs, (de Roever, W.-P.; Langmaack, H.; Pnueli, A., Compositionality, the Significant Difference: … COMPOS ’97. Compositionality, the Significant Difference: … COMPOS ’97, Lecture Notes in Computer Science, vol. 1536 (1998), Springer: Springer Berlin), 186-238
[7] Davey, B. A.; Priestley, H. A., Introduction to Lattices and Order (1990), Cambridge University Press: Cambridge University Press Cambridge, UK · Zbl 0701.06001
[8] Goldberg, A. V.; Tarjan, R. E., A new approach to the maximum-flow problem, Journal of the ACM, 35, 4, 921-940 (1988) · Zbl 0661.90031
[9] C. Grabmayer, A. Visser, Axiomatization of generalized Boolean algebras, personal communication, 2007; C. Grabmayer, A. Visser, Axiomatization of generalized Boolean algebras, personal communication, 2007
[10] Jones, C., Systematic Software Development using VDM (1986), Prentice Hall: Prentice Hall Englewood Cliffs · Zbl 0584.68008
[11] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer: Springer Berlin · Zbl 0994.68131
[12] Post, E. L., The Two-Valued Iterative Systems of Mathematical Logic, Annals of Mathematics Studies, vol. 5 (1941), Princeton University Press: Princeton University Press Princeton · Zbl 0063.06326
[13] Prover9/Mace4
[14] Spivey, J. M., The Z Notation: A Reference Manual (1989), Prentice Hall: Prentice Hall Englewood Cliffs · Zbl 0777.68003
[15] Stone, M. H., Subsumption of Boolean algebras under the theory of rings, Proceedings of the National Academy of Sciences of the USA, 21, 2, 103-105 (1935) · Zbl 0011.05104
[16] Winskel, G., The Formal Semantics of Programming Languages: An Introduction (1993), MIT Press: MIT Press Cambridge, MA · Zbl 0919.68082
[17] Yices
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.