×

Boolean restriction categories and taut monads. (English) Zbl 1097.68071

Summary: A Boolean category is a restriction category if and only if it has one exception and all morphisms are deterministic. In the category of sets, taut monads are precisely the Boolean ones. It follows that collection monad types in Haskell inherit an assertion calculus based on dynamic logic.

MSC:

68Q55 Semantics in the theory of computing
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Carboni, A., Bicategories of partial maps, Cahiers Topologie Géom. Différentielle, 28, 111-126 (1987) · Zbl 0631.18002
[2] Cockett, J. R.B.; Lack, S., Restriction categories I: categories of partial maps, Theoret. Comput. Sci., 270, 223-259 (2002) · Zbl 0988.18003
[3] Curien, P. L.; Obtulowicz, A., Partiality and cartesian categories, Inform. and Comput., 80, 50-95 (1989) · Zbl 0674.18001
[4] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[5] DiPaola, R. A.; Heller, A., Dominical categories: recursion theory without elements, J. Symbolic Logic, 52, 595-635 (1987) · Zbl 0649.03032
[6] S. Eilenberg, Automata, Languages and Machines, Vol. A, Academic Press, New York, 1974.; S. Eilenberg, Automata, Languages and Machines, Vol. A, Academic Press, New York, 1974. · Zbl 0317.94045
[7] Elgot, C. C., Monadic computation and iterative algebraic theories, (Rose, H. E.; Shepherdson, J. C., Proc. Logic Colloq. ’73 (1975), North-Holland: North-Holland Amsterdam), 175-230 · Zbl 0327.02040
[8] Fischer, M. J.; Ladner, R. E., Propositional dynamic logic of regular programs, J. Comput. System Sci., 18, 286-294 (1979)
[9] Kleisli, H., Every standard construction is induced by a pair of adjoint functors, Proc. Amer. Math. Soc., 16, 544-546 (1965) · Zbl 0138.01704
[10] D. Kozen, A representation theorem for *-free PDL, Lecture Notes in Computer Science, Vol. 85, Springer, Berlin, 1980, pp. 351-362.; D. Kozen, A representation theorem for *-free PDL, Lecture Notes in Computer Science, Vol. 85, Springer, Berlin, 1980, pp. 351-362. · Zbl 0451.03005
[11] Lawson, M. V., Inverse Semigroups, the Theory of Partial Symmetries (1998), World Scientific Publishing: World Scientific Publishing Singapore · Zbl 1079.20505
[12] G. Longo, E. Moggi, Cartesian closed categories and partial morphisms for effective type structures, in: G. Kahn, D.B. McQueen, G. Plotkin (Eds.), Internat. Symp. Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173, Springer, Berlin, 1984, pp. 235-255.; G. Longo, E. Moggi, Cartesian closed categories and partial morphisms for effective type structures, in: G. Kahn, D.B. McQueen, G. Plotkin (Eds.), Internat. Symp. Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173, Springer, Berlin, 1984, pp. 235-255. · Zbl 0564.03037
[13] Manes, E. G., Predicate Transformer Semantics (1992), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0784.68003
[14] Manes, E. G., Implementing collection classes with monads, Math. Structures Comput. Sci., 8, 231-276 (1998) · Zbl 0916.68016
[15] E.G. Manes, Boolean monads for functional programming, in: N. Callaos, S. Long, M. Loutfi (Eds.), Proc. World Multiconference on Systemics, Cybernetics and Informatics ISAS/SCI 2001, Orlando, Florida, USA, XVII, 2001, pp. 189-193.; E.G. Manes, Boolean monads for functional programming, in: N. Callaos, S. Long, M. Loutfi (Eds.), Proc. World Multiconference on Systemics, Cybernetics and Informatics ISAS/SCI 2001, Orlando, Florida, USA, XVII, 2001, pp. 189-193.
[16] Manes, E. G., Taut monads and T0 spaces, Theoret. Comput. Sci., 275, 79-109 (2002) · Zbl 1033.18001
[17] Manes, E. G., Monads of sets, (Hazewinkel, M., Handbook of Algebra, Vol. 3 (2003), Elsevier: Elsevier Amsterdam), 67-153 · Zbl 1064.18003
[18] E.G. Manes, Guarded and banded semigroups, Semigroup Forum, to appear.; E.G. Manes, Guarded and banded semigroups, Semigroup Forum, to appear. · Zbl 1097.20044
[19] Moggi, E., Partial morphisms in categories of effective objects, Inform. and Comput., 76, 250-277 (1988) · Zbl 0655.18005
[20] Moggi, E., Notions of computation and monads, Inform. and Comput., 93, 55-92 (1991) · Zbl 0723.68073
[21] Mulry, P. S., Monads and algebras in the semantics of partial data types, Theoret. Comput. Sci., 99, 141-155 (1992) · Zbl 0769.68084
[22] V.R. Pratt, Semantical considerations on Floyd-Hoare Logic, in: Proc. 17th IEEE Symp. the Foundations of Computer Science, 1976, pp. 109-121.; V.R. Pratt, Semantical considerations on Floyd-Hoare Logic, in: Proc. 17th IEEE Symp. the Foundations of Computer Science, 1976, pp. 109-121.
[23] Robinson, E.; Rosolini, G., Categories of partial maps, Inform. and Comput., 79, 95-130 (1988) · Zbl 0656.18001
[24] Wadler, P., Comprehending monads, Math. Structures Comput. Sci., 2, 461-493 (1992) · Zbl 0798.68040
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.