Join inverse categories and reversible recursion. (English) Zbl 1359.68045
Summary: Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily desirable, and certainly not required in order to guarantee reversibility. In a categorical setting, however, faithfully capturing partiality requires handling it as additional structure. Recently, B. G. Giles [An investigation of some theoretical aspects of reversible computing. Calgary: Univ. Calgery (PhD Thesis) (2012)] studied inverse categories as a model of partial reversible (functional) programming. In this paper, we show how additionally assuming the existence of countable joins on such inverse categories leads to a number of properties that are desirable when modeling reversible functional programming, notably morphism schemes for reversible recursion, a \(\dagger\)-trace, and algebraic \(\omega\)-compactness. This gives a categorical account of reversible recursion, and, for the latter, provides an answer to the problem posed by Giles [loc. cit.] regarding the formulation of recursive data types at the inverse category level.
MSC:
| 68N18 | Functional programming and lambda calculus |
| 18C50 | Categorical semantics of formal languages |
| 18D20 | Enriched categories (over closed or monoidal categories) |
| 68Q55 | Semantics in the theory of computing |
| 68Q65 | Abstract data types; algebraic specification |
Software:
TheseusReferences:
| [2] | Axelsen, H. B.; Kaarsgaard, R., Join inverse categories as models of reversible recursion, (Jacobs, B.; Löding, C., Foundations of Software Science and Computation Structures, 19th International Conference, FoSSaCS 2016, Proceedings. Foundations of Software Science and Computation Structures, 19th International Conference, FoSSaCS 2016, Proceedings, Lecture Notes in Computer Science, vol. 9634 (2016), Springer), 73-90 · Zbl 1475.68058 |
| [3] | Landauer, R., Irreversibility and heat generation in the computing process, IBM J. Res. Dev., 5, 3, 183-191 (1961) · Zbl 1160.68305 |
| [4] | Fredkin, E.; Toffoli, T., Conservative logic, Int. J. Theor. Phys., 21, 3-4, 219-253 (1982) · Zbl 0496.94015 |
| [5] | Bennett, C. H., Logical reversibility of computation, IBM J. Res. Dev., 17, 6, 525-532 (1973) · Zbl 0267.68024 |
| [6] | Axelsen, H. B.; Glück, R., What do reversible programs compute?, (Hofmann, M., Foundations of Software Science and Computational Structures, 14th International Conference, FOSSACS 2011, Proceedings. Foundations of Software Science and Computational Structures, 14th International Conference, FOSSACS 2011, Proceedings, Lecture Notes in Computer Science, vol. 6604 (2011), Springer), 42-56 · Zbl 1326.68134 |
| [7] | Kutrib, M.; Wendlandt, M., Reversible limited automata, (Durand-Lose, J.; Nagy, B., Machines, Computations, and Universality, 7th International Conference, MCU 2015, Proceedings. Machines, Computations, and Universality, 7th International Conference, MCU 2015, Proceedings, Lecture Notes in Computer Science, vol. 9288 (2015), Springer), 113-128 · Zbl 1415.68136 |
| [8] | Morita, K., Two-way reversible multihead automata, Fundam. Inform., 110, 1-4, 241-254 (2011) · Zbl 1234.68230 |
| [9] | Schordan, M.; Jefferson, D.; Barnes, P.; Oppelstrup, T.; Quinlan, D., Reverse code generation for parallel discrete event simulation, (Krivine, J.; Stefani, J.-B., Reversible Computation, 7th International Conference, RC 2015, Proceedings. Reversible Computation, 7th International Conference, RC 2015, Proceedings, Lecture Notes in Computer Science, vol. 9138 (2015), Springer), 95-110 · Zbl 1464.68049 |
| [10] | Cristescu, I.; Krivine, J.; Varacca, D., A compositional semantics for the reversible \(π\)-calculus, (LICS 2013 (2013), IEEE Computer Society), 388-397 · Zbl 1366.68201 |
| [11] | Schultz, U. P.; Bordignon, M.; Støy, K., Robust and reversible execution of self-reconfiguration sequences, Robotica, 29, 1, 35-57 (2011) |
| [12] | Schultz, U. P.; Laursen, J. S.; Ellekilde, L.; Axelsen, H. B., Towards a domain-specific language for reversible assembly sequences, (Krivine, J.; Stefani, J.-B., Reversible Computation, 7th International Conference, RC 2015, Proceedings. Reversible Computation, 7th International Conference, RC 2015, Proceedings, Lecture Notes in Computer Science, vol. 9138 (2015), Springer), 111-126 · Zbl 1464.68406 |
| [13] | Yokoyama, T.; Glück, R., A reversible programming language and its invertible self-interpreter, (Partial Evaluation and Program Manipulation. Proceedings (2007), ACM), 144-153 |
| [14] | Yokoyama, T.; Axelsen, H. B.; Glück, R., Fundamentals of reversible flowchart languages, Theor. Comput. Sci., 611, 87-115 (2016) · Zbl 1332.68028 |
| [15] | James, R. P.; Sabry, A., Theseus: A high level language for reversible computing (2014), available at |
| [16] | Bowman, W. J.; James, R. P.; Sabry, A., Dagger traced symmetric monoidal categories and reversible programming, (De Vos, A.; Wille, R., Reversible Computation 2011, Proceedings (2011), Ghent University), 51-56 |
| [17] | Cockett, J. R.B.; Lack, S., Restriction categories I: categories of partial maps, Theor. Comput. Sci., 270, 1-2, 223-259 (2002) · Zbl 0988.18003 |
| [18] | Giles, B. G., An investigation of some theoretical aspects of reversible computing (2014), University of Calgary, Ph.D. thesis |
| [19] | Guo, X., Products, joins, meets, and ranges in restriction categories (2012), University of Calgary, Ph.D. thesis |
| [20] | Haghverdi, E., A categorical approach to linear logic, geometry of proofs and full completeness (2000), Carlton University and University of Ottawa, Ph.D. thesis |
| [21] | Hoshino, N., A representation theorem for unique decomposition categories, (Berger, U.; Mislove, M., MFPS XXVIII. MFPS XXVIII, Electronic Notes in Theoretical Computer Science, vol. 286 (2012), Elsevier), 213-227 · Zbl 1343.03050 |
| [22] | Yokoyama, T.; Axelsen, H. B.; Glück, R., Towards a reversible functional language, (De Vos, A.; Wille, R., Reversible Computation, Third International Workshop, RC 2011, Revised papers. Reversible Computation, Third International Workshop, RC 2011, Revised papers, Lecture Notes in Computer Science, vol. 7165 (2012), Springer), 14-29 · Zbl 1407.68075 |
| [23] | Abramov, S. M.; Glück, R., Principles of inverse computation and the universal resolving algorithm, (Mogensen, T. Æ.; Schmidt, D. A.; Sudborough, I. H., The Essence of Computation: Complexity, Analysis, Transformation. The Essence of Computation: Complexity, Analysis, Transformation, Lecture Notes in Computer Science, vol. 2566 (2002), Springer), 269-295 · Zbl 1026.68023 |
| [24] | Glück, R.; Kawabe, M., Derivation of deterministic inverse programs based on LR parsing, (Kameyama, Y.; Stuckey, P. J., Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Proceedings. Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Proceedings, Lecture Notes in Computer Science, vol. 2998 (2004), Springer), 291-306 · Zbl 1122.68394 |
| [25] | Glück, R.; Kawabe, M., A program inverter for a functional language with equality and constructors, (Ohori, A., Programming Languages and Systems, First Asian Symposium, APLAS 2003, Proceedings. Programming Languages and Systems, First Asian Symposium, APLAS 2003, Proceedings, Lecture Notes in Computer Science, vol. 2895 (2003), Springer), 246-264 · Zbl 1254.68057 |
| [26] | James, R. P.; Sabry, A., Information effects, (Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12 (2012), ACM), 73-84 · Zbl 1321.68267 |
| [27] | Cockett, J. R.B.; Lack, S., Restriction categories II: partial map classification, Theor. Comput. Sci., 294, 1-2, 61-102 (2003) · Zbl 1023.18005 |
| [28] | Cockett, J. R.B.; Lack, S., Restriction categories III: colimits, partial limits and extensivity, Math. Struct. Comput. Sci., 17, 4, 775-817 (2007) · Zbl 1123.18003 |
| [29] | Lawson, M. V., Inverse Semigroups: The Theory of Partial Symmetries (1998), World Scientific · Zbl 1079.20505 |
| [30] | Kastl, J., Inverse categories, (Hoehnke, H.-J., Algebraische Modelle, Kategorien und Gruppoide. Algebraische Modelle, Kategorien und Gruppoide, Studien zur Algebra und Ihre Anwendungen, vol. 7 (1979), Akademie-Verlag), 51-60 · Zbl 0427.18003 |
| [31] | Heunen, C., On the functor \(\ell^2\), (Computation, Logic, Games, and Quantum Foundations - The Many Facets of Samson Abramsky. Computation, Logic, Games, and Quantum Foundations - The Many Facets of Samson Abramsky, Lecture Notes in Computer Science, vol. 7860 (2013), Springer), 107-121 · Zbl 1264.46014 |
| [32] | Robinson, E.; Rosolini, G., Categories of partial maps, Inf. Comput., 79, 95-130 (1988) · Zbl 0656.18001 |
| [33] | Adámek, J., Recursive data types in algebraically \(ω\)-complete categories, Inf. Comput., 118, 181-190 (1995) · Zbl 0841.18003 |
| [34] | Barr, M., Algebraically compact functors, J. Pure Appl. Algebra, 82, 3, 211-231 (1992) · Zbl 0777.18005 |
| [35] | Cockett, J. R.B.; Guo, X., Join restriction categories and the importance of being adhesive (2007), presentation at Category Theory (2007) |
| [36] | Laplaza, M. L., Coherence for distributivity, (Kelly, G. M.; Laplaza, M. L.; Lewis, G.; Mac Lane, S., Coherence in Categories. Coherence in Categories, Lecture Notes in Mathematics, vol. 281 (1972), Springer), 29-65 · Zbl 0244.18010 |
| [37] | Carette, J.; Sabry, A., Computing with semirings and weak rig groupoids, (Thiemann, P., Programming Languages and Systems, 25th European Symposium on Programming, Proceedings. Programming Languages and Systems, 25th European Symposium on Programming, Proceedings, Lecture Notes in Computer Science, vol. 9632 (2016), Springer), 123-148 · Zbl 1335.68048 |
| [38] | Joyal, A.; Street, R.; Verity, D., Traced monoidal categories, Math. Proc. Camb. Philos. Soc., 119, 3, 447-468 (1996) · Zbl 0845.18005 |
| [39] | Abramsky, S., Retracing some paths in process algebra, (Montanari, U.; Sassone, V., CONCUR ’96: Concurrency Theory, 7th International Conference, Proceedings. CONCUR ’96: Concurrency Theory, 7th International Conference, Proceedings, Lecture Notes in Computer Science, vol. 1119 (1996), Springer), 1-17 · Zbl 1514.68153 |
| [40] | Hasegawa, M., Recursion from cyclic sharing: traced monoidal categories and models of cyclic lambda calculi, (de Groote, P.; Hindley, J. R., Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA ’97, Proceedings. Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA ’97, Proceedings, Lecture Notes in Computer Science, vol. 1210 (1997), Springer), 196-213 · Zbl 1063.68599 |
| [41] | Hasegawa, M., Models of sharing graphs (1997), University of Edinburgh, Ph.D. thesis |
| [42] | Hyland, M., Abstract and concrete models for recursion, (Grumberg, O.; Nipkow, T.; Pfaller, C., Proceedings of the NATO Advanced Study Institute on Formal Logical Methods for System Security and Correctness (2008), IOS Press), 175-198 |
| [43] | Selinger, P., A survey of graphical languages for monoidal categories, (Coecke, B., New Structures for Physics. New Structures for Physics, Lecture Notes in Physics, vol. 813 (2011), Springer), 289-355 · Zbl 1217.18002 |
| [44] | Hines, P. M., The algebra of self-similarity and its applications (1998), University of Wales: University of Wales Bangor, Ph.D. thesis |
| [45] | Abramsky, S.; Haghverdi, E.; Scott, P., Geometry of Interaction and linear combinatory algebras, Math. Struct. Comput. Sci., 12, 05, 625-665 (2002) · Zbl 1014.03056 |
| [46] | Manes, E. G.; Benson, D. B., The inverse semigroup of a sum-ordered semiring, Semigroup Forum, 31, 1, 129-152 (1985) · Zbl 0549.06014 |
| [47] | Cockett, R.; Garner, R., Restriction categories as enriched categories, Theor. Comput. Sci., 523, 37-55 (2014) · Zbl 1288.18007 |
| [48] | Fiore, M. P., Axiomatic domain theory in categories of partial maps (1994), University of Edinburgh, Ph.D. thesis |
| [49] | Selinger, P., Finite dimensional Hilbert spaces are complete for dagger compact closed categories, Log. Methods Comput. Sci., 8, 3, 1-12 (2012) · Zbl 1250.18007 |
| [50] | Selinger, P., Idempotents in dagger categories, (Selinger, P., QPL 2006. QPL 2006, Electronic Notes in Theoretical Computer Science, vol. 210 (2008), Elsevier), 107-122 · Zbl 1279.18006 |
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.
