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.

翻译：我们给出了简单类型λ-演算及其线性与有序变体的语义阐释，采用了多元结构。我们定义了多元范畴的泛性质，并利用这些性质推导出关于积、张量积与指数的常见规则。最后，我们阐释了如何从多元框架中恢复范畴论句法模型及其语义解释。进而利用这些思想研究了无积的组合逻辑与简单类型λ-演算的语义解释。我们引入了外延SK-克隆，并证明了它们对具有外延弱等式的组合逻辑与无积的简单类型λ-演算具有可靠性与完备性。随后证明这类SK-克隆等价于一种称为SK-范畴的闭范畴变体，因此无积的简单类型λ-演算正是SK-范畴的内部语言。作为推论，我们推导出SK-范畴与笛卡尔幺半范畴的关系，类同于闭范畴与幺半范畴的关系。