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?
$\begingroup$
$\endgroup$
$\begingroup$
$\endgroup$
$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 '19 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 pal Oct 8 '19 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$ – Andrej Bauer Oct 8 '19 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 pal Oct 8 '19 at 21:10
-
2$\begingroup$ $C$-monoids are described in Lambek & Scott's "Introduction to higher-order categorical logic", section 15 $\endgroup$ – Andrej Bauer Oct 8 '19 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 pal Oct 8 '19 at 21:22
