If cartesian closed categories are the model for simply typed lambda calculus, then can it be said that a monoid is a categorical model for untyped lambda calculus?
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
5
$C$-monoids and their variants is what you are looking for. You can find further references and an account of what is what in Martin Hyland's Towards a Notion of Lambda Monoid.
answered Oct 8, 2019 at 8:03
-
$\begingroup$ Thanks for the answer. I'm new to category theory so pardon me if it sounds silly but is C-monoids the same thing as monoidal category? $\endgroup$– al palOct 8, 2019 at 19:46
-
2$\begingroup$ Nope. It's a rather special kind of object in a category whose structure allows you to model $\lambda$-calculus. $\endgroup$ Oct 8, 2019 at 21:07
-
$\begingroup$ Is there any other reference which talks and explains the monodical category other than the reference you mentioned? I couldn't find one on Internet!! $\endgroup$– al palOct 8, 2019 at 21:10
-
2$\begingroup$ $C$-monoids are described in Lambek & Scott's "Introduction to higher-order categorical logic", section 15 $\endgroup$ Oct 8, 2019 at 21:22
-
$\begingroup$ Following is the only thing I found: Möbius polynomial species, Domenico Senato, A. Venezia, J. Yang. Please let me know if there is a more direct reference to such. $\endgroup$– al palOct 8, 2019 at 21:22