論文の公開元へPlanar Realizability via Left and Right Applications
概要
Categorical realizability gives us a useful method to construct categorical models of various
logics and programming languages from simple structures called applicative structures. The
most well known is the case of partial combinatory algebras (PCAs), which are an important
class of applicative structures. From a PCA A, we can construct Cartesian closed categories
(CCCs) Asm(A) and Mod(A) and a realizability topos RT(A) [11].
The structures of such categories obtained by realizability depend on the structures of
applicative structures. Thus, assuming other conditions to applicative structures than being
PCAs, we can obtain other categorical structures and use them to model other kinds of
languages. A well known case is a class of applicative structure called BCI-algebras, which
induces a symmetric monoidal closed structure on Asm(A) and Mod(A) [1, 2]. While
PCAs correspond to the untyped lambda calculus by the combinatory completeness property,
BCI-algebras correspond to the untyped linear lambda calculus.
These two cases for PCAs and BCI-algebras are useful to give various models based
on CCCs and symmetric monoidal closed categories (SMCCs). On the other hand, the
categorical realizability giving rise to non-symmetric categorical structures has not been
investigated much. In our previous work [14], several classes of applicative structures that
•
induce certain non-symmetric categorical structures were introduced. The BI(−) -algebra
•
is one of such classes. A BI(−) -algebra A induces the structure of closed multicategories
on Asm(A) and Mod(A), and corresponds to the untyped planar lambda calculus by
combinatory completeness. Here, the planar lambda calculus is the restricted linear lambda
calculus that consists of linear lambda terms whose orders of bound variables can not be freely
exchanged. The name “planar” comes from the fact that planar lambda terms correspond to
graphically planar maps [16, 15].
© Haruka Tomita;
licensed under Creative Commons License CC-BY 4.0
30th EACSL Annual Conference on Computer Science Logic (CSL 2022).
Editors: Florin Manea and Alex Simpson; Article No. 35; pp. ...
