Clones, closed categories, and combinatory logic
Philip Saville
TL;DR
This paper addresses the mismatch between contexts in syntax and unary morphisms in category theory by developing a multi-ary semantics based on multimaps $A_1,\dots,A_n \to B$, thereby clarifying the internal language of typed calculi. It formalizes multicategories, clones, and their internal languages, and introduces SK-clones and SK-categories as semantic models for the simply-typed $\lambda$-calculus without products. It proves that extensional SK-clones are sound and complete for combinatory logic with extensional weak equality and for $\Lambda^{\to}_{\mathcal{S}}$ without products, and shows SK-categories are equivalent to closed clones, making the calculus the internal language of SK-categories. A key corollary is that SK-categories have the same relationship to cartesian monoidal categories as closed categories have to monoidal categories, providing a unified semantic framework for $\Lambda^{\times}$, $\Lambda^{\to}$, and their combinations in a product-free setting.
Abstract
We give an exposition of the semantics of the simply-typed lambda-calculus, and its linear and ordered variants, using multi-ary structures. We define universal properties for multicategories, and use these to derive familiar rules for products, tensors, and exponentials. Finally we explain how to recover both the category-theoretic syntactic model and its semantic interpretation from the multi-ary framework. We then use these ideas to study the semantic interpretation of combinatory logic and the simply-typed lambda-calculus without products. We introduce extensional SK-clones and show these are sound and complete for both combinatory logic with extensional weak equality and the simply-typed lambda-calculus without products. We then show such SK-clones are equivalent to a variant of closed categories called SK-categories, so the simply-typed lambda-calculus without products is the internal language of SK-categories. As a corollary, we deduce that SK-categories have the same relationship to cartesian monoidal categories that closed categories have to monoidal categories.