Abstract
The correspondence between up-closed multirelations and isotone predicate transformers is well known. Less known is that multirelations have also been used for modelling topological contact, not only computations. We investigate how properties from these two lines of research translate to predicate transformers. To this end, we express the correspondence of multirelations and predicate transformers using relation algebras. It turns out to be similar to the correspondence between contact relations and closure operations. Many results generalise from up-closed to arbitrary multirelations.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Aumann, G.: Kontakt-Relationen. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Mathematisch-Naturwissenschaftliche Klasse, pp. 67–77 (1970)
Aumann, G.: AD ARTEM ULTIMAM - Eine Einführung in die Gedankenwelt der Mathematik. R. Oldenbourg Verlag (1974)
Back, R.J., von Wright, J.: Refinement Calculus. Springer, New York (1998)
Backhouse, R.C., van der Woude, J.: Demonic operators and monotype factors. Math. Struct. Comput. Sci. 3(4), 417–433 (1993)
Berghammer, R., Guttmann, W.: Closure, properties and closure properties of multirelations (submitted 2015)
Berghammer, R., Schmidt, G., Zierer, H.: Symmetric quotients and domain constructions. Inf. Process. Lett. 33(3), 163–168 (1989)
Berghammer, R., Zierer, H.: Relational algebraic semantics of deterministic and nondeterministic programs. Theor. Comput. Sci. 43, 123–147 (1986)
Bird, R., de Moor, O.: Algebra of Programming. Prentice Hall (1997)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)
Freyd, P.J., Ščedrov, A.: Categories, Allegories. North-Holland Mathematical Library, vol. 39. Elsevier Science Publishers (1990)
Furusawa, H., Struth, G.: Concurrent dynamic algebra (2014). CoRR http://arxiv.org/abs/1407.5819
Gries, D.: The Science of Programming. Springer, New York (1981)
Guttmann, W.: Multirelations with infinite computations. J. Log. Algebr. Meth. Program. 83(2), 194–211 (2014)
Hesselink, W.H.: Multirelations are predicate transformers (2004). Available from http://www.cs.rug.nl/~wim/pub/whh318.pdf
Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127–132 (1987)
Kozen, D.: Kleene algebra with tests. ACM Trans. Progr. Lang. Syst. 19(3), 427–443 (1997)
Macedo, H.D., Oliveira, J.N.: Typing linear algebra: a biproduct-oriented approach. Sci. Comput. Program. 78(11), 2160–2191 (2013)
Martin, C.E., Curtis, S.A.: The algebra of multirelations. Math. Struct. Comput. Sci. 23(3), 635–674 (2013)
Martin, C.E., Curtis, S.A., Rewitzky, I.: Modelling angelic and demonic nondeterminism with multirelations. Sci. Comput. Program. 65(2), 140–158 (2007)
Morris, J.M., Tyrrell, M.: Modelling higher-order dual nondeterminacy. Acta Inf. 45(6), 441–465 (2008)
Naumann, D.A.: A categorical model for higher order imperative programming. Math. Struct. Comput. Sci. 8(4), 351–399 (1998)
Parikh, R.: Propositional logics of programs: new directions. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 347–359. Springer, Heidelberg (1983)
Peleg, D.: Concurrent dynamic logic. J. ACM 34(2), 450–479 (1987)
Preoteasa, V.: Algebra of monotonic Boolean transformers. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 140–155. Springer, Heidelberg (2011)
Rewitzky, I.: Binary multirelations. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, vol. 2929, pp. 256–271. Springer, Heidelberg (2003)
Rewitzky, I., Brink, C.: Monotone predicate transformers as up-closed multirelations. In: Schmidt, R.A. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 311–327. Springer, Heidelberg (2006)
Schmidt, G.: Partiality I: embedding relation algebras. J. Log. Algebr. Program. 66(2), 212–238 (2006)
Schmidt, G.: Relational Mathematics. Cambridge University Press, Cambridge (2011)
Schmidt, G., Berghammer, R.: Contact, closure, topology, and the linking of row and column types of relations. J. Log. Algebr. Program. 80(6), 339–361 (2011)
Schmidt, G., Ströhlein, T.: Relationen und Graphen. Springer, Heidelberg (1989)
Tarski, A.: On the calculus of relations. J. Symb. Log. 6(3), 73–89 (1941)
Tsumagari, N.: Probabilistic relational models of complete IL-semirings. Bull. Inf. Cybern. 44, 87–109 (2012)
Acknowledgments
We thank Hitoshi Furusawa and Georg Struth for pointing out related work and the anonymous referees for making helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Berghammer, R., Guttmann, W. (2015). A Relation-Algebraic Approach to Multirelations and Predicate Transformers. In: Hinze, R., Voigtländer, J. (eds) Mathematics of Program Construction. MPC 2015. Lecture Notes in Computer Science(), vol 9129. Springer, Cham. https://doi.org/10.1007/978-3-319-19797-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-19797-5_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19796-8
Online ISBN: 978-3-319-19797-5
eBook Packages: Computer ScienceComputer Science (R0)