Short answer
No. In the twenty-odd years since the handbook chapter appeared the “adjunction–version’’ of the limit/colimit–coincidence theorem has never been needed in published work on the denotational semantics of programming languages. All semantic applications that rely on limit/colimit coincidence – recursive‐domain equations for PCF, fully-abstract game models, models for references, concurrency etc. – continue to use the original form of the theorem for ω-chains of embedding–projection pairs (retractions). Whenever identifications of points are required, authors still prefer to take an explicit quotient of the final object rather than to let the identifications happen stage-by-stage by means of non-injective lower adjoints.
A little more detail
Recursive domain equations
• The constructions of Smyth & Plotkin (1982), Abramsky (1991), Pitts (1996), Simpson (1998) and others all use ω-chains of embeddings and their projections.
• The more general adjunction version is mentioned for completeness in a couple of places (e.g. Simpson, “Recursive Domain Equations and Inductive Types’’, 1998, §6), but each time the subsequent semantic development re-specialises to retractions.
Game semantics
• Models for PCF, Idealised Algol, call/cc, references, concurrency, etc. (Hyland–Ong, Abramsky–McCusker, Laird, Honda–Yoshida–Berger, Murawski, etc.) are all built as direct–inverse limits along injective inclusions of arenas or strategies.
• None of these constructions allows strategies that are later identified via non-injective maps; when quotienting is required it is done once, at the end (observational equivalence).
Other semantic settings
• Metric models/guarded recursion (Nakano, Appel–Nanevski–Schwinghammer, Birkedal et al.), presheaf models for names (Fiore–Pitts, Stark, Ghica–Murawski), and nominal‐set semantics again do not use the adjunction generalisation.
• Outside programming-language semantics the theorem has been rediscovered in categorical form (ω-bilimits of adjunctions, Adámek–Rosický, Lack–Velebil), but these papers are concerned with general category theory rather than language models.
Why it has not been used
• In most semantic constructions the approximation order is intensional: information can be added but not retracted.
• If one really needs to identify points (e.g. to quotient by observational equivalence) it is technically simpler to form a quotient of the final object rather than to carry identification information through the whole inductive sequence.
• Allowing information to disappear along the chain breaks several standard proof techniques (induction on the approximation level, admissibility of predicates, etc.), so there has never been an incentive to abandon e-p pairs.
So the situation Abramsky and Jung reported in 1994 still holds: the more general limit/colimit coincidence theorem for Scott-continuous adjunctions is mathematically elegant, but it has not found any concrete application in denotational semantics.
Was this answer helpful?
version: o3-2025-04-16
Status: UQ Validated
Validated: 8 months ago
Status: Needs Human Verification
Loading model reviews...
Loading reviews...