nLab
reflexive object

Contents

Idea

A reflexive object is a model of the pure (untyped) lambda calculus validating the β\beta law, and sometimes also the η\eta law.

Definition

A reflexive object in a cartesian closed category is an object UU equipped with a pair of maps

U lamapp U U \array{U & \overset{app}{\underset{lam}{\rightleftarrows}} & U^U}

such that applam=1app \circ lam = 1. In other words, a reflexive object is an object UU together with data U UUU^U \lhd U exhibiting U UU^U as a retract of UU. A reflexive object is said to be extensional (or “strict”) when also lamapp=1lam \circ app = 1, so that there is an isomorphism U UUU^U \cong U.

Viewed as a model of lambda calculus, the equation applam=1app \circ lam = 1 of a reflexive object represents β\beta-equality (λx.t)(u)=t[u/x](\lambda x.t)(u) = t[u/x], while the equation lamapp=1lam \circ app = 1 of an extensional reflexive object represents η\eta-equality λx.t(x)=t\lambda x.t(x) = t.

In a closed (symmetric) monoidal category

The definition has a straightforward generalization to any symmetric monoidal closed category (i.e., not necessarily cartesian monoidal), where we just replace the exponential object U UU^U by the internal hom [U,U][U,U]. Indeed, the definition also makes sense in any left-closed or right-closed monoidal category.

A reflexive object in a symmetric monoidal closed category provides a model of linear lambda calculus?.

In a closed monoidal 2-category

The definition of reflexive object also has a natural generalization to any closed monoidal 2-category (or cartesian closed 2-category), where the retraction should be replaced by an adjunction applam:[U,U]Uapp \dashv lam : [U,U] \to U. Then the counit of the adjunction applam1 [U,U]app \circ lam \Rightarrow 1_{[U,U]} models beta-reduction (λx.t)(u)t[u/x](\lambda x.t)(u) \to t[u/x], while the unit 1 Ulamapp1_U \Rightarrow lam \circ app models eta-expansion tλx.t(x)t \to \lambda x.t(x).

Examples

Terminal object

The terminal object of a ccc provides a degenerate example of a (extensional) reflexive object, and for cardinality reasons, this is the only reflexive object in Set.

Scott’s D D_\infty construction

The first non-degenerate model of untyped lambda calculus was described by Dana Scott (see Scott (1970) and Scott (1972)), who solved the cardinality issue by replacing sets with algebraic lattices, and arbitrary set-theoretic functions by Scott-continuous functions. The so-called “D D_\infty” model is built by a limit construction, starting from D 0=DD_0 = D an arbitrary algebraic lattice, and taking D n+1=D nD nD_{n+1} = D_n \to D_n.

Enumeration operator model

Scott later gave a more concrete model of lambda calculus in Scott (1976), defining a reflexive object with carrier the lattice PωP\omega of all subsets of the non-negative integers, and with the maps appapp and lamlam (there called “fun” and “graph”) defined as follows:

app(u)(x)={me nx.(n,m)u}app(u)(x) = \{m \mid \exists e_n \subseteq x. (n,m) \in u\}
lam(f)={(n,m)mf(e n)}lam(f) = \{(n,m) \mid m \in f(e_n)\}

Here e ne_n stands for the set whose elements are the exponents in the binary expansion of nn (thus e ne_n is the nnth subset in the standard enumeration of finite subsets of ω\omega), while “(n,m)(n,m)” stands for the standard enumeration of pairs of integers

(n,m)=12(n+m)(n+m+1)+m(n,m) = \frac{1}{2}(n+m)(n+m+1)+m

Note that the enumeration operator model is not “extensional” in the sense that it only validates η\eta-conversion as an inclusion u(a(u))u \subseteq \ell(a(u)), which is not an equality in general.

Scott’s representation theorem

Scott (1980) proved a sort of representation theorem for pure lambda calculus, showing that any “type-free theory” (a.k.a., lambda theory) can be realized as a reflexive object. He began by constructing a category whose objects are the closed lambda terms AA such that one can prove A=λx.A(A(x))A = \lambda x.A(A(x)), and whose morphisms f:ABf : A \to B are (equivalence classes of) closed terms ff such that one can prove f=λx.B(f(A(x)))f = \lambda x.B(f(A(x))) (cf. Karoubi envelope), with identity and composition defined by

1 A=Afg=λx.f(g(x)) 1_A = A \qquad f \circ g = \lambda x.f(g(x))

This category is cartesian closed, where products and exponentials are defined (on objects) by

A×B=λuλz.z(A(u(λxλy.x)))(B(u(λxλy.y)))AB=λf.BfA A \times B = \lambda u\lambda z.z(A(u(\lambda x\lambda y.x)))(B(u(\lambda x\lambda y.y))) \qquad A \to B = \lambda f.B \circ f \circ A

Now, the identity term U=λx.xU = \lambda x.x lives inside this category since obviously U=UUU = U\circ U, and moreover, every object AA is a retract of UU, since A:AUA : A \to U and A:UAA : U \to A and AA=A=1 AA \circ A = A = 1_A. Thus, UU equipped with its retraction from UUU \to U is a reflexive object.

A more abstract analysis of Scott’s representation theorem appears in Hyland (2013).

Higher-order abstract syntax

Another way of looking at the free cartesian closed category containing a reflexive object is as a representation of pure lambda terms (up to β\beta-equality) in the style of so-called higher-order abstract syntax. The operation app:UU Uapp : U \to U^U is the curried form of application, while the operation lam:U UUlam : U^U \to U represents lambda abstraction. The global elements of UU can be interpreted as closed lambda terms, and more generally, morphisms U nUU^n \to U can be interpreted as terms with nn free variables.

References

Dana Scott’s original work on lattice models of the lambda calculus can be found in:

  • Dana Scott. Outline of a Mathematical Theory of Computation. In 4th Annual Princeton Conference on Information Sciences and Systems, pages 169-176, 1970. (pdf)

  • Dana Scott. Continuous Lattices. Toposes, Algebraic Geometry and Logic (ed.: E. Lawvere), pages 97-136, 1972. (pdf)

  • Dana Scott. Data types as lattices. SIAM Journal of Computing, 5(3):522–587, September 1976. (pdf)

Scott made the underlying categorical structure explicit in a later paper, where he introduced the definition of a reflexive object in a ccc, and proved a representation theorem for theories of pure lambda calculus:

  • Dana Scott. Relating theories of the λ\lambda-calculus. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism (eds. Hindley and Seldin), Academic Press, 403–450, 1980.

For a modern analysis of Scott’s representation theorem, see:

  • Martin Hyland. Classical lambda calculus in modern dress. To appear in Mathematical Structures in Computer Science, 2013. arxiv

  • Martin Hyland, Towards a Notion of Lambda Monoid , Electronic Notes in Theoretical Computer Science 303 (2014) pp.59-77.

Bicategorical and monoidal generalizations of the notion of reflexive object are discussed in:

  • R. A. G. Seely. Modelling Computations : a 2-categorical Framework. LICS 1987. (pdf)

  • Bart Jacobs. Semantics of lambda-I and of other substructure lambda calculi. M. Bezem and J.F. Groote (eds.) Typed Lambda Calculi and Applications, Springer LNCS 664, 1993, p. 195-208.

  • Noam Zeilberger. Linear lambda terms as invariants of rooted trivalent maps. 31 Jan 2016. (arXiv)

Last revised on June 28, 2017 at 07:58:18. See the history of this page for a list of all contributions to it.