Clones, closed categories, and combinatory logic
| Autor: | Saville, Philip |
|---|---|
| Rok vydání: | 2024 |
| Předmět: | |
| Zdroj: | In: Kobayashi, N., Worrell, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2024. Lecture Notes in Computer Science, vol 14575. Springer, Cham |
| Druh dokumentu: | Working Paper |
| DOI: | 10.1007/978-3-031-57231-9_8 |
| Popis: | 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. Comment: A slightly-extended version of the paper published at Foundations of Software Science and Computation Structures (FoSSaCS) 2024 |
| Databáze: | arXiv |
| Externí odkaz: |
|