The typing rules for simply typed lambda calculus
can be seen as defining a family of sets of terms, indexed by context and by type, while the computation rule can be seen as considering the quotient of this family of sets by the axiom (defined in terms of the substitution operation).
But suppose that we collapse all of the types into one “universal” type , so that terms need no longer be simply-typed:
Now, these rules can be seen as defining a family of sets of terms indexed only by the length of the context (corresponding to the number of free variables). Together with the action of substitution and after quotienting by the axiom, this family of sets can then be considered as a cartesian operad defining an algebraic theory of pure lambda calculus terms.
Let be a cartesian operad (i.e., essentially a Lawvere theory). A semi-closed structure (Hyland) on is a family of maps
natural in , which are compatible with the operadic structure in an appropriate sense. A lambda theory is a cartesian operad equiped with a semi-closed structure.
Any lambda theory is isomorphic to the endomorphism lambda theory of a reflexive object in a cartesian closed category. In particular, let be a lambda theory, then for the associated reflexive object we simply take itself, seen as an object of the presheaf category together with its associated ccc structure (see closed monoidal structure on presheaves). We have that the exponential is isomorphic to , and thus a retract of by the semi-closed structure of . Moreover, we have that naturally in .
Last revised on October 19, 2021 at 04:04:13. See the history of this page for a list of all contributions to it.