Document Open Access Logo

On Compositionality of Dinatural Transformations

Authors Guy McCusker , Alessio Santamaria

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2018.33.pdf
  • Filesize: 0.57 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Proof theory
Keywords
  • Dinatural transformation
  • categorical logic
  • compositionality

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Natural transformations are ubiquitous in mathematics, logic and computer science. For operations of mixed variance, such as currying and evaluation in the lambda-calculus, Eilenberg and Kelly's notion of extranatural transformation, and often the even more general dinatural transformation, is required. Unfortunately dinaturals are not closed under composition except in special circumstances. This paper presents a new sufficient condition for composability. 
We propose a generalised notion of dinatural transformation in many variables, and extend the Eilenberg-Kelly account of composition for extranaturals to these transformations. Our main result is that a composition of dinatural transformations which creates no cyclic connections between arguments yields a dinatural transformation. 
We also extend the classical notion of horizontal composition to our generalized dinaturals and demonstrate that it is associative and has identities.

Cite As Get BibTex

Guy McCusker and Alessio Santamaria. On Compositionality of Dinatural Transformations. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 33:1-33:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.33

Author Details

Guy McCusker
  • University of Bath, United Kingdom
Alessio Santamaria
  • University of Bath, United Kingdom

Funding

  • McCusker, Guy: The author acknowledges the support of EPSRC grant EP/K033042/1.
  • Santamaria, Alessio: The author acknowledges the support of an EPSRC Doctoral Training Partnership studentship at the University of Bath.

References

  1. E. S. Bainbridge, P. J. Freyd, A. Scedrov, and P. J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35-64, 1990. URL: http://dx.doi.org/10.1016/0304-3975(90)90151-7.
  2. R. Blute. Linear logic, coherence and dinaturality. Theoretical Computer Science, 115(1):3-41, 1993. URL: http://dx.doi.org/10.1016/0304-3975(93)90053-V.
  3. J. Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, volume 47 of Lecture Notes in Mathematics, pages 1-77. Springer, Berlin, Heidelberg, 1967. URL: http://dx.doi.org/10.1007/BFb0074299.
  4. E. Dubuc and Ross Street. Dinatural transformations. In S. Mac Lane, H. Applegate, M. Barr, B. Day, E. Dubuc, A. P. Phreilambud, R. Street, M. Tierney, and S. Swierczkowski, editors, Reports of the Midwest Category Seminar IV, volume 137 of Lecture Notes in Mathematics, pages 126-137. Springer, Berlin, Heidelberg, 1970. URL: http://dx.doi.org/10.1007/BFb0060443.
  5. S. Eilenberg and G. M. Kelly. A generalization of the functorial calculus. Journal of Algebra, 3(3):366-375, 1966. URL: http://dx.doi.org/10.1016/0021-8693(66)90006-8.
  6. P. J. Freyd, E. P. Robinson, and G. Rosolini. Dinaturality for free. In A. M. Pitts, M. P. Fourman, and P. T. Johnstone, editors, Applications of Categories in Computer Science: Proceedings of the London Mathematical Society Symposium, Durham 1991, London Mathematical Society Lecture Note Series, pages 107-118. Cambridge University Press, Cambridge, 1992. URL: http://dx.doi.org/10.1017/CBO9780511525902.007.
  7. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, jan 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  8. J.-Y. Girard, A. Scedrov, and P. J. Scott. Normal Forms and Cut-Free Proofs as Natural Transformations. In N. M. Yiannis, editor, Logic from Computer Science, volume 21 of Mathematical Sciences Research Institute Publications, pages 217-241. Springer, New York, NY, 1992. URL: http://dx.doi.org/10.1007/978-1-4612-2822-6_8.
  9. A. Guglielmi and T. Gundersen. Normalisation Control in Deep Inference via Atomic Flows. Logical Methods in Computer Science, 4(1), 2008. URL: http://dx.doi.org/10.2168/LMCS-4(1:9)2008.
  10. A. Guglielmi, T. Gundersen, and L. Straßburger. Breaking Paths in Atomic Flows for Classical Logic. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 284-293, jul 2010. URL: http://dx.doi.org/10.1109/LICS.2010.12.
  11. K. Hiraishi and A. Ichikawa. A Class of Petri Nets That a Necessary and Sufficient Condition for Reachability is Obtainable. Transactions of the Society of Instrument and Control Engineers, 24(6):635-640, 1988. URL: http://dx.doi.org/10.9746/sicetr1965.24.635.
  12. G. M. Kelly. An abstract approach to coherence. In G. M. Kelly, M. Laplaza, G. Lewis, and S. Mac Lane, editors, Coherence in Categories, volume 281 of Lecture Notes in Mathematics, pages 106-147. Springer, Berlin, Heidelberg, 1972. URL: http://dx.doi.org/10.1007/BFb0059557.
  13. G. M. Kelly. Many-variable functorial calculus. I. In G. M. Kelly, M. Laplaza, G. Lewis, and S. Mac Lane, editors, Coherence in Categories, volume 281 of Lecture Notes in Mathematics, pages 66-105. Springer, Berlin, Heidelberg, 1972. URL: http://dx.doi.org/10.1007/BFb0059556.
  14. G. M. Kelly and S. MacLane. Coherence in closed categories. Journal of Pure and Applied Algebra, 1(1):97-140, jan 1971. URL: http://dx.doi.org/10.1016/0022-4049(71)90013-2.
  15. S. MacLane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 2 edition, 1978. URL: https://www.springer.com/gb/book/9780387984032.
  16. P. S. Mulry. Categorical fixed point semantics. Theoretical Computer Science, 70(1):85-97, jan 1990. URL: http://dx.doi.org/10.1016/0304-3975(90)90154-A.
  17. T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-580, 1989. URL: http://dx.doi.org/10.1109/5.24143.
  18. C. A. Petri. Kommunikation mit Automaten. PhD thesis, Mathematisches Institut der Universität Bonn, Bonn, 1962. OCLC: 258511501. Google Scholar
  19. P. Selinger. A Survey of Graphical Languages for Monoidal Categories. In B. Coecke, editor, New Structures for Physics, volume 813 of Lecture Notes in Physics, pages 289-355. Springer, Berlin, Heidelberg, 2010. URL: http://dx.doi.org/10.1007/978-3-642-12821-9_4.
  20. A. K. Simpson. A characterisation of the least-fixed-point operator by dinaturality. Theoretical Computer Science, 118(2):301-314, 1993. URL: http://dx.doi.org/10.1016/0304-3975(93)90112-7.
  21. G. Stremersch and R. K. Boel. Structuring Acyclic Petri Nets for Reachability Analysis and Control. Discrete Event Dynamic Systems, 12(1):7-41, jan 2002. URL: http://dx.doi.org/10.1023/A:1013331703036.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact