×

Determinisation of relational substitutions in ordered categories with domain. (English) Zbl 1203.18007

Summary: Restating a unification problem as a single relational substitution instead of as multiple functional substitutions (or terms), a solution becomes a “determiniser” arrow and allows formalisation in the context of locally ordered categories with domain. This relies on the determinacy concept of “characterisation by domain” introduced by Desharnais and Möller for Kleene algebras with domain; this is here applied in the weakest possible setting.
We show how “most general determinisers” can be seen as generalisation of quotient projections of partial equivalence relations, and show a characterisation that manages to avoid using converse or symmetry by employing restricted residuals instead.

MSC:

18C10 Theories (e.g., algebraic theories), structure, and semantics
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Z
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] R. Backhouse, P. Hoogendijk, Elements of a relational theory of datatypes, in: B. Möller, H. Partsch, S. Schuman (Eds.), Formal Program Development. Proc. IFIP TC2/WG 2.1 State of the Art Seminar, Rio de Janeiro, January 1992, LNCS, vol. 755, 1992, pp. 7-42.; R. Backhouse, P. Hoogendijk, Elements of a relational theory of datatypes, in: B. Möller, H. Partsch, S. Schuman (Eds.), Formal Program Development. Proc. IFIP TC2/WG 2.1 State of the Art Seminar, Rio de Janeiro, January 1992, LNCS, vol. 755, 1992, pp. 7-42.
[2] R.C. Backhouse, Constructive lattice theory, October 1993. <http://www.cs.nott.ac.uk/∼;rcb/papers/abstract.html#isos>.; R.C. Backhouse, Constructive lattice theory, October 1993. <http://www.cs.nott.ac.uk/∼;rcb/papers/abstract.html#isos>.
[3] Backhouse, R. C.; deBruin, P. J.; Malcom, G.; Voermans, E.; vander Woude, J., Relational catamorphisms, (Möller, B., Constructing Programs From Specifications. IFIP WG 2.1 (1991), North-Holland), 319-371
[4] Beck, J., Distributive laws, (Appelgate, H.; Eckmann, B., Seminar on Triples and Categorical Homology Theory, ETH, 1966-1967. Seminar on Triples and Categorical Homology Theory, ETH, 1966-1967, Lect. Notes in Math., vol. 80 (1969), Springer), 119-140
[5] Berghammer, R.; Haeberer, A. M.; Schmidt, G.; Veloso, P. A.S., Comparing two different approaches to products in abstract relation algebra, (Nivat, M.; Rattray, C.; Rus, T.; Scollo, G., AMAST ’93. Workshops in Computing (1994), Springer), 167-176
[6] (Berghammer, R.; Jaoua, A.; Möller, B., Relations and Kleene Algebra in Computer Science - 11th International Conference on Relational Methods in Computer Science, and Sixth International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2009, Doha, Qatar, November 1-5, 2009. Proceedings. Relations and Kleene Algebra in Computer Science - 11th International Conference on Relational Methods in Computer Science, and Sixth International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2009, Doha, Qatar, November 1-5, 2009. Proceedings, LNCS, vol. 5827 (2009), Springer) · Zbl 1177.68003
[7] Berghammer, R.; Schmidt, G.; Zierer, H., Symmetric quotients and domain constructions, Inform. Process. Lett., 33, 3, 163-168 (1989) · Zbl 0689.68095
[8] Bird, R. S.; deMoor, O., Algebra of programming, International Series in Computer Science, vol. 100 (1997), Prentice Hall
[9] J. Desharnais, P. Jipsen, G. Struth, Domain and antidomain semigroups, in: R. Berghammer et al. (Eds.), 2009, pp. 73-87.; J. Desharnais, P. Jipsen, G. Struth, Domain and antidomain semigroups, in: R. Berghammer et al. (Eds.), 2009, pp. 73-87. · Zbl 1267.03067
[10] Desharnais, J.; Möller, B., Characterizing determinacy in Kleene algebras, Inform. Sci., 139, 253-273 (2001) · Zbl 1004.68105
[11] Desharnais, J.; Möller, B.; Struth, G., Kleene algebra with domain, ACM Trans. Comput. Logic, 7, 4, 798-833 (2006) · Zbl 1367.68205
[12] Doornbos, H.; van Gasteren, N.; Backhouse, R., Programs and datatypes, (Brink, C.; Kahl, W.; Schmidt, G., Relational Methods in Computer Science, Advances in Computing Science (1997), Springer: Springer Wien, New York), 150-165, (Ch. 10) · Zbl 0884.68081
[13] Eklund, P.; Galán, M. A.; Medina, J.; OjedaAciego, M.; Valverde, A., A categorical approach to unification of generalised terms, Electron. Notes Comput. Sci., 66, 5, 41-51 (2002), (Special Issue: UNCL’2002, Unification in Non-Classical Logics (ICALP 2002 Satellite Workshop)) · Zbl 1270.03141
[14] Eklund, P.; Galán, M. A.; Medina, J.; OjedaAciego, M.; Valverde, A., Set functors, \(l\)-fuzzy set categories, and generalized terms, Comput. Math. Appl., 43, 6-7, 693-705 (2002) · Zbl 1035.03030
[15] P. Eklund, M.A. Galán, M. Ojeda-Aciego, A. Valverde, Set functors and generalised terms, in: Proc. IPMU 2000, Eighth Information Processing and Management of Uncertainty in Knowledge-based Systems Conference, vol. III, 2000, pp. 1595-1599.; P. Eklund, M.A. Galán, M. Ojeda-Aciego, A. Valverde, Set functors and generalised terms, in: Proc. IPMU 2000, Eighth Information Processing and Management of Uncertainty in Knowledge-based Systems Conference, vol. III, 2000, pp. 1595-1599.
[16] P. Eklund, R. Helgesson, Composing partially ordered monads, in: R. Berghammer et al. (Eds.), 2009, pp. 88-102.; P. Eklund, R. Helgesson, Composing partially ordered monads, in: R. Berghammer et al. (Eds.), 2009, pp. 88-102. · Zbl 1267.18005
[17] P. Freyd, P. Hoogendijk, O. deMoor, Membership of datatypes, unpublished manuscript, December 1993 (see also Bird and de Moor, 1997, Sect. 6.5).; P. Freyd, P. Hoogendijk, O. deMoor, Membership of datatypes, unpublished manuscript, December 1993 (see also Bird and de Moor, 1997, Sect. 6.5).
[18] P.J. Freyd, A. Scedrov, Categories, allegories, North-Holland Mathematical Library, vol. 39, North-Holland, Amsterdam, 1990.; P.J. Freyd, A. Scedrov, Categories, allegories, North-Holland Mathematical Library, vol. 39, North-Holland, Amsterdam, 1990. · Zbl 0698.18002
[19] Goguen, J. A., What is unification?, (Aït-Kaci, H.; Nivat, M., Resolution of Equations in Algebraic Structures. 1: Algebraic Techniques (1989), Academic Press: Academic Press Boston), 217-261
[20] M.P. Jones, L. Duponcheel, Composing monads, Research Report YALEU/DCS/RR-1004, Yale University, New Haven, CT, USA, December 1993.; M.P. Jones, L. Duponcheel, Composing monads, Research Report YALEU/DCS/RR-1004, Yale University, New Haven, CT, USA, December 1993.
[21] W. Kahl, A relation-algebraic approach to graph structure transformation, Habil. Thesis, Fakultät für Informatik, Univ. der Bundeswehr München, Techn. Report 2002-03, 2001. <http://sqrl.mcmaster.ca/∼;kahl/Publications/RelRew/>.; W. Kahl, A relation-algebraic approach to graph structure transformation, Habil. Thesis, Fakultät für Informatik, Univ. der Bundeswehr München, Techn. Report 2002-03, 2001. <http://sqrl.mcmaster.ca/∼;kahl/Publications/RelRew/>.
[22] Kahl, W., Refactoring heterogeneous relation algebras around ordered categories and converse, J. Relational Methods Comput. Sci., 1, 277-313 (2004)
[23] Kahl, W., Determinisation of relational substitutions in ordered categories with domain, (Berghammer, R.; Möller, B.; Struth, G., Relations and Kleene-Algebra in Computer Science, RelMiCS/AKA 2008. Relations and Kleene-Algebra in Computer Science, RelMiCS/AKA 2008, LNCS, vol. 4988 (2008), Springer), 243-258 · Zbl 1139.18006
[24] Kahl, W., Relational semigroupoids: Abstract relation-algebraic interfaces for finite relations between infinite types, J. Logic Algebraic Program., 76, 1, 60-89 (2008) · Zbl 1139.18005
[25] Kawahara, Y., Notes on the universality of relational functors, Mem. Fac. Sci. Kyushu Univ. Ser. A, 27, 2, 275-289 (1973) · Zbl 0274.18004
[26] D. Kozen, Natural transformations as rewrite rules and monad composition, Tech. Rep. TR2004-1942, Computer Science Department, Cornell University, July 2004.; D. Kozen, Natural transformations as rewrite rules and monad composition, Tech. Rep. TR2004-1942, Computer Science Department, Cornell University, July 2004.
[27] Lawvere, F. W., Functorial semantics of algebraic theories, Proc. Natl. Acad. Sci. USA, 50, 869-872 (1963) · Zbl 0119.25901
[28] Möller, B., Kleene getting lazy, Sci. Comput. Programming, 65, 195-214 (2007) · Zbl 1109.68060
[29] Olivier, J.-P.; Serrato, D., Catégories de Dedekind. Morphismes dans les catégories de Schröder, C. R. Acad. Sci. Paris Ser. A-B, 290, 939-941 (1980) · Zbl 0438.18003
[30] Olivier, J.-P.; Serrato, D., Squares and rectangles in relation categories – three cases: Semilattice, distributive lattice and boolean non-unitary, Fuzzy Sets and Systems, 72, 167-178 (1995) · Zbl 0844.18002
[31] Rydeheard, D.; Burstall, R., A categorical unification algorithm, (Proc. Summer Workshop on Category Theory and Computer Programming 1985. Proc. Summer Workshop on Category Theory and Computer Programming 1985, LNCS, vol. 240 (1986), Springer), 493-505 · Zbl 0616.68016
[32] Schmidt, G.; Ströhlein, T., Relation algebras – concept of points and representability, Discrete Math., 54, 83-92 (1985) · Zbl 0575.03040
[33] J.M. Spivey, The Z Notation: A Reference Manual, second ed., Prentice Hall International Series in Computer Science, Prentice Hall, 1992 (out of print). <http://spivey.oriel.ox.ac.uk/∼;mike/zrm/>.; J.M. Spivey, The Z Notation: A Reference Manual, second ed., Prentice Hall International Series in Computer Science, Prentice Hall, 1992 (out of print). <http://spivey.oriel.ox.ac.uk/∼;mike/zrm/>.
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.