Clones, closed categories, and combinatory logic

We explain how to recast the semantics of the simply-typed lambda-calculus, and its linear and ordered variants, using multiary structures. We define universal properties for multicategories, and use these to derive familiar rules for products, tensors, and exponentials. Finally we outline how to recover both the category-theoretic syntactic model and its semantic interpretation from the multiary 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.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.