Clones, closed categories, and combinatory logic

TL;DR

This paper explores the semantics of various typed lambda-calculi using multi-ary structures, introduces SK-clones, and establishes their equivalence to SK-categories, linking syntax and semantics in categorical logic.

Contribution

It introduces extensional SK-clones and demonstrates their equivalence to SK-categories, providing a new categorical framework for understanding typed lambda-calculi.

Findings

SK-clones are sound and complete for combinatory logic and lambda-calculus without products.

SK-clones are equivalent to SK-categories, linking syntax with categorical semantics.

The work establishes a relationship between SK-categories and cartesian monoidal categories.

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.