Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion

• Autorzy: Milius S. , Litak T.

Identyfikatory

DOI

10.3233/FI-2017-1475

• Języki publikacji: EN

Abstrakty

EN

Motivated by the recent interest in models of guarded (co-)recursion, we study their equational properties. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Ésik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading, hopefully, towards future description of classifying theories for guarded recursion.

Słowa kluczowe

EN

(co-)recursion; theories of Bloom; theories of Ésik; guarded fixpoint operators

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 3/4
• Strony: 407--449
• Opis fizyczny: Bibliogr. 32 poz., rys.

Twórcy

autor

Milius S.

• Chair for Theoretical Computer Science (Informatik 8), Friedrich-Alexander University Erlangen-Nürnberg, Germany

autor

Litak T.

• Chair for Theoretical Computer Science (Informatik 8), Friedrich-Alexander University Erlangen-Nürnberg, Germany

Bibliografia

• [1] Milner R. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
• [2] Elgot CC. Monadic Computation and Iterative Algebraic Theories. In: Rose HE, Sheperdson JC (eds.), Logic Colloquium’73, volume 80. North-Holland Publishers, Amsterdam, 1975 pp. 175-230. doi: 10.1007/978-1-4613-8177-8\_6.
• [3] Nakano H. A Modality for Recursion. In: LICS. IEEE Computer Society. ISBN 0-7695-0725-5, 2000 pp. 255-266. doi: 10.1109/LICS.2000.855774.
• [4] Nakano H. Fixed-Point Logic with the Approximation Modality and Its Kripke Completeness. In: Kobayashi N, Pierce BC (eds.), TACS, volume 2215 of Lecture Notes in Computer Science. Springer. ISBN 3-540-42736-8, 2001 pp. 165-182. doi: 10.1007/3-540-45500-0\_8.
• [5] Appel AW, Melliès PA, Richards CD, Vouillon J. A very modal model of a modern, major, general type system. In: Hofmann M, Felleisen M (eds.). POPL. ACM. ISBN 1-59593-575-4, 2007 pp. 109-122. doi: 10.1145/1190216.1190235.
• [6] Benton N, Tabareau N. Compiling functional types to relational specifications for low level imperative code. In: Kennedy A, Ahmed A (eds.), TLDI. ACM. ISBN 978-1-60558-420-1, 2009 pp. 3-14. doi: 10.1145/1481861.1481864.
• [7] Krishnaswami NR, Benton N. Ultrametric Semantics of Reactive Programs. In: LICS. IEEE Computer Society, IEEE Computer Society. ISBN 978-0-7695-4412-0, 2011 pp. 257-266. doi: 10.1109/LICS.2011.38.
• [8] Krishnaswami NR, Benton N. A semantic model for graphical user interfaces. In: Chakravarty MMT, Hu Z, Danvy O (eds.), ICFP ACM. ISBN 978-1-4503-0865-6, 2011 pp. 45-57. doi: 10.1145/2034773.2034782.
• [9] Birkedal L, Møgelberg RE, Schwinghammer J, Støvring K. First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. Logical Methods in Computer Science, 2012. 8 (4:1): 1-45. doi: 10.2168/LMCS-8(4:1)2012.
• [10] Birkedal L, Møgelberg RE. Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. In: Proceedings of LICS. 2013 pp. 213-222. doi: 10.1109/LICS.2013.27.
• [11] Atkey R, McBride C. Productive Coprogramming with Guarded Recursion. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP’13. ACM, New York. NY USA. ISBN 978-1-4503-2326-0, 2013 pp. 197-208. doi: 10.1145/2500365.2500597.
• [12] Litak T. Constructive modalities with provability smack. In: Bezhanishvili G (ed.), Leo Esakia on duality in modal and intuitionistic logics, volume 4 of Outstanding Contributions to Logic, pp. 179-208. Springer, 2014. doi: 10.1007/978-94-017-8860-l\_8. Author’s Cut at https://www8.cs.fau.de/ext/litak/esakiaarxivfull.pdf.
• [13] Di Gianantonio P, Miculan M. Unifying Recursive and Co-recursive Definitions in Sheaf Categories. In: Walukiewicz I (ed.), Foundations of Software Science and Computation Structures, volume 2987 of Lecture Notes in Computer Science, pp. 136-150. Springer Berlin / Heidelberg. ISBN 978-3-540-21298-0, 2004. doi: 10.1007/978-3-540-24727-2\_11.
• [14] Bloom SL, Ésik Z. Iteration Theories: the equational logic of iterative processes. EATCS Monographs on Theoretical Computer Science. Springer, 1993. doi: 10.1007/978-3-642-78034-9.
• [15] Simpson A, Plotkin GD. Complete axioms for categorical fixed-point operators. In: Proc. 15th Symposium on Logic in Computer Science (LICS’00). IEEE Computer Society, 2000 pp. 30-41. doi: 10.1109/LICS.2000.855753.
• [16] Crole RL, Pitts AM. New Foundations for Fixpoint Computations: FIX-Hyperdoctrines and FIX-Logic. Inform. and Comput., 1992. 98 (2): 171-210. doi: 10.1016/0890-5401(92)90018-B.
• [17] Hasegawa M. Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi. In: Proc. 3rd International Conference on Typed Lambda Calculi and Applications, volume 1210 of Lecture Notes Comput. Sci. Springer-Verlag, 1997 pp. 196-213. doi: 10.1007/3-540-62688-3\_37.
• [18] Joyal A, Street R, Verity D. Traced Monoidal Categories. Math. Proc. Cambridge Philos. Soc., 1996. 119 (3): 447-468. doi: 10.1017/S0305004100074338.
• [19] Milius S, Litak T. Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion. In: Baelde D, Carayol A (eds.), Proc. Fixed Points in Computer Science (FICS’13), Electron. Proc. Theoret. Comput. Sci. 2013 pp. 72-86. doi: 10.4204/eptcs.126.6.
• [20] Hasegawa M. Models of Sharing Graphs: A Categorical Semantics of let and letrec. Distinguished Dissertation Series. Springer, 1999. doi: 10.1007/978-l-4471-0865-8.
• [21] Crole RL. Programming Metalogics with a Fixpoint Type. Phd thesis, Computer Laboratory, University of Cambridge, 1991.
• [22] Manes EG. Handbook of Algebra, volume 3, chapter Monads of Sets, pp. 67-153. Elsevier, 2003. doi: 10.1016/s1570-7954(03)80059-1.
• [23] Elgot CC, Bloom SL, Tindell R. On the algebraic structure of rooted trees. J. Comput. System Sci., 1978. 16: 362-399. doi: 10.1007/978-1-4613-8177-8\_7.
• [24] Milius S. Completely Iterative Algebras and Completely Iterative Monads. Inform. and Comput., 2005. 196: 1-41. doi: 10.1016/j.ic.2004.05.003.
• [25] Badouel E. Terms and infinite trees as monads over a signature. Lecture Notes Comput. Sci., 1989. 351: 89-103. doi: 10.1007/3-540-50939-9\_l26.
• [26] Aczel P, Adámek J, Milius S, Velebil J. Infinite Trees and Completely Iterative Theories: A Coalgebraic View. Theoret. Comput. Sci., 2003. 300: 1-45. doi: 10.1016/S0304-3975(02)00728-4.
• [27] Adámek J, Milius S. Terminal Coalgebras and Free Iterative Theories. Inform. and Comput., 2006. 204: 1139-1172. doi: 10.1016/j.ic.2005.11.005.
• [28] Mulry PS. Lifting Theorems for Kleisli Categories. In: Brookes S, Main M, Melton A, Mislove M, Schmidt D (eds.), Proc. Mathematical Foundations of Programming Semantics (MFPS’93), volume 802 of Lecture Notes Comput. Sci. Springer, 1994 pp. 304-319. doi: 10.1007/3-540-58027-1\_15.
• [29] Ésik Z. Independence of the Equational Axioms for Iteration Theories. J. Comput. System Sci., 1988. 36: 66-76. doi: 10.1016/0022-0000(88)90020-7.
• [30] Stefanescu G. On Flowchart Theories. I. The Deterministic Case. J. Comput. Syst. Sci., 1987. 35 (2): 163-191. doi: 10.1016/0022-0000(87)90011-0.
• [31] Ésik Z. Fixed Point Theory. In: Droste M, Kuich W, Vogler H (eds.), Handbook of Weighted Automata, Monographs in Theoretical Computer Science. An EATCS Series, pp. 29-65. Springer Berlin Heidelberg. ISBN 978-3-642-01491-8, 2009. doi: 10.1007/978-3-642-01492-5\_2.
• [32] Gilbert WS, Sullivan A. The Pirates of Penzance, or The Slave of Duty, 1879. See: https://en.wikisource.org/w/index.php?title=The_Pirates_of_Penzance&oldid=5456948.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).