This entry is about a notion of reflexivity in cartesian closed categories of relevance in the categorical semantics of lambda calculus. For the notion of reflexive weak dual objects in closed monoidal categories see there.
A reflexive object is a model of the pure (untyped) lambda calculus validating the law, and sometimes also the law.
A reflexive object in a cartesian closed category is an object equipped with a pair of morphisms
(where denotes the exponential object) such that .
In other words, a reflexive object is an object together with data exhibiting as a retract of .
A reflexive object is said to be extensional (or “strict”) when also , so that there is an isomorphism .
Viewed as a model of lambda calculus, the equation of a reflexive object represents -equality , while the equation of an extensional reflexive object represents -equality .
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 by the internal hom . 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?.
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 . Then the counit of the adjunction models beta-reduction , while the unit models eta-expansion .
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.
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 “” model is built by a limit construction, starting from an arbitrary algebraic lattice, and taking .
Scott later gave a more concrete model of lambda calculus in Scott (1976), defining a reflexive object with carrier the lattice of all subsets of the non-negative integers, and with the maps and (there called “fun” and “graph”) defined as follows:
Here stands for the set whose elements are the exponents in the binary expansion of (thus is the th subset in the standard enumeration of finite subsets of ), while “” stands for the standard enumeration of pairs of integers
Note that the enumeration operator model is not “extensional” in the sense that it only validates -conversion as an inclusion , which is not an equality in general.
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 such that one can prove , and whose morphisms are (equivalence classes of) closed terms such that one can prove (cf. Karoubi envelope), with identity and composition defined by
This category is cartesian closed, where products and exponentials are defined (on objects) by
Now, the identity term lives inside this category since obviously , and moreover, every object is a retract of , since and and . Thus, equipped with its retraction from is a reflexive object.
A more abstract analysis of Scott’s representation theorem appears in Hyland (2013).
Another way of looking at the free cartesian closed category containing a reflexive object is as a representation of pure lambda terms (up to -equality) in the style of so-called higher-order abstract syntax. The operation is the curried form of application, while the operation represents lambda abstraction. The global elements of can be interpreted as closed lambda terms, and more generally, morphisms can be interpreted as terms with free variables.
Dana Scott’s original work on lattice models of the lambda calculus can be found in:
Dana S. Scott, Outline of a mathematical theory of computation, in: Proceedings of the Fourth Annual Princeton Conference on Information Sciences and Systems (1970) 169–176. [pdf, pdf]
Dana Scott. Continuous Lattices. Toposes, Algebraic Geometry and Logic (ed.: E. Lawvere), pages 97-136, Lecture Notes in Mathematics, vol 274. 1972. doi:10.1007/BFb0073967 (pdf)
Dana Scott, Data types as lattices. SIAM Journal of Computing 5 3 (1976) 522–587 [doi:10.1137/0205037, 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:
For a modern analysis of Scott’s representation theorem, see:
Martin Hyland. Classical lambda calculus in modern dress Mathematical Structures in Computer Science, 27(5) (2017) 762-781. doi:10.1017/S0960129515000377. arxiv:1211.5762
Martin Hyland, Towards a Notion of Lambda Monoid , Electronic Notes in Theoretical Computer Science 303 (2014) pp.59-77, doi:10.1016/j.entcs.2014.02.004
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, in: M. Bezem and J.F. Groote (eds.) Typed Lambda Calculi and Applications, Springer
LNCS 664, 1993, p. 195-208 (doi:10.1007/BFb0037107)
Noam Zeilberger, Linear lambda terms as invariants of rooted trivalent maps, Journal of Functional Programming, 26, e21 2016 (doi:10.1017/S095679681600023X, arXiv:1512.06751)
Last revised on September 21, 2023 at 09:36:35. See the history of this page for a list of all contributions to it.