nLab lambda theory

Idea

The typing rules for simply typed lambda calculus

Γt:στΓu:σΓt(u):τΓ,x:σt:τΓλx.t:στ \frac{\Gamma \vdash t: \sigma\to \tau \quad \Gamma \vdash u:\sigma}{\Gamma \vdash t(u) : \tau} \qquad \frac{\Gamma,x:\sigma \vdash t:\tau}{\Gamma \vdash \lambda x.t : \sigma \to \tau}

can be seen as defining a family of sets of terms, indexed by context and by type, while the computation rule (λx.t)u=t[u/x](\lambda x.t)u = t[u/x] can be seen as considering the quotient of this family of sets by the β\beta axiom (defined in terms of the substitution operation).

But suppose that we collapse all of the types into one “universal” type UU, so that terms need no longer be simply-typed:

Γt:UΓu:UΓt(u):UΓ,x:Ut:UΓλx.t:U \frac{\Gamma \vdash t: U \quad \Gamma \vdash u: U}{\Gamma \vdash t(u) : U} \qquad \frac{\Gamma,x: U \vdash t: U}{\Gamma \vdash \lambda x.t:U}

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 β\beta axiom, this family of sets can then be considered as a cartesian operad defining an algebraic theory of pure lambda calculus terms.

Definition

Let L:FinSetL : Fin \to Set be a cartesian operad (i.e., essentially a Lawvere theory). A semi-closed structure (Hyland) on LL is a family of maps

ρ:L(n)L(n+1)λ:L(n+1)L(n)\rho : L(n) \to L(n+1) \quad \lambda : L(n+1) \to L(n)
ρλ=id\rho \circ \lambda = id

natural in nn, which are compatible with the operadic structure in an appropriate sense. A lambda theory is a cartesian operad equiped with a semi-closed structure.

Scott’s representation theorem

Any lambda theory is isomorphic to the endomorphism lambda theory of a reflexive object in a cartesian closed category. In particular, let LL be a lambda theory, then for the associated reflexive object U UUU^U \lhd U we simply take U=LU = L itself, seen as an object of the presheaf category [Fin,Set][Fin,Set] together with its associated ccc structure (see closed monoidal structure on presheaves). We have that the exponential U UU^U is isomorphic to L(+1)L(-+1), and thus a retract of UU by the semi-closed structure of LL. Moreover, we have that [Fin,Set](U n,U)L(n)[Fin,Set](U^n,U) \cong L(n) naturally in nn.

References

Last revised on October 19, 2021 at 04:04:13. See the history of this page for a list of all contributions to it.