Not Enough Points Is Enough

Models of the untyped λ-calculus may be defined either as applicative structures satisfying a bunch of first order axioms, known as “λ-models”, or as (structures arising from) any reflexive object in a cartesian closed category (ccc, for brevity). These notions are tightly linked in the sense that: given a λ-model A, one may define a ccc in which A (the carrier set) is a reflexive object; conversely, if U is a reflexive object in a ccc C, having enough points, then C(½, U) may be turned into a λ-model. It is well known that, if C does not have enough points, then the applicative structure C(½, U) is not a λ-model in general. This paper: (i) shows that this mismatch can be avoided by choosing appropriately the carrier set of the λ-model associated with U; (ii) provides an example of an extensional reflexive object D in a ccc without enough points: the Kleisli-category of the comonad “finite multisets” on Rel; (iii) presents some algebraic properties of the λ-mod...

• Type: Conference
• Year: 2007
• Where: CSL
• Authors: Antonio Bucciarelli, Thomas Ehrhard, Giulio Manzonetto
• Keywords: Applicative Structure, CSL 2007, Reflexive Object, first Order Axioms