Clones, closed categories, and combinatory logic
<|reference_start|>Clones, closed categories, and combinatory logic: 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.<|reference_end|>
@article{saville2024clones,,
    title={Clones, closed categories, and combinatory logic},
    author={Philip Saville},
    journal={In: Kobayashi, N., Worrell, J. (eds) Foundations of Software
  Science and Computation Structures. FoSSaCS 2024. Lecture Notes in Computer
  Science, vol 14575. Springer, Cham},
    year={2024},
    doi={10.1007/978-3-031-57231-9_8},
    archivePrefix={arXiv},
    eprint={2405.01675},
    primaryClass={cs.LO math.CT}
}