A categorical foundation for structured reversible flowchart languages: Soundness and adequacy

Preprint English OPEN
Glück, Robert ; Kaarsgaard, Robin (2017)
  • Related identifiers: doi: 10.23638/LMCS-14(3:16)2018
  • Subject: Mathematics - Category Theory | Computer Science - Programming Languages | D.3.1 | F.3.2
    arxiv: Computer Science::Programming Languages

Structured reversible flowchart languages is a class of imperative reversible programming languages allowing for a simple diagrammatic representation of control flow built from a limited set of control flow structures. This class includes the reversible programming language Janus (without recursion), as well as more recently developed reversible programming languages such as R-CORE and R-WHILE. In the present paper, we develop a categorical foundation for this class of languages based on inverse categories with joins. We generalize the notion of extensivity of restriction categories to one that may be accommodated by inverse categories, and use the resulting decisions to give a reversible representation of predicates and assertions. This leads to a categorical semantics for structured reversible flowcharts, which we show to be computationally sound and adequate, as well as equationally fully abstract with respect to the operational semantics under certain conditions.
  • References (32)
    32 references, page 1 of 4

    [1] Abramov, S. M. and R. Glu¨ck, The universal resolving algorithm: inverse computation in a functional language, in: R. Backhouse and J. N. Oliveira, editors, Mathematics of Program Construction. Proceedings, LNCS 1837 (2000), pp. 187-212.

    [2] Axelsen, H. B. and R. Glu¨ck, What do reversible programs compute?, in: M. Hofmann, editor, Foundations of Software Science and Computation Structures. Proceedings, Lecture Notes in Computer Science 6604 (2011), pp. 42-56.

    [3] Axelsen, H. B., R. Glu¨ck and T. Yokoyama, Reversible machine code and its abstract processor architecture, in: V. Diekert, M. V. Volkov and A. Voronkov, editors, Computer Science - Theory and Applications. Proceedings, Lecture Notes in Computer Science 4649 (2007), pp. 56-69.

    [4] Axelsen, H. B. and R. Kaarsgaard, Join inverse categories as models of reversible recursion, in: B. Jacobs and C. L¨oding, editors, FOSSACS 2016, Proceedings, number 9634 in LNCS (2016), pp. 73-90.

    [5] Carboni, A., S. Lack and R. F. C. Walters, Introduction to extensive and distributive categories, Journal of Pure and Applied Algebra 84 (1993), pp. 145 - 158.

    [6] Carothers, C. D., K. S. Perumalla and R. M. Fujimoto, Efficient optimistic parallel simulations using reverse computation, ACM Trans. Model. Comput. Simul. 9 (1999), pp. 224-253.

    [7] Cockett, J. R. B., Itegories & PCAs (2007), slides from talk at FMCS 2007.

    [8] Cockett, J. R. B. and S. Lack, Restriction categories I: Categories of partial maps, Theoretical Computer Science 270 (2002), pp. 223-259.

    [9] Cockett, J. R. B. and S. Lack, Restriction categories II: Partial map classification, Theoretical Computer Science 294 (2003), pp. 61-102.

    [10] Cockett, R. and S. Lack, Restriction categories III: Colimits, partial limits and extensivity, Mathematical Structures in Computer Science 17 (2007), pp. 775-817.

  • Similar Research Results (3)
  • Metrics
    No metrics available
Share - Bookmark