Document Open Access Logo

Planar Realizability via Left and Right Applications

Author Haruka Tomita

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2022.35.pdf
  • Filesize: 0.66 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
Keywords
  • Realizability
  • combinatory algebra
  • monoidal bi-closed category
  • exponential modality
  • exchange modality

Metrics

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

Abstract

We introduce a class of applicative structures called bi-BDI-algebras. Bi-BDI-algebras are generalizations of partial combinatory algebras and BCI-algebras, and feature two sorts of applications (left and right applications). Applying the categorical realizability construction to bi-BDI-algebras, we obtain monoidal bi-closed categories of assemblies (as well as of modest sets). We further investigate two kinds of comonadic applicative morphisms on bi-BDI-algebras as non-symmetric analogues of linear combinatory algebras, which induce models of exponential and exchange modalities on non-symmetric linear logics.

Cite As Get BibTex

Haruka Tomita. Planar Realizability via Left and Right Applications. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CSL.2022.35

Author Details

Haruka Tomita
  • Research Institute for Mathematical Sciences, Kyoto University, Japan

Funding

  • Tomita, Haruka: This work was supported by JST ERATO Grant Number JPMJER1603, Japan.

Acknowledgements

I would like to thank Masahito Hasegawa for a lot of helpful discussions and comments. I am also grateful to Naohiko Hoshino for useful advice. Thanks also to anonymous reviewers for their helpful feedback.

References

  1. Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625-665, 2002. Google Scholar
  2. Samson Abramsky and Marina Lenisa. Linear realizability and full completeness for typed lambda-calculi. Annals of Pure and Applied Logic, 134(2-3):122-168, 2005. Google Scholar
  3. Brian Day. A reflection theorem for closed categories. Journal of pure and applied algebra, 2(1):1-11, 1972. Google Scholar
  4. J Michael Dunn and Robert K Meyer. Combinators and structurally free logic. Logic Journal of IGPL, 5(4):505-537, 1997. Google Scholar
  5. Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987. Google Scholar
  6. Masahito Hasegawa. A quantum double construction in Rel. Mathematical Structures in Computer Science, 22(4):618-650, 2012. Google Scholar
  7. Masahito Hasegawa. Linear exponential comonads without symmetry. Electronic Proceedings in Theoretical Computer Science, 238:54-63, 2016. Google Scholar
  8. Naohiko Hoshino. Linear realizability. In International Workshop on Computer Science Logic, pages 420-434. Springer, 2007. Google Scholar
  9. Jiaming Jiang, Harley Eades III, and Valeria de Paiva. On the lambek calculus with an exchange modality. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018, volume 292 of EPTCS, pages 43-89, 2018. Google Scholar
  10. Joachim Lambek. Deductive systems and categories II. standard constructions and closed categories. In Category theory, homology theory and their applications I, pages 76-122. Springer, 1969. Google Scholar
  11. John R Longley. Realizability toposes and language semantics. PhD thesis, University of Edinburgh, 1995. Google Scholar
  12. Oleksandr Manzyuk. Closed categories vs. closed multicategories. Theory and Applications of Categories, 26(5):132-175, 2012. Google Scholar
  13. Alex Simpson. Reduction in a linear lambda-calculus with applications to operational semantics. In International Conference on Rewriting Techniques and Applications, pages 219-234. Springer, 2005. Google Scholar
  14. Haruka Tomita. Realizability Without Symmetry. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 38:1-38:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  15. Noam Zeilberger. A theory of linear typings as flows on 3-valent graphs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 919-928. ACM, 2018. Google Scholar
  16. Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. Log. Methods Comput. Sci., 11, 2015. Google Scholar
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