×

Override and update. (English) Zbl 1454.08004

Summary: 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.

MSC:

08A70 Applications of universal algebra in computer science
03B35 Mechanization of proofs and logical operations
20M20 Semigroups of transformations, relations, partitions, etc.
03B70 Logic in computer science
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Software:

Z; Prover9; Mace4
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Berendsen, J.; Jansen, D. N.; Schmaltz, J.; Vaandrager, F. W., The axiomatization of override and update, J. Appl. Log., 8, 141-150 (2010) · Zbl 1194.03020
[2] Burris, S.; Sankappanavar, H. P., A Course in Universal Algebra, Graduate Texts in Mathematics (1981), Springer-Verlag · Zbl 0478.08001
[3] Cirulis, J., Nearlattices with an overriding operation, Order, 28, 33-51 (2011) · Zbl 1216.06003
[4] Cvetko-Vah, K.; Leech, J.; Spinks, M., Skew lattices and binary operations on functions, J. Appl. Log., 11, 253-265 (2013) · Zbl 1284.03279
[5] Garvac’kiĭ, V. S., ∩-semigroups of transformations, (Theory of Semigroups and Its Applications, vol. 2 (1971), Izdat. Saratov. Univ.: Izdat. Saratov. Univ. Saratov), 2-13, (in Russian) · Zbl 0245.20064
[6] Hirsch, R.; Jackson, M.; Mikulas, Sz., The algebra of functions with antidomain and range, J. Pure Appl. Algebra, 220, 2214-2239 (2016) · Zbl 1377.08001
[7] Howie, J. M., Fundamentals of Semigroup Theory (1995), Oxford University Press: Oxford University Press New York · Zbl 0835.20077
[8] Jackson, M.; Stokes, T., Modal restriction semigroups: towards an algebra of functions, Int. J. Algebra Comput., 21, 1053-1095 (2011) · Zbl 1256.20058
[9] Jones, C., Systematic Software Development Using VDM (1986), Prentice Hall: Prentice Hall Englewood Cliffs · Zbl 0584.68008
[10] Kozen, D., A completeness theorem for Kleene algebras and the algebra of regular events, Inf. Comput., 110, 366-390 (1994) · Zbl 0806.68082
[11] Kozen, D., On the complexity of reasoning in Kleene algebra, Inf. Comput., 179, 152-162 (2002) · Zbl 1096.03077
[12] Leech, J., Skew Boolean algebras, Algebra Univers., 27, 497-506 (1990) · Zbl 0719.06010
[13] Margolis, S.; Saliola, F.; Steinberg, B., Semigroups embeddable in hyperplane face monoids, Semigroup Forum, 89, 236-248 (2014) · Zbl 1323.20055
[14] McCune, W., Prover9 and Mace4, version LADR-Dec-2007
[15] Schein, B. M., Restrictively multiplicative algebras of transformations, Izv. Vysš. Učebn. Zaved., Mat., 1970, 4(95), 91-102 (1970), (in Russian) · Zbl 0199.33501
[16] Spivey, J. M., The Z Notation: A Reference Manual (1989), Prentice Hall: Prentice Hall Englewood Cliffs · Zbl 0777.68003
[17] Vagner, V. V., Restrictive semigroups, Izv. Vysš. Učebn. Zaved., Mat., 1962, 6(31), 19-27 (1962), (in Russian) · Zbl 0131.01801
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.