■ Note. A new preprint on powerdomains in synthetic domain theory [powerdomains-synthetic-domain-theory-note]

I finally got around to uploading the preprint with Taro Sekiyama on powerdomains in synthetic domain theory. This is a follow up on Phoa and Taylor’s work on the synthetic Plotkin powerdomain, where the convex/Plotkin powerdomain is constructed by taking the synthetic predomain reflection of the free semilattice on a type. I realized this approach can be quite simply extended to account for the upper and lower powerdomains if one writes down the expected axioms ($𝑆\vee 𝑇\subseteq 𝑇$ and $𝑆\subseteq 𝑆\vee 𝑇$, respectively) in terms of the path order of predomains.

These synthetic powerdomains are computationally adequate for a nondeterministic extension of PCF. I particularly enjoyed understanding the obtuse-looking adequacy statements found in the usual accounts. In contrast to keeping in one’s mind the definition of powerdomains qua “subsets of subsets”, the synthetic construction forces one to look only at the universal properties of the various powerdomains, which evince canonical notions of observation at base type corresponding to may and must termination that made the respective notions of adequacy quite intuitive.