Planar Realizability via Left and Right Applications
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.
Realizability
combinatory algebra
monoidal bi-closed category
exponential modality
exchange modality
Theory of computation~Categorical semantics
35:1-35:17
Regular Paper
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.
Haruka
Tomita
Haruka Tomita
Research Institute for Mathematical Sciences, Kyoto University, Japan
This work was supported by JST ERATO Grant Number JPMJER1603, Japan.
10.4230/LIPIcs.CSL.2022.35
Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science, 12(5):625-665, 2002.
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.
Brian Day. A reflection theorem for closed categories. Journal of pure and applied algebra, 2(1):1-11, 1972.
J Michael Dunn and Robert K Meyer. Combinators and structurally free logic. Logic Journal of IGPL, 5(4):505-537, 1997.
Jean-Yves Girard. Linear logic. Theoretical computer science, 50(1):1-101, 1987.
Masahito Hasegawa. A quantum double construction in Rel. Mathematical Structures in Computer Science, 22(4):618-650, 2012.
Masahito Hasegawa. Linear exponential comonads without symmetry. Electronic Proceedings in Theoretical Computer Science, 238:54-63, 2016.
Naohiko Hoshino. Linear realizability. In International Workshop on Computer Science Logic, pages 420-434. Springer, 2007.
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.
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.
John R Longley. Realizability toposes and language semantics. PhD thesis, University of Edinburgh, 1995.
Oleksandr Manzyuk. Closed categories vs. closed multicategories. Theory and Applications of Categories, 26(5):132-175, 2012.
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.
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.
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.
Noam Zeilberger and Alain Giorgetti. A correspondence between rooted planar maps and normal planar lambda terms. Log. Methods Comput. Sci., 11, 2015.
Haruka Tomita
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode