5
$\begingroup$

In "Domains and Lambdi Calculi" by Amadio and Curien, in the section on solving recursive domain equations (section 7), they give sufficient conditions on a cpo-enriched category so that the category of embedding-projection pairs has $\omega$-colimits. Specifically they say it is sufficient for the category to have $\omega^{op}$-limits.

They then have a theorem that the category of CPOs has all $\omega^{op}$ limits, but the proof is incomplete and I don't see how it could be completed.

To be clear in their book the category CPO has as objects directed complete partial orders with a least element and as maps continuous (not neccesarily strict!) functions.

Their proof proceeds as follows. Given a diagram ${D_n,f_n}_{n\in\omega}$ ($f_n : D_{n+1} \to D_n)$, their proposed limit is $$D = \{ \alpha : \Pi_{n\in\omega} D_n | \forall n, f_n(\alpha_{n+1}) = \alpha_{n} \}$$

with the pointwise ordering. This is definitely the product of that diagram in DCPO, but I don't see why $D$ must have a least element. In particular, you can't pick $\alpha_n = \bot_n \in D_n$ since the functions $f_n$ are not assumed to be strict.

However, restricting to strict continuous functions is all they need anyway because embedding-projection pairs of CPOs are strict anyway (embedding because it's a left adjoint, projection because it's a retract of the embedding). However this doesn't seem quite right either because for example a right adjoint wouldn't necessarily have to be strict, so it seems less general.

So to summarize

  1. Is there a way to prove $D$ is a CPO or a concrete counterexample?
  2. If it's not, what is the right way to "fix" to their formula for solving recursive domain equations? Specifically, we do want to limit the construction to a category of CPOs since they have the bottom elements needed for recursive domain equations, but restricting to limits of strict functions seems stronger than necessary (though sufficient for my needs for now).

I know I could go back through Wand and Plotkin and Pitts and probably find the answers to (3) there, but it would be nice to have a succinct general construction like in their book chapter. Specifically I would like a reference that includes Pitt's minimal invariants work (otherwise Abramsky-Jung is probably sufficient).

$\endgroup$
  • 2
    $\begingroup$ Since the category has all products, you can simplify your question to: does it have equalizers? (I think not.) So then the question is whether $\omega^\mathrm{op}$-limits exist "by accident". $\endgroup$ – Andrej Bauer May 27 '17 at 18:49
  • $\begingroup$ In Abramsky&Jung "Domain Theory", the DCPO category is proved complete (not just $\omega$-) in that way, but there a DCPO can have no bottom element. $\endgroup$ – chi May 29 '17 at 15:12
6
$\begingroup$

Here's an attempt (please check!).

We have that $\bot_D = d$, where

$$ d_i = \bigsqcup^{D_i} \{\bot_i,f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),\ldots\} $$

By construction (and monotonicity), the above is the supremum of an $\omega$-chain inside $D_i$, so $d_i$ is well defined.

It is an element of $D$ since, by continuity,

$$ \begin{array}{ll} & f_i(d_{i+1}) \\ = & f_i(\bigsqcup^{D_{i+1}} \{\bot_{i+1},f_{i+1}(\bot_{i+2}),f_{i+1}(f_{i+2}(\bot_{i+3})),\ldots\}) \\ = & \bigsqcup^{D_{i}} \{f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\ = & \bigsqcup^{D_{i}} \{\bot_i, f_i(\bot_{i+1}),f_i(f_{i+1}(\bot_{i+2})),f_i(f_{i+1}(f_{i+2}(\bot_{i+3}))),\ldots\} \\ = & d_i \end{array} $$

To prove that $d$ is the bottom, we take any $x \in D$, and we observe

$$ \begin{array}{ll} & d_i \sqsubseteq x_i \\ \Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq x_i \\ \Leftarrow & \forall k\geq i.\ f_i \circ \cdots \circ f_k(\bot_{k+1}) \sqsubseteq f_i \circ \cdots \circ f_k (x_{k+1})\\ \Leftarrow & \forall k\geq i.\ \bot_{k+1} \sqsubseteq x_{k+1}\\ \Leftarrow & {\sf true} \end{array} $$

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ This proof checks out, and I found the same argument in Smyth-Plotkin's "The Category-Theoretic Solution to Recursive Domain Equations". The key step is that the set of images of _|_s is directed because the diagram is codirected, so the proof immediately generalizes. That's also why the proof doesn't generalize to equalizers, because you won't be able to take the join. $\endgroup$ – Max New May 29 '17 at 16:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.