The Scott model of PCF in univalent type theory

TL;DR

This paper constructs the Scott model of PCF within univalent type theory, demonstrating that partiality can be modeled constructively and predicatively using the lifting monad, avoiding choice or quotient inductive types.

Contribution

It develops a constructive, predicative Scott model of PCF in univalent type theory using the lifting monad, avoiding additional axioms or complex type constructions.

Findings

Lifting monad effectively models partiality in univalent type theory.

Constructive and predicative Scott model of PCF is achievable.

Avoids reliance on choice or quotient inductive-inductive types.

Abstract

We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escard\'o and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.

Equations

$$\mathrm{pred}\underline{0}▹\underline{0};\mathrm{pred}\underline{n+1}▹\underline{n};\mathrm{ifz}st\underline{0}▹s;\mathrm{ifz}st\underline{n+1}▹t;\mathrm{fix}f▹f(\mathrm{fix}f).$$

$$X$$

$$\mathsf{iter}(n)(f):\text{mspace}-1.2mu\equiv f^n(\perp ):\text{mspace}-1.2mu\equiv \underset{n\text{ times}}{\underbrace{f(f(\dots (f}}(\perp ))\dots )).$$

$$0$$

$$\prod _{\alpha :\mathsf{N}\to 2}\left(\prod _{n:\mathsf{N}}\alpha (n)=0\right)+\left(\sum _{k:\mathsf{N}}\alpha (k)=1\right).$$

$$\beta (n):\text{mspace}-1.2mu\equiv \{\begin{array}{ll}\mathrm{inl}(k)& \text{if k is the least integer ≤n such that α(k)=1;}\\ \mathrm{inr}(\star )& \text{else}.\end{array}$$

$$L(X):\text{mspace}-1.2mu\equiv \sum _{P:\Omega }(P\to X).$$

$${\perp }_X:\text{mspace}-1.2mu\equiv \left(0,\text{from-}{0}_X\right):L(X),$$

$${\eta }_X(x):\text{mspace}-1.2mu\equiv (1,\lambda t.x).$$

$$L(X)\equiv \left(\sum _{P:\Omega }(P\to X)\right)\simeq \left(\left(1\to X\right)+\left(0\to X\right)\right)\simeq \left(X+1\right),$$

$$\left(l=m\right)\simeq \sum _{e^{\prime }:\mathrm{isdefined}(l)=\mathrm{isdefined}(m)}\mathrm{transport}(e^{\prime },\mathrm{value}(l))=\mathrm{value}(m).$$

$$e:\text{mspace}-1.2mu\equiv \mathsf{eqtoiff}(e^{\prime }):\mathrm{isdefined}(l)\leftrightarrow \mathrm{isdefined}(m).$$

$$\mathrm{transport}(e^{\prime },\mathrm{value}(l))=\mathrm{value}(l)\circ (\mathsf{idtoeqv}(e^{\prime }){)}^{-1}.$$

$$f^{\#}(P,\varphi)\vcentcolon\mspace{-1.2mu}\equiv\Bigg{(}\sum_{p:P}\operatorname{\mathsf{isdefined}}(f(\varphi(p))),\psi\Bigg{)},$$

$$l=m\simeq \sum _{e:\mathrm{isdefined}(l)=\mathrm{isdefined}(m)}\mathrm{transport}(e,\mathrm{value}(l))=\mathrm{value}(m).$$

$$(P=R)\to (P\leftrightarrow R)\stackrel{\text{PropExt}}{\to }(P=R)$$

$$l⊑m:\text{mspace}-1.2mu\equiv \mathrm{isdefined}(l)\to l=m.$$

$$\underline{0}:\text{mspace}-1.2mu\equiv \mathsf{zero};\underline{n+1}:\text{mspace}-1.2mu\equiv \mathrm{succ}\underline{n}.$$

$$\prod _{\sigma :\text{PCF types}}\text{PCF terms of type σ}\to \text{PCF terms of type σ}\to {\mathcal{U}}_0$$

$$R:\prod _{\sigma :\text{PCF types}}\left(\text{PCF terms of type σ}\to \text{PCF terms of type σ}\to {\Omega }_{{\mathcal{U}}_0}\right)$$

$${▹}_{\text{impred}}:\prod _{\sigma :\text{PCF types}}\left(\text{PCF terms of type σ}\to \text{PCF terms of type σ}\to {\Omega }_{{\mathcal{U}}_1}\right).$$

$$\mathsf{extend}$$

$$\mathsf{refl}$$

$$\mathsf{trans}$$

$${\chi }_{x,y}(n):\text{mspace}-1.2mu\equiv \{\begin{array}{ll}x& \text{if }n=0;\\ y& \text{else};\end{array}$$

$$[[\underline{m+1}]]$$

$$=L(s)(\eta (m))$$

$$=\eta (m+1)$$

$$[[\mathrm{ifz}st\underline{n+1}]]=[[t]].$$

$$[[\mathrm{ifz}st\underline{n+1}]]$$

$$=[[\mathrm{ifz}st]](\eta (n+1))$$

$$=({\chi }_{[[s]],[[t]]}{)}^{\#}(\eta (n+1))$$

$$={\chi }_{[[s]],[[t]]}(n+1)$$

$$=[[t]].$$

Full text

1 Introduction

We develop the Scott model of the programming language PCF in constructive predicative univalent mathematics. In 1969, Dana Scott [24] proposed a logic (LCF) for computing with functionals. In 1977, Gordon Plotkin [21] considered LCF as a programming language (PCF); introducing operational semantics based on Scott’s logic and proving (and formulating) soundness and computational adequacy. Later, the techniques of Scott and Plotkin were extended to many other programming languages [22]. These developments all took place in (informal) set theory with classical logic.

Our aim is to test these techniques in Voevodsky’s constructive univalent type theory [28]. Our development differs from the classical approach [25] in three key ways. First of all, we have situated our development in the framework of univalent mathematics. Secondly, our work takes place in a constructive meta-theory. Thirdly, we work predicatively (meaning we do not assume propositional resizing).

The essential difference (for our development) between univalent type theory on the one hand, and set theory or systems like Coq on the other, is the treatment of truth values (propositions). We will discuss manifestations of this difference in Section 1.1.3 and throughout the paper.

1.1 Technical preliminaries

In this section we briefly explain the syntax of PCF and its computational behaviour. Moreover, we recall the notion of denotational semantics and the Scott model of PCF (in a classical setting) in particular. We also mention two fundamental properties that a model of PCF should enjoy: soundness and computational adequacy. Finally, we recall the lifting monad in the context of univalent type theory and sketch the construction of the Scott model in constructive univalent type theory.

1.1.1 PCF

PCF [21] is a typed programming language. A detailed description of PCF is given in Section 5. We briefly discuss its most characteristic features here. PCF is a typed $\lambda$-calculus with additional constants. For example, we have numerals $\underline{n}$ of base type $\iota$ corresponding to natural numbers and basic operations on them, such as a predecessor term $\operatorname{\mathsf{pred}}$ and a term $\operatorname{\mathsf{ifz}}$ that allows us to perform case distinction on whether an input is zero or not. The most striking feature of PCF is its fixed point combinator $\operatorname{\mathsf{fix}}_{\sigma}$ for every PCF type $\sigma$. The idea is that for a term $t$ of function type $\sigma\Rightarrow\sigma$, the term $\operatorname{\mathsf{fix}}_{\sigma}\,t$ of type $\sigma$ is a fixed point of $t$. The use of $\operatorname{\mathsf{fix}}$ is that it gives us general recursion.

The operational semantics of PCF is a reduction strategy that allows us to compute in PCF. We write $s\mathbin{\triangleright}t$ for $s$ reduces to $t$. We show a few examples below:

[TABLE]

We see that $\operatorname{\mathsf{pred}}$ indeed acts as a predecessor function and that $\operatorname{\mathsf{ifz}}$ performs case distinction on whether its third argument is zero or not. The reduction rule for $\operatorname{\mathsf{fix}}$ reflects that $\operatorname{\mathsf{fix}}f$ is a fixed point $f$ and may be seen as an unfolding (of a recursive definition).

As an example of the use of $\operatorname{\mathsf{fix}}$, consider a function $g$ on the natural numbers given by the recursive definition: $g(0)\coloneqq s$ and $g(n+1)\coloneqq t(g(n))$. We can define $g$ in PCF as $\operatorname{\mathsf{fix}}G$ where $G\coloneqq\lambda(f:\iota\Rightarrow\iota).\lambda(x:\iota).\operatorname{\mathsf{ifz}}s\,(t(\operatorname{\mathsf{pred}}x))\,x$. Having general recursion also introduces non-termination, as for example the successor function on naturals has no fixed point.

Instead of the formulation by Plotkin [21], which features variables and $\lambda$-abstraction, we revert in Section 5 to the original, combinatory, formulation of the terms of LCF by Scott [24] in order to simplify the technical development.

1.1.2 Models of PCF

We have seen that the operational semantics give meaning to the PCF terms by specifying computational behaviour. Another way to give meaning to the PCF terms is through denotational semantics, i.e. by giving a model of PCF. A model of PCF assigns to every PCF type $\sigma$ some mathematical structure $\llbracket\sigma\rrbracket$ and to every PCF term $t$ of type $\sigma$ an element $\llbracket t\rrbracket$ of $\llbracket\sigma\rrbracket$.

Soundness and computational adequacy.

Soundness and computational adequacy are important properties that a model of PCF should have.

Soundness states that if a PCF term $s$ computes to $t$ (according to the operational semantics), then their interpretations are equal in the model (symbolically, $\llbracket s\rrbracket=\llbracket t\rrbracket$).

Computational adequacy is completeness at the base type $\iota$. It says that for every term $t$ of type $\iota$ and every natural number $n$, if $\llbracket t\rrbracket=\llbracket\underline{n}\rrbracket$, then $t$ computes to $\underline{n}$.

The Scott model, classically.

To model PCF and its non-termination, Dana Scott [24] introduced the Scott model: a type is interpreted as a directed complete poset with a least element (or dcpo with $\bot$, for short). Concretely, PCF types are interpreted as follows.

Interpreting the base type $\iota$.

One proves that adding a least element $\bot_{\mathbb{N}}$ to the set $\mathbb{N}$ of natural numbers yields a dcpo with $\bot$, known as the flat natural numbers. This is then the interpretation of the base type $\iota$. This least element $\bot_{\mathbb{N}}$ serves as the interpretation of a term of type $\iota$ that does not compute to a numeral, like $\operatorname{\mathsf{fix}}\operatorname{\mathsf{succ}}$ where $\operatorname{\mathsf{succ}}$ denotes the successor map on $\iota$.

Interpreting function types.

Function types are interpreted by considering continuous maps (i.e. monotone maps that preserve directed suprema) between two dcpos with $\bot$. Such maps can be ordered pointwise to form another dcpo with $\bot$.

A striking feature, and the crux of the Scott model, is that every continuous map has a (least) fixed point. Moreover, the assignment of a continuous map to its least fixed point is continuous. This allows us to soundly interpret the characteristic $\operatorname{\mathsf{fix}}$ term of PCF.

The Scott model was proved sound and computationally adequate by Plotkin [21]. A modern presentation may be found in Streicher’s [25].

Issues with constructivity.

While the interpretation of function types goes through constructively, the above interpretation of the base type $\iota$ is problematic from a constructive viewpoint. Indeed, the proof that the flat natural numbers form a dcpo relies on classical reasoning in its analysis of the directed subsets: excluded middle allows us to prove that every directed subset of the flat natural numbers is exactly one of $\{\bot\}$, $\{\bot,n\}$ or $\{n\}$ for some natural number $n$. In fact, we can show that this reliance is in some sense essential: in Section 3 we prove that if the flat natural numbers form a dcpo, then the Limited Principle of Omniscience (LPO) holds. This principle asserts that every binary sequence is either [math] everywhere or it attains the value $1$ at some point. LPO is not constructively acceptable [4, p. 9], it is even provably false in some varieties of constructive mathematics [5, pp. 3–4], and it is independent of Martin-Löf Type Theory [13].

1.1.3 Univalent type theory

As mentioned at the beginning of Section 1, an essential difference between univalent type theory on the one hand, and set theory or systems like Coq on the other, is the treatment of truth values (propositions). To illustrate this difference, consider the definition of a poset (cf. Definition 2).

Example 1**.**

In set theory, the mathematical structure is provided by a set $X$ and a binary relation $\leq$ on $X$. Moreover, this relation is required to be reflexive, transitive and antisymmetric. Reflexivity, $\forall_{x\in X}x\leq x$ is a logical statement that is bivalent.

In type theory, if we define ${\leq}:{X\to X\to\mathsf{Type}}$, with $\mathsf{Type}$ some type universe, then the type encoding reflexivity, $\prod_{x:X}x\leq x$, may have more than one element. This is a fundamental difference with set theory.

In Coq, we could instead define ${\leq}:{X\to X\to\texttt{Prop}}$, where Prop is Coq’s special sort of propositions. This sort is defined such that (for instance) reflexivity, $\forall_{x:X}\,x\leq x$, is again in Prop.

The crucial difference between these approaches and the univalent approach, is that in univalent type theory, we prove that something is a proposition (truth value). Following Voevodsky, we define a type to be a proposition (truth value, subsingleton) if it has at most one element with respect to its identity type, i.e. up to propositional equality. To define posets, we then ask for a witness that the type $x\leq y$ is a proposition for every $x,y:X$. This allows us, in the presence of function extensionality (which is a consequence of the univalence axiom), to prove that reflexivity and transitivity are propositions. For example, for reflexivity, we wish to show that the type $\prod_{x:X}x\leq x$ is a proposition. So let $f,g$ be two elements of this type. By function extensionality, it suffices to show that $f(x)=g(x)$ for every $x:X$. But the type of $f(x)$ and $g(x)$ is $x\leq x$, which is a proposition by requirement, so $f(x)$ and $g(x)$ must be (propositionally) equal, as desired. Finally, we require $X$ to be a set: any two elements of $X$ are equal in at most one way. This ensures, using function extensionality again, that antisymmetry is a proposition.

Sometimes, we will want to make a type into a proposition, by identifying its elements. This is achieved through the propositional truncation, a higher inductive type. For example, we will need it to define directed families (Definition 5), but also to define the reflexive transitive closure of a proposition-valued relation (Definition 35). We will further explain these examples in the main text. The universal property of the propositional truncation is described in Section 1.2. For more on propositions, sets and propositional truncation in univalent type theory, see [28, Chapter 3].

1.2 Overview of results

We work in intensional Martin-Löf Type Theory with inductive types (including the empty $\mathsf{0}$, unit $\mathsf{1}$, natural numbers $\mathsf{N}$, and identity types), $+$-, $\Sigma$- and $\Pi$-types. As usual, we simply write $x=y$ for the identity type $\operatorname{\mathsf{Id}}_{X}(x,y)$, use ${\equiv}$ for the judgemental equality and write ${\simeq}$ for Voevodsky’s notion of type equivalence.

We need (at least) two universes $\mathcal{U}_{0},\mathcal{U}_{1}$ closed under $+$-, $\Sigma$- and $\Pi$-types, such that $\mathcal{U}_{0}$ contains $\mathsf{0}$, $\mathsf{1}$ and $\mathsf{N}$, while $\mathcal{U}_{1}$ contains $\mathcal{U}_{0}$. We work predicatively, i.e. we do not assume propositional resizing, so the type of propositions in $\mathcal{U}_{0}$, denoted by $\Omega$, lives in the universe $\mathcal{U}_{1}$.

We also assume two extensionality axioms. The first is function extensionality, which asserts that pointwise equal functions are equal. Given two (dependent) functions $f,g:\prod_{a:A}B(a)$, we write $f\sim g$ for the type $\prod_{a:A}f(a)=g(a)$, often called the type of homotopies between $f$ and $g$. Function extensionality makes the type $f\sim g$ equivalent to the identity type $f=g$. The second is propositional extensionality, which says that logically equivalent propositions are equal, i.e. if $P$ and $Q$ are propositions, then $P\leftrightarrow Q$ implies $P=Q$. In the presence of function extensionality this is equivalent to $(P\leftrightarrow Q)\simeq(P=Q)$.

Although we do not need the univalence axiom at any point, we remark that both extensionality axioms above follow from it. Moreover, we emphasise the importance of the idea of truncation levels, which is fundamental to univalent type theory.

Finally, we assume the existence of a single higher inductive type, the propositional truncation: given a type $X$ in a universe $\mathcal{U}$, we assume that we have a proposition $\left\|X\right\|$ in $\mathcal{U}$ with a map $\left|-\right|:X\to\left\|X\right\|$ such that if $P$ is a proposition in any universe and $f:X\to P$ is a map, then $f$ factors through $\left|-\right|$. Diagrammatically,

[TABLE]

Observe that the factorisation $\overline{f}$ is unique by function extensionality and the fact that $P$ is a proposition.

Our paper can be summarised as follows:

Section 2.

We introduce the theory of dcpos with $\bot$ (known as domain theory) in predicative constructive univalent type theory. We take the carriers of the dcpos to be sets (in the sense of univalent type theory) and the partial orders to be proposition-valued. Propositional truncation plays an import part in defining directedness.

Section 3.

We elaborate on the issue with the classical construction of the Scott model in a constructive meta-theory (cf. the final paragraph of Section 1.1.2).

Section 4.

To remedy this issue, we work instead with the lifting monad (also known as the partial map classifier monad) from topos theory [19], which has been extended to constructive type theory by Reus and Streicher [23] and recently to univalent type theory by Escardó and Knapp [12, 18]. The lifting $\operatorname{\mathcal{L}}(X)$ of a type $X$ is defined as ${\operatorname{\mathcal{L}}(X)\vcentcolon\mspace{-1.2mu}\equiv\sum_{P:\Omega}(P\to X)}$, where $\Omega$ is the type of propositions in the first universe. We think of the elements $(P,\varphi)$ of $\operatorname{\mathcal{L}}(X)$ as partial elements of $X$: in case $P$ holds, we get an element of $X$, but $P$ may also fail to hold and then the partial element is thought of as undefined. In our constructive model, we interpret the base type of PCF as the lifting $\operatorname{\mathcal{L}}(\mathsf{N})$ of the natural numbers.

Section 5.

We define a combinatory version of PCF and its (small-step) operational semantics. We use the propositional truncation to obtain well-behaved relations in the small-step operational semantics.

Section 6.

We define our constructive Scott model of PCF using the lifting monad.

Section 7.

We show how the usual proofs of soundness and computational adequacy adapt to our constructive setting with propositional truncations.

Section 8.

Recall that in our model the PCF type $\iota$ for natural numbers is interpreted as $\operatorname{\mathcal{L}}(\mathsf{N})$, where $\mathsf{N}$ is the natural numbers type. Thus, if $t$ is a PCF term of type $\iota$, then we get an element $\llbracket t\rrbracket:\operatorname{\mathcal{L}}(\mathsf{N})$. Hence, for every such term $t$ we have a proposition $\operatorname{\mathsf{pr_{1}}}(\llbracket t\rrbracket):\Omega$. We show that such propositions are all semidecidable. This result should be contrasted with the fact that a restricted version of the lifting monad where we take a $\Sigma$-type over only semidecidable propositions is not adequate for our purposes, as we explain at the end of Section 8.

In proving our results, we take the opportunity to record some more general properties of reflexive transitive closures (Section 8.1) and indexed $\mathsf{W}$-types (Section 8.2).

Section 9.

We discuss the universe levels involved in our development. This is important, because we want our results to go through predicatively, i.e. without propositional resizing.

Section 10.

We summarise our main results and describe directions for future work.

1.3 Related work

Partiality in type theory has been the subject of recent study. We briefly discuss the different approaches.

Firstly, there are the delay monad by Capretta [6] and its quotient by weak bisimilarity, as studied by Chapman et al. [7]. They used countable choice to prove that the quotient is again a monad. Escardó and Knapp [12, 18] showed that a weak form of countable choice is indeed necessary to prove this. However, Coquand, Mannaa, and Ruch [9, Corollary 2] have shown that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation. Theorem 3.3 of Coquand’s [8] extends this to dependent type theory with a hierarchy of univalent universes and (some) higher inductive types. Moreover, Andrew Swan [26, 27] recently showed that even the weak form of choice required is not provable in univalent type theory.

Another approach is laid out by Altenkirch, Danielsson and Kraus. [2]. They postulated the existence of a particular quotient inductive-inductive type (QIIT) and showed that it satisfies the universal property of the free $\omega$-cpo with a least element [2, Theorem 5]. Moreover, Altenkirch et al. showed that, assuming countable choice, their QITT coincides with the quotiented delay monad.

We stress that our approach does not need countable choice or quotient inductive-inductive types.

Finally, Benton, Kennedy and Varming [3] used Capretta’s delay monad to give a constructive approach to domain theory. Their approach used setoids, so that every object comes with an equivalence relation that maps must preserve. One cannot quotient these objects, because quotienting Capretta’s delay monad requires (a weak form of) countable choice, as explained above. In our development, we instead use Martin-Löf’s identity types as our notion of equality. Moreover, we do not make use of Coq’s impredicative Prop universe and our treatment incorporates directed complete posets (dcpos) and not just $\omega$-cpos.

1.4 Formalisation

All our results up to and including the proof of computational adequacy (and except for Section 3 and Remark 29) have been formalised in the proof assistant Coq using the UniMath library [29] and Coq’s Inductive types. The general results from Section 8 have also been formalised, but their direct applications to PCF, e.g. single-valuedness of the operational semantics and PCF as an indexed $\mathsf{W}$-type, have not. The code may be found at https://github.com/tomdjong/UniMath/tree/paper. Instructions for use can be found in the repository’s README.md file. Browsable documentation for the formalisation may be found at https://tomdjong.github.io/Scott-PCF-UniMath/toc.html. Definitions and proofs of lemmas, propositions and theorems are labelled with their corresponding identifiers in the Coq name, for example as pcf, which also functions as a hyperlink to the appropriate definition in the documentation.

At present, it is not possible to verify universe levels in UniMath. Therefore, to verify the correctness of our development and our claims in Section 9 about universe levels in particular, we reformalised part of our development in Agda using Martín Escardó library [14]. Our code is now part of the library. An HTML rendering may be found at: https://www.cs.bham.ac.uk/~mhe/agda-new/PCFModules.html.

1.5 Acknowledgements

Firstly, I would like to thank Martín Escardó for suggesting and supervising this project. Secondly, I am grateful to Benedikt Ahrens for his support, his help with UniMath, and in particular for his feedback on earlier versions of this paper. I should also like to thank Andrej Bauer and Bernhard Reus for their comments and questions. Finally, I am indebted to the anonymous referees for their thorough and valuable reports that helped to improve the paper.

2 Basic domain theory

We introduce basic domain theory in the setting of constructive predicative univalent mathematics. We adapt known definitions (cf. [1, Section 2.1] and [25, Chapter 4]) to constructive univalent type theory, paying special attention to how our definitions may involve propositional truncations.

2.1 Directed complete posets

Definition 2** (PartialOrder).**

A poset $(X,\leq)$ is a set $X$ together with a proposition-valued binary relation $\leq:X\to X\to\Omega$ satisfying:

reflexivity*: $\prod_{x:X}x\leq x$;* 2. 2.

antisymmetry*: $\prod_{x,y:X}x\leq y\to y\leq x\to x=y$;* 3. 3.

transitivity*: $\prod_{x,y,z:X}x\leq y\to y\leq z\to x\leq z$.*

Remark 3*.*

Notice that we require $\leq$ to take values in $\Omega$, the type of propositions in $\mathcal{U}_{0}$, cf. Example 1. This allows us to prove (using function extensionality [28, Example 3.6.2]) that reflexivity and transitivity are propositions, i.e. there is at most one witness of reflexivity and transitivity. We also express this by saying that reflexivity and transitivity are properties, rather than structures. Moreover, we restrict to $X$ being a set to ensure that antisymmetry is a property, rather than a structure.

Definition 4** (posetmorphism).**

Let $X$ and $Y$ be posets. A poset morphism from $X$ to $Y$ is a function between the underlying sets that preserves the order. We also say that the function is monotone.

Definition 5** (isdirected).**

Let $(X,\leq)$ be a poset and $I$ any type. Given a family $u:I\to X$, we often write $u_{i}$ for $u(i)$. Such a family is called directed if $I$ is inhabited (i.e. $\|I\|$ holds) and $\prod_{i,j:I}\left\|\sum_{k:I}{\left(u_{i}\leq u_{k}\right)\times\left(u_{j}\leq u_{k}\right)}\right\|$.

Remark 6*.*

We use the propositional truncation in the definition above to ensure that being directed is a property, rather than a structure (isaprop_isdirected).

Firstly, we express that the type $I$ is inhabited by requiring an element of $\|I\|$. This is different from requiring an element of $I$. It is akin to the difference (in set theory) between a set $X$ such that $\exists{x\in X}$ holds and a pair $(X,x)$ of a set with a chosen element $x\in X$.

Secondly, if we had used an untruncated $\Sigma$ in the second clause of the definition, then we would have asked our poset to be equipped with an operation mapping pairs $(x,y)$ of elements to some specified element greater than both $x$ and $y$.

Definition 7** **(isupperbound,

islub, isdirectedcomplete).

An element $x$ of a poset $X$ is an upper bound of a family $u:I\to X$ if $u_{i}\sqsubseteq x$ for every $i:I$. It is a least upper bound of $u$ if it is an upper bound and $x\sqsubseteq y$ holds whenever $y$ is an upper bound of $u$.

A poset $X$ is called $\mathcal{U}$-directed complete for a type universe $\mathcal{U}$ if every directed family in $X$ indexed by a type in $\mathcal{U}$ has a least upper bound in $X$, which we denote by $\bigsqcup_{i:I}u_{i}$. Symbolically, $\prod_{I:\mathcal{U}}\prod_{u:I\to X}\left(u\text{ is directed}\to\sum_{x:X}x\text{ is a least upper bound of u}\right).$

We call such a poset a $\mathcal{U}$-dcpo. We shall often simply write dcpo, omitting reference to the type universe.

Remark 8*.*

Contrary to Definition 5, directed completeness is not phrased with a truncated $\Sigma$. This justifies having the least upper bound operator $\bigsqcup$. The reason for this definition of directed completeness is that least upper bounds are unique when they exist (lubsareunique). Moreover, the type expressing that an element is a least upper bound for a family can be shown to be a proposition using function extensionality (isaprop_islub). Hence, for any family $u$, the type of least upper bounds of $u$ and its propositional truncation are equivalent. This observation also tells us, using function extensionality again, that the type expressing that a poset is directed complete is also a proposition (isaprop_isdirectedcomplete), i.e. it is a property of the poset.

Remark 9*.*

In classical mathematics, a dcpo is usually defined as a poset such that every directed subset has a least upper bound. We have formulated our version using families, because in our type-theoretic framework functions are primitive, unlike in set theory where sets are primitive and functions are encoded as particular sets. Another reason for preferring families is that we work in the absence of propositional resizing, so that we must pay attention to size and therefore only ask for least upper bounds of small directed subsets. This point is explained and worked out in detail in [11, Section 5] to which we refer the interested reader. Here we limit ourselves to saying that working with families is more direct, and that for the Scott model we will only need to consider simple $\mathsf{N}$-indexed directed families anyway.

2.2 Morphisms of dcpos

Definition 10** (isdcpomorphism).**

Let $D$ and $E$ be dcpos. A poset morphism from $D$ to $E$ is a dcpo morphism (or continuous) if it preserves least upper bounds of directed families. That is, if $u:I\to D$ is a directed family, then $f\left(\bigsqcup_{i:I}u_{i}\right)$ is the least upper bound of $f\circ u:I\to E$.

Thus, by definition, a dcpo morphism is required to be a poset morphism, i.e. it must be monotone. However, as is well-known in domain theory, requiring that the function is monotone is actually redundant, as the following lemma shows.

Lemma 11**.**

Let $D$ and $E$ be dcpos. If $f$ is a function (on the underlying types) from $D$ to $E$ preserving least upper bounds of directed families, then $f$ is order preserving.

• Proof (preservesdirectedlub_isdcpomorphism). Let $f:D\to E$ be a morphism of dcpos and suppose $x,y:D$ with $x\leq y$. Consider the family $\mathsf{1}+\mathsf{1}\to D$ defined as $\operatorname{\mathsf{inl}}(\star)\mapsto x$ and $\operatorname{\mathsf{inr}}(\star)\mapsto y$. This family is easily seen to be directed and its least upper bound is $y$. Now $f$ preserves this least upper bound, so $f(x)\leq f(y)$. ∎

Lemma 12**.**

Every morphism of dcpos preserves directed families. That is, if $f:D\to E$ is a morphism of dcpos and $u$ is a directed family in $D$, then $f\circ u$ is a directed family in $E$.

• Proof (dcpomorphism_preservesdirected). Using monotonicity of $f$. ∎

Theorem 13**.**

Let $D$ and $E$ be dcpos. The morphisms from $D$ to $E$ form a dcpo with the pointwise order.

• Proof (dcpoofdcpomorphisms). The least upper bound of a directed family of dcpo morphisms is also given pointwise. The proof only differs from the standard proof of [25, Theorem 4.2] in that it uses directed families, rather than subsets. One may consult the formalisation for the technical details. ∎

2.3 Dcpos with $\bot$

Definition 14** (dcpowithbottom).**

A dcpo with $\bot$ is a dcpo $D$ together with a least element in $D$.

Theorem 15**.**

Let $D$ be a dcpo and let $E$ be a dcpo with $\bot$. Ordered pointwise, the morphisms from $D$ to $E$ form a dcpo with $\bot$, which we denote by $E^{D}$.

• Proof (dcpowithbottom_ofdcpomorphisms). Since the order is pointwise, the least morphism from $D$ to $E$ is simply given by mapping every element in $D$ to the least element in $E$. The rest is as in Theorem 13. ∎

Dcpos with bottom elements are interesting because they admit least fixed points. Moreover, these least fixed points are themselves given by a continuous function.

Theorem 16**.**

Let $D$ be a dcpo with $\bot$. There is a continuous function $\mu:D^{D}\to D$ that sends each continuous function to its least fixed point. In fact, $\mu$ satisfies:

$f(\mu(f))=\mu(f)$* for every continuous $f:D\to D$;* 2. 2.

for every continuous $f:D\to D$ and each $d:D$, if $f(d)\leq d$, then $\mu(f)\leq d$.

• Proof. (leastfixedpoint_isfixedpoint, leastfixedpoint_isleast). We have formalised the proof of [1, Theorem 2.1.19]. We sketch the main construction here. For each natural number $n$, define $\mathsf{iter}(n):D^{D}\to D$ as

[TABLE]

By induction on $n$, one may show that every $\mathsf{iter}(n)$ is continuous. Then, the assignment $n~{}\mapsto~{}{\mathsf{iter}(n)}$ is a directed family in $D^{\left(D^{D}\right)}$. Finally, one defines $\mu$ as the least upper bound of this directed family. Recall that least upper bounds in the exponential are given pointwise, so that $\mu(f)=\bigsqcup_{n:\mathsf{N}}f^{n}(\bot)$. ∎

3 Constructive issues with partiality

In classical mathematics, a partial map from $\mathbb{N}$ to $\mathbb{N}$ can simply be seen as a total map from $\mathbb{N}$ to $\mathbb{N}\cup\{\bot\}$, where $\bot$ is some fresh element not in $\mathbb{N}$. The flat dcpo $\mathbb{N}_{\bot}$ is $\mathbb{N}\cup\{\bot\}$ ordered as in the following Hasse diagram:

[TABLE]

Using excluded middle, a directed subset of $\mathbb{N}_{\bot}$ is either $\{\bot\}$, $\{n\}$ or $\{\bot,n\}$ (with $n$ a natural number). The least upper bounds of which are easily computed as $\bot$, $n$ and $n$, respectively. Thus, with excluded middle, $\mathbb{N}_{\bot}$ is directed complete.

One could hope that the above translates directly into constructive univalent mathematics, that is, that the poset $\mathsf{N}_{\bot}\vcentcolon\mspace{-1.2mu}\equiv\left(\mathsf{N}+\mathsf{1},\leq_{\bot}\right)$ with $\leq_{\bot}$ the flat order (i.e. $\operatorname{\mathsf{inr}}(\star)$ is the least element and all other elements are incomparable) is ($\mathcal{U}_{0}$-)directed complete (in the sense of Definition 7). However, we can prove that this implies Bishop’s Limited Principle of Omniscience (LPO), a constructive taboo (recall the final paragraph of Section 1.1.2), as follows.

Write $\mathsf{2}$ for the type $\mathsf{1}+\mathsf{1}$, and [math] and $1$ for its inhabitants $\operatorname{\mathsf{inl}}(\star)$ and $\operatorname{\mathsf{inr}}(\star)$, respectively. In type theory, LPO may be formulated111This formulation does not ensure that the type is a proposition, so one could also consider truncating the $\Sigma$ or asking for the least $k$ such that $\alpha(k)=1$. But this version is sufficient for our purposes, and logically equivalent to the one with the truncated $\Sigma$. as the following type:

[TABLE]

Lemma 17**.**

Directed completeness of $\mathsf{N}_{\bot}$ implies LPO.

• Proof. Suppose that $\mathsf{N}_{\bot}$ is ($\mathcal{U}_{0}$-)directed complete. Let $\alpha:\mathsf{N}\to\mathsf{2}$ be an arbitrary binary sequence. Define the family $\beta:\mathsf{N}\to\mathsf{N}_{\bot}$ as

[TABLE]

Then $\beta$ is directed, so by assumption, it has a supremum $s$ in $\mathsf{N}_{\bot}$. By the induction principle of sum-types, we can decide whether $s=\operatorname{\mathsf{inl}}(k)$ for some $k:\mathsf{N}$ or $s=\operatorname{\mathsf{inr}}(\star)$. The former implies $\sum_{k:\mathsf{N}}\alpha(k)=1$ and we claim that the latter implies $\prod_{n:\mathsf{N}}\alpha(n)=0$. For suppose that $s=\operatorname{\mathsf{inr}}(\star)$ and let $n:\mathsf{N}$. Since $\mathsf{2}$ has decidable equality, it suffices to show that $\alpha(n)\neq 1$. Assume for a contradiction that $\alpha(n)=1$. Then $\beta(n)=\operatorname{\mathsf{inl}}(k)$ for some natural number $k\leq n$. Using that $s$ is the supremum of $\beta$ yields: $\operatorname{\mathsf{inl}}(k)=\beta(n)\leq_{\bot}s=\operatorname{\mathsf{inr}}(\star)$. By definition of the order we also have the reverse inequality $\operatorname{\mathsf{inr}}(\star)\leq_{\bot}\operatorname{\mathsf{inl}}(k)$. Hence, $\operatorname{\mathsf{inr}}(\star)=\operatorname{\mathsf{inl}}(k)$ by antisymmetry, which is a contradiction, so $\alpha(n)\neq 1$ as desired. ∎

4 Partiality, constructively

In this section we present the lifting monad as a solution to the problem described in the previous section. Using the lifting monad in univalent type theory to deal with partiality originates with the work of Escardó and Knapp [12, 18] and aims to avoid countable choice.

We start by defining the lifting of a type and by characterising its identity type. In Section 4.1 we prove that the lifting carries a monad structure, while in Section 4.2 we show that the lifting of a set is a dcpo with $\bot$. Most of the definitions and some of the results in this section can be found in [18] or in [12]. Exceptions are Lemma 22, Theorem 25 and Theorem 27. We note that our characterisation of equality of the lifting, Lemma 22, is implicit in the fact that the order of [12] is antisymmetric. The order on the lifting in this paper (see Theorem 26) is different from the order presented in [12, 18]. The two orders are equivalent, however, as observed by in [14, LiftingUnivalentPrecategory]. We found the order in this paper to be more convenient.

Definition 18** (lift).**

Let $X$ be any type. Define the lifting of X as

[TABLE]

Strictly speaking, we should have written $\operatorname{\mathsf{pr_{1}}}(P)\to X$, because elements of $\Omega$ are pairs of types and witnesses that these types are subsingletons. We will almost always suppress reference to these witnesses in this paper.

Definition 19** (liftorder_least).**

For any type $X$, the type $\operatorname{\mathcal{L}}(X)$ has a distinguished element

[TABLE]

where $\textup{{from-}}\mathsf{0}_{X}$ is the unique function from $\mathsf{0}$ to $X$.

Definition 20** (lift_embedding).**

There is a canonical map $\eta_{X}\colon X\to\operatorname{\mathcal{L}}(X)$ defined by

[TABLE]

Assuming LEM (i.e. $\prod_{P:\Omega}(P+\lnot P)$), we can prove that the only propositions are $\mathsf{0}$ and $\mathsf{1}$, for if a proposition $P$ holds, then it is equal (by propositional extensionality) to $\mathsf{1}$ and if it does not hold, then it is equal to $\mathsf{0}$. Hence, if we assume LEM then the two definitions above capture all of the lifting, since LEM implies:

[TABLE]

as $\left(\mathsf{1}\to X\right)\simeq X$ and there is a unique function from $\mathsf{0}$ to any type $X$. Constructively, things are more interesting, of course.

We proceed by defining meaningful projections.

Definition 21** **(isdefined,

value).

We take $\operatorname{\mathsf{isdefined}}:\operatorname{\mathcal{L}}(X)\to\Omega$ to be the first projection. The function $\operatorname{\mathsf{value}}:\prod_{l:\operatorname{\mathcal{L}}(X)}\operatorname{\mathsf{isdefined}}(l)\to X$ is given by: $\operatorname{\mathsf{value}}(P,\varphi)(p)\vcentcolon\mspace{-1.2mu}\equiv\varphi(p)$.

Since equality of $\Sigma$-types often requires $\operatorname{\mathsf{transport}}$, it will be convenient to characterise the equality of $\operatorname{\mathcal{L}}(X)$.

Lemma 22**.**

Let $X$ be any type and let $l,m:\operatorname{\mathcal{L}}(X)$. The following are logically equivalent222In fact, there is a type equivalence. One can prove this using univalence and a generalised structure identity principle, cf. [14, LiftingIdentityViaSIP].

$l=m$;** 2. 2.

$\sum_{e:\operatorname{\mathsf{isdefined}}(l)\leftrightarrow\operatorname{\mathsf{isdefined}}(m)}\operatorname{\mathsf{value}}(l)\circ\operatorname{\mathsf{pr_{2}}}(e)\sim\operatorname{\mathsf{value}}(m)$.

• Proof. (lifteq_necc, lifteq_suff).

First of all, the characterisation of the identity type of $\Sigma$-types [28, Theorem 2.7.2] yields:

[TABLE]

Thus we only have to show that the right-hand side of ($\dagger$ ‣ ‣ 4) is logically equivalent to (2) in the lemma. Suppose first that we have $e^{\prime}:\operatorname{\mathsf{isdefined}}(l)=\operatorname{\mathsf{isdefined}}(m)$ and an equality ${p:\operatorname{\mathsf{transport}}(e^{\prime},\operatorname{\mathsf{value}}(l))=\operatorname{\mathsf{value}}(m)}$. Then

[TABLE]

Using path induction on $e^{\prime}$, we can prove that $\operatorname{\mathsf{value}}(l)\circ\operatorname{\mathsf{pr_{2}}}(e)=\operatorname{\mathsf{transport}}(e^{\prime},\operatorname{\mathsf{value}}(l))$. Together with $p$, this equality implies $\operatorname{\mathsf{value}}(l)\circ\operatorname{\mathsf{pr_{2}}}(e)\sim\operatorname{\mathsf{value}}(m)$, as desired.

Conversely, suppose $e:\operatorname{\mathsf{isdefined}}(l)\leftrightarrow\operatorname{\mathsf{isdefined}}(m)$ and $v:\operatorname{\mathsf{value}}(l)\circ\operatorname{\mathsf{pr_{2}}}(e)\sim\operatorname{\mathsf{value}}(m)$. By propositional extensionality, we obtain $e^{\prime}:\operatorname{\mathsf{isdefined}}(l)=\operatorname{\mathsf{isdefined}}(m)$ from $e$. From $e^{\prime}$ we can get an equivalence $\mathsf{idtoeqv}(e^{\prime}):\operatorname{\mathsf{isdefined}}(l)\simeq\operatorname{\mathsf{isdefined}}(m)$. Furthermore, using path induction on $e^{\prime}$, one can prove that

[TABLE]

Hence, it suffices to show that the right-hand side of ($\ast$ ‣ ‣ 4) is equal to $\operatorname{\mathsf{value}}(m)$. The homotopy $v$ yields $\operatorname{\mathsf{value}}(l)\circ\operatorname{\mathsf{pr_{2}}}(e)=\operatorname{\mathsf{value}}(m)$ by function extensionality, so it suffices to prove that $(\mathsf{idtoeqv}(e^{\prime}))^{-1}=\operatorname{\mathsf{pr_{2}}}(e)$. But these are both functions with codomain $\operatorname{\mathsf{isdefined}}(l)$, which is a proposition, so they are equal by function extensionality. ∎

4.1 The lifting monad

In this section we prove that the lifting carries a monad structure.

This monad structure is most easily described as a Kleisli triple. The unit is given by Definition 20.

Definition 23** (Kleisli_extension).**

Given $f:X\to\operatorname{\mathcal{L}}(Y)$, the Kleisli extension $f^{\#}:\operatorname{\mathcal{L}}(X)\to\operatorname{\mathcal{L}}(Y)$ is defined by:

[TABLE]

where $\psi(p,d)\vcentcolon\mspace{-1.2mu}\equiv\operatorname{\mathsf{value}}(f(\varphi(p)))(d)$.

Theorem 24** (Theorem 5.8 in [18], Section 2.2 in [12]).**

The above constructions yield a monad structure on $\operatorname{\mathcal{L}}(X)$, i.e. the Kleisli laws hold (pointwise):

$\left(\eta_{X}\right)^{\#}\sim\operatorname{id}_{\operatorname{\mathcal{L}}(X)}$; 2. 2.

$f^{\#}\circ\eta_{X}\sim f$* for any $f:X\to\operatorname{\mathcal{L}}(Y)$;* 3. 3.

$g^{\#}\circ f^{\#}\sim(g^{\#}\circ f)^{\#}$* for any $f:X\to\operatorname{\mathcal{L}}(Y)$ and $g:Y\to\operatorname{\mathcal{L}}(Z)$.*

• Proof. (eta_extension, fun_extension_after_eta, extension_comp). The proofs are straightforward thanks to Lemma 22. Item (3) is essentially the associativity of $\Sigma$, i.e. equivalence between $\sum_{a:A}\sum_{b:B(a)}C(a,b)$ and $\sum_{(a,b):\sum_{a:A}B(a)}C(a,b)$. ∎

4.2 The lifting as a dcpo with $\bot$

The goal of this section is to endow $\operatorname{\mathcal{L}}(X)$ with a partial order that makes it into a dcpo with $\bot$, provided that $X$ is a set. We also show that the Kleisli extension from the previous section is continuous when regarded as a morphism between dcpos with $\bot$.

Theorem 25**.**

If $X$ is a set, then so is its lifting $\operatorname{\mathcal{L}}(X)$.

• Proof (liftofhset_isaset). As in the proof of Lemma 22, we have:

[TABLE]

Since $X$ is a set, the type $\operatorname{\mathsf{transport}}(e,\operatorname{\mathsf{value}}(l))=\operatorname{\mathsf{value}}(m)$ is a proposition. So, if we can prove that $\operatorname{\mathsf{isdefined}}(l)=\operatorname{\mathsf{isdefined}}(m)$ is a proposition, then the right hand side is a proposition indexed sum of propositions, which is again a proposition.

So let us prove that if $P$ and $Q$ are propositions, then so is $P=Q$. At first glance, it might seem like one needs univalence (for propositions) to prove this, but in fact propositional extensionality suffices. By [20, Lemma 3.11] (applied to the type of propositions), it suffices to give for every proposition $R$, a (weakly) constant (i.e. any two of its values are equal) endomap on $P=R$. But the composition

[TABLE]

is weakly constant, because $P\leftrightarrow R$ is a proposition, so this finishes the proof. ∎

Theorem 26** **(cf. Theorem 5.14 in [18] and Theorem 1 in

[12]).

If $X$ is a set, then $\operatorname{\mathcal{L}}(X)$ is a dcpo with $\bot$ with the following order:

[TABLE]

• Proof (liftdcpowithbottom). First of all, we should prove that $\operatorname{\mathcal{L}}(X)$ is a poset with the specified order. In particular, $\sqsubseteq$ should be proposition-valued. If $X$ is a set, then $\operatorname{\mathsf{isdefined}}(l)\to l=m$ is a function type into a proposition and therefore a proposition itself.

Reflexivity and transitivity of $\sqsubseteq$ are easily verified. Moreover, $\sqsubseteq$ is seen to be antisymmetric using Lemma 22.

The $\bot$ element of $\operatorname{\mathcal{L}}(X)$ is given by $\bot_{X}$ from Definition 19.

The construction of the least upper bound of a directed family is the most challenging part of the proof. Let $u:I\to\operatorname{\mathcal{L}}(X)$ be a directed family in $\operatorname{\mathcal{L}}(X)$. Consider the diagram (of solid arrows):

{\sum_{i:I}\operatorname{\mathsf{isdefined}}(u_{i})}$${X}$${\left\|\sum_{i:I}\operatorname{\mathsf{isdefined}}(u_{i})\right\|}$$\scriptstyle{\varphi:{(i,d)}\mapsto\operatorname{\mathsf{value}}(u_{i})(d)}$$\scriptstyle{|-|}$$\scriptstyle{\psi}

We are going to construct the dashed map $\psi$ that makes the diagram commute and define the least upper bound of $u$ as: $\left(\left\|\sum_{i:I}\operatorname{\mathsf{isdefined}}(u_{i})\right\|,\psi\right)$. Truncating the type is necessary, as $\sum_{i:I}\operatorname{\mathsf{isdefined}}(u_{i})$ may have more than one element if $I$ is not a proposition. The difficulty lies in the fact that the universal property of the truncation only tells us how to define maps into propositions. But $X$ is a set. We solve this problem using [20, Theorem 5.4], which says that every weakly constant function $f:A\to B$ to a set $B$ factors through $\left\|A\right\|$. That $f$ is weakly constant means that $f(a)=f(a^{\prime})$ for every $a,a^{\prime}:A$. So, to construct $\psi$, we only need to prove that the top map $\varphi$ in the diagram is weakly constant. Let $(i,d_{i}),(j,d_{j})$ be two elements of the domain of $\varphi$. We are to prove that $\operatorname{\mathsf{value}}(u_{i})(d_{i})=\operatorname{\mathsf{value}}(u_{j})(d_{j})$. As $X$ is a set, this is a proposition. Therefore, using that $u$ is directed, we obtain $k:I$ with $u_{i},u_{j}\sqsubseteq u_{k}$. But $d_{i}:\operatorname{\mathsf{isdefined}}(u_{i})$ and $d_{j}:\operatorname{\mathsf{isdefined}}(u_{j})$, so $u_{i}=u_{k}=u_{j}$ by definition of the order. Hence, $\varphi(i,d_{i})=\operatorname{\mathsf{value}}(u_{i})(d_{i})=\operatorname{\mathsf{value}}(u_{j})(d_{j})=\varphi(j,d_{j})$, as we wished to show. ∎

Theorem 27**.**

Let $X$ and $Y$ be sets and $f:X\to\operatorname{\mathcal{L}}(Y)$ any function. The Kleisli extension $f^{\#}:\operatorname{\mathcal{L}}(X)\to\operatorname{\mathcal{L}}(Y)$ is a morphism of dcpos.

• Proof (Kleisli_extension_dcpo). Let $v$ be the least upper bound of a directed family $u:I\to\operatorname{\mathcal{L}}(X)$ in $\operatorname{\mathcal{L}}(X)$. Proving that $f^{\#}$ is monotone is quite easy. By monotonicity, $f^{\#}(v)$ is an upper bound for the family $f^{\#}\circ u$. We are left to prove that it is the least. Suppose that $l:\operatorname{\mathcal{L}}(Y)$ is another upper bound for the family $f^{\#}\circ u$, i.e. $l\sqsupseteq f^{\#}(u_{i})$ for every $i:I$. We must show that $f^{\#}(v)\sqsubseteq l$. To this end, assume we have $q:\operatorname{\mathsf{isdefined}}(f^{\#}(v))$. We must prove that $f^{\#}(v)=l$.

From $q$, we obtain $p:\operatorname{\mathsf{isdefined}}(v)$ by definition of $f^{\#}$. By our construction of suprema in $\operatorname{\mathcal{L}}(X)$ and the fact that $f^{\#}(v)=l$ is a proposition, we may in fact assume that we have an element $i:I$ and $d_{i}:\operatorname{\mathsf{isdefined}}(u_{i})$. But $l\sqsupseteq f^{\#}(u_{i})$, so using $d_{i}$, we get the equality $l=f^{\#}(u_{i})$. Since $v$ is an upper bound for $u$, the term $d_{i}$ also yields $u_{i}=v$. In particular, $l=f^{\#}(u_{i})=f^{\#}(v)$, as desired. ∎

Remark 28* (liftfunctor_eq).*

Finally, one could define the functor $\operatorname{\mathcal{L}}$ from the Kleisli extension and unit by putting $\operatorname{\mathcal{L}}(f)\vcentcolon\mspace{-1.2mu}\equiv(\eta_{Y}\circ f)^{\#}$ for any $f:X\to Y$. However, it is equivalent and easier to directly define $\operatorname{\mathcal{L}}(f)$ by postcomposition: $\operatorname{\mathcal{L}}(f)(P,\varphi)\vcentcolon\mspace{-1.2mu}\equiv(P,f\circ\varphi)$.

Remark 29*.*

We remark that lifting may be regarded as a free construction, in more than one way in fact. This result should be compared to [2, Theorem 5], where Altenkirch et al. exhibit their QIIT as the free $\omega$-cpo with a least element (cf. Section 1.3).

By [10, Theorems 21 and 23], the lifting of a set $X$ can be regarded both as the free pointed dcpo on $X$ and as the free subsingleton complete poset on $X$. In our predicative setting, some care should be taken in formulating these statements. We do not go into the details here and instead refer the interested reader to [10].

5 PCF and its operational semantics

This section formally defines the types and terms of PCF as well as the small-step operational semantics. It should be regarded as a formal counterpart to the informal introduction to PCF in Section 1.1.1.

To avoid dealing with free and bound variables (in the formalisation), we opt to work in the combinatory version of PCF, as originally presented by Scott [24]. We note that it is possible to represent every closed $\lambda$-term in terms of combinators by a well-known technique [15, Section 2C].

We inductively define combinatory PCF as follows.

Definition 30** (type).**

The PCF types are inductively defined as:

$\iota$* is a type, the base type;* 2. 2.

for every two types $\sigma$ and $\tau$, there is a function type $\sigma\Rightarrow\tau$.

As usual, $\Rightarrow$ will be right associative, so we write $\sigma\Rightarrow\tau\Rightarrow\rho$ for $\sigma\Rightarrow(\tau\Rightarrow\rho)$.

Definition 31** (term).**

The PCF terms of PCF type $\sigma$ are inductively generated by:

$t:\iota$

${\mathsf{zero}}\text{ of type }\iota$

**   **

$t:\iota$

${\operatorname{\mathsf{succ}}}\text{ of type }\iota\Rightarrow\iota$

---

$t:\iota$

$\operatorname{\mathsf{pred}}\text{ of type }\iota\Rightarrow\iota$

**   **

$t:\iota$

${\operatorname{\mathsf{ifz}}}\text{ of type }{\iota\Rightarrow\iota\Rightarrow\iota\Rightarrow\iota}$

---

$t:\iota$

${\operatorname{\mathsf{k}}_{\sigma,\tau}}\text{ of type }\sigma\Rightarrow\tau\Rightarrow\sigma$

**   **

$t:\iota$

${\operatorname{\mathsf{s}}_{\sigma,\tau,\rho}}\text{ of type }(\sigma\Rightarrow\tau\Rightarrow\rho)\Rightarrow\break(\sigma\Rightarrow\tau)\Rightarrow\sigma\Rightarrow\rho$

---

$t:\iota$

${\operatorname{\mathsf{fix}}_{\sigma}}\text{ of type }(\sigma\Rightarrow\sigma)\Rightarrow\sigma$

**   **

$s\text{ of type }\sigma\Rightarrow\tau$         $t\text{ of type }\tau$

$(st)\text{ of type }\tau$

---

We will often drop the parentheses in the final clause, as well as the PCF type subscripts in ${\operatorname{\mathsf{k}}_{\sigma,\tau}}$, ${\operatorname{\mathsf{s}}_{\sigma,\tau,\rho}}$ and ${\operatorname{\mathsf{fix}}_{\sigma}}$. Finally, we employ the convention that the parentheses associate to the left, i.e. we write $rst$ for $(rs)t$.

Definition 32** (numeral).**

For any $n:\mathsf{N}$, let us write $\underline{n}$ for the $n$th PCF numeral, defined inductively as:

[TABLE]

To define the small-step operational semantics of PCF, we first define the following inductive type.

Definition 33** **(smallstep',

smallstep).

Define the small-step pre-relation $\mathbin{\widetilde{\triangleright}}$ of type

[TABLE]

as the inductive family generated by:

$f\mathbin{\widetilde{\triangleright}}g$

$\operatorname{\mathsf{pred}}\underline{0}\mathbin{\widetilde{\triangleright}}\underline{0}$

**   **

$f\mathbin{\widetilde{\triangleright}}g$

$\operatorname{\mathsf{pred}}\underline{n+1}\mathbin{\widetilde{\triangleright}}\underline{n}$

**   **

$f\mathbin{\widetilde{\triangleright}}g$

$\operatorname{\mathsf{ifz}}s\,t\,\underline{0}\mathbin{\widetilde{\triangleright}}s$

**   **

$f\mathbin{\widetilde{\triangleright}}g$

$\operatorname{\mathsf{ifz}}s\,t\,\underline{n+1}\mathbin{\widetilde{\triangleright}}t$

---

$f\mathbin{\widetilde{\triangleright}}g$

${\operatorname{\mathsf{k}}}st\mathbin{\widetilde{\triangleright}}s$

**   **

$f\mathbin{\widetilde{\triangleright}}g$

${\operatorname{\mathsf{s}}}fgt\mathbin{\widetilde{\triangleright}}ft(gt)$

**   **

$f\mathbin{\widetilde{\triangleright}}g$

$\operatorname{\mathsf{fix}}f\mathbin{\widetilde{\triangleright}}f(\operatorname{\mathsf{fix}}f)$

**   **

$f\mathbin{\widetilde{\triangleright}}g$

$ft\mathbin{\widetilde{\triangleright}}gt$

---

$s\mathbin{\widetilde{\triangleright}}t$

$\operatorname{\mathsf{succ}}s\mathbin{\widetilde{\triangleright}}\operatorname{\mathsf{succ}}t$

**   **

$s\mathbin{\widetilde{\triangleright}}t$

$\operatorname{\mathsf{pred}}s\mathbin{\widetilde{\triangleright}}\operatorname{\mathsf{pred}}t$

**   **

$r\mathbin{\widetilde{\triangleright}}r^{\prime}$

$\operatorname{\mathsf{ifz}}s\,t\,r\mathbin{\widetilde{\triangleright}}\operatorname{\mathsf{ifz}}s\,t\,r^{\prime}$

---

We have been unable to prove that $s\mathbin{\widetilde{\triangleright}}t$ is a proposition for every suitable PCF terms $s$ and $t$. The difficulty is that one cannot perform induction on both $s$ and $t$. However, conceptually, $s\mathbin{\widetilde{\triangleright}}t$ should be a proposition, as (by inspection of the definition), there is at most one way by which we obtained $s\mathbin{\widetilde{\triangleright}}t$. Moreover, for technical reasons that will become apparent later, we really want $\mathbin{\widetilde{\triangleright}}$ to be propostion-valued.

We solve the problem by defining the small-step relation $\mathbin{\triangleright}$ as the propositional truncation of $\mathbin{\widetilde{\triangleright}}$, i.e. $s\mathbin{\triangleright}t\vcentcolon\mspace{-1.2mu}\equiv\|s\mathbin{\widetilde{\triangleright}}t\|$.

Remark 34*.*

Benedikt Ahrens pointed out that in an impredicative framework, one could use propositional resizing and an impredicative encoding, i.e. by defining $\mathbin{\triangleright}$ as a $\Pi$-type of all suitable proposition-valued relations. This is similar to the situation in set theory, where one would define $\mathbin{\triangleright}$ as an intersection. Specifically, say that a relation

[TABLE]

is suitable if it closed under all the clauses of Definition 33, i.e. $R\left(\iota,\operatorname{\mathsf{pred}}\underline{0},\underline{0}\right)$, $R\left(\iota,\operatorname{\mathsf{pred}}\underline{n+1},\underline{n}\right)$, etc. are all inhabited. We could define $s\mathbin{\triangleright}_{\text{impred}}t\vcentcolon\mspace{-1.2mu}\equiv\prod_{R\text{ suitable}}R(\sigma,s,t)$. But notice the increase in universe level:

[TABLE]

So because of this increase, $\mathbin{\triangleright}_{\text{impred}}$ itself is not one of the suitable relations. Therefore $\mathbin{\triangleright}_{\text{impred}}$ does not satisfy the appropriate universal property in being the least relation closed under the clauses in Definition 33. With propositional resizing we could resize $\mathbin{\triangleright}_{\text{impred}}$ to a $\mathcal{U}_{0}$-valued relation satisfying the appropriate universal property. The advantage of using the propositional truncation above is that it does satisfy the right universal property even without propositional resizing.

Let $R:X\to X\to\Omega$ be a relation on a type $X$. We might try to define the reflexive transitive closure $R_{\ast}$ of $R$ as an inductive type, generated by three constructors:

[TABLE]

But $R_{\ast}$ is not necessarily proposition-valued, even though $R$ is. This is because we might add a pair $(x,y)$ to $R_{\ast}$ in more than one way, for example, once by an instance of $\mathsf{extend}$ and once by an instance of $\mathsf{trans}$. Thus, we are led to the following definition.

Definition 35** **(refl_trans_clos,

refl_trans_clos_hrel).

Let $R:X\to X\to\Omega$ be a relation on a type $X$. We define the reflexive transitive closure $R^{\ast}$ of $R$ by $xR^{\ast}y\vcentcolon\mspace{-1.2mu}\equiv\left\|xR_{\ast}y\right\|$, where $R_{\ast}$ is as above.

It is not hard to show that $R^{\ast}$ is the least reflexive and transitive proposition-valued relation that extends $R$, so $R^{\ast}$ satisfies the appropriate universal property (refl_trans_clos_univprop).

Some properties of $\mathbin{\triangleright}$ reflect onto $\mathbin{\triangleright}^{\ast}$ as the following lemma shows.

Lemma 36**.**

Let $r^{\prime},r,s$ and $t$ be PCF terms of type $\iota$. If $r^{\prime}\mathbin{\triangleright}^{\ast}r$, then

$\operatorname{\mathsf{succ}}r^{\prime}\mathbin{\triangleright}^{\ast}\operatorname{\mathsf{succ}}r$; 2. 2.

$\operatorname{\mathsf{pred}}r^{\prime}\mathbin{\triangleright}^{\ast}\operatorname{\mathsf{pred}}r$; 3. 3.

$\operatorname{\mathsf{ifz}}s\,t\,r^{\prime}\mathbin{\triangleright}^{\ast}\operatorname{\mathsf{ifz}}s\,t\,r$.

Moreover, if $f$ and $g$ are PCF terms of type $\sigma\Rightarrow\tau$ and $f\mathbin{\triangleright}^{\ast}g$, then $ft\mathbin{\triangleright}^{\ast}gt$ for any PCF term $t$ of type $\sigma$.

• Proof (succ_refltrans_smallstep, pred_refltrans_smallstep, ifz_refltrans_smallstep, app_refltrans_smallstep). We only prove (1) the rest is similar. Suppose $r^{\prime}\mathbin{\triangleright}^{\ast}r^{\prime}$. Since $\operatorname{\mathsf{succ}}r^{\prime}\mathbin{\triangleright}^{\ast}\operatorname{\mathsf{succ}}r$ is a proposition, we may assume that we actually have a term $p$ of type $r^{\prime}\mathbin{\triangleright}_{\ast}r^{\prime}$. Now we can perform induction on $p$. The cases were $p$ is formed using $\mathsf{refl}$ or $\mathsf{trans}$ are easy. If $p$ is formed by $\mathsf{extend}$, then we get a term of type $r\mathbin{\triangleright}r^{\prime}\equiv\|r\widetilde{\mathbin{\triangleright}}r^{\prime}\|$. Again, as we are proving a proposition, we may suppose the existence of a term of type $r\widetilde{\mathbin{\triangleright}}r^{\prime}$. By Definition 33, we then get $\operatorname{\mathsf{succ}}r^{\prime}\widetilde{\mathbin{\triangleright}}\operatorname{\mathsf{succ}}r$. This in turn yields, $\operatorname{\mathsf{succ}}r^{\prime}\mathbin{\triangleright}\operatorname{\mathsf{succ}}r$ and finally we use $\mathsf{extend}$ to get the desired $\operatorname{\mathsf{succ}}r^{\prime}\mathbin{\triangleright}^{\ast}\operatorname{\mathsf{succ}}r$. ∎

6 The Scott model of PCF using the lifting monad

Next, we wish to give a denotational semantics for PCF, namely the Scott model, as explained in Definition 1.1.2. We recall that the idea is to assign some mathematical structure to each PCF type. The PCF terms are then interpreted as elements of the structure.

Definition 37** (denotational_semantics_type).**

Inductively assign to each PCF type $\sigma$ a dcpo with $\bot$ as follows:

$\llbracket\iota\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\operatorname{\mathcal{L}}(\mathsf{N})$; 2. 2.

$\llbracket\sigma\Rightarrow\tau\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\llbracket\tau\rrbracket^{\llbracket\sigma\rrbracket}$.

Recall that if $D$ and $E$ are dcpos with $\bot$, then $E^{D}$ is the dcpo with $\bot$ of dcpo morphisms from $D$ to $E$, with pointwise ordering and pointwise least upper bounds.

Next, we interpret PCF terms as elements of these dcpos with $\bot$, for which we will need that $\operatorname{\mathcal{L}}$ is a monad (with unit $\eta$) and (in particular) a functor (recall Theorem 24 and Remark 28).

Definition 38** (denotational_semantics_terms).**

Define for each PCF term $t$ of PCF type $\sigma$ a term $\llbracket t\rrbracket$ of type $\llbracket\sigma\rrbracket$, by the following inductive clauses:

$\llbracket\mathsf{zero}\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\eta(0)$; 2. 2.

$\llbracket\operatorname{\mathsf{succ}}\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\operatorname{\mathcal{L}}(s)$, where $s:\mathsf{N}\to\mathsf{N}$ is the successor function; 3. 3.

$\llbracket\operatorname{\mathsf{pred}}\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\operatorname{\mathcal{L}}(p)$, where $p:\mathsf{N}\to\mathsf{N}$ is the predecessor function; 4. 4.

$\llbracket\operatorname{\mathsf{ifz}}\rrbracket:\llbracket\iota\Rightarrow\iota\Rightarrow\iota\Rightarrow\iota\rrbracket$* is defined using the Kleisli extension as: $\lambda x,y.\left(\chi_{x,y}\right)^{\#}$, where*

[TABLE] 5. 5.

$\llbracket\operatorname{\mathsf{k}}\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\lambda x,y.x$; 6. 6.

$\llbracket\operatorname{\mathsf{s}}\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\lambda f,g,x.(f(x))(g(x))$; 7. 7.

$\llbracket\operatorname{\mathsf{fix}}\rrbracket\vcentcolon\mspace{-1.2mu}\equiv\mu$, where $\mu$ is the least fixed point operator from Theorem 16.

Remark 39*.*

Of course, there are some things to be proved here. Namely, $\llbracket\operatorname{\mathsf{succ}}\rrbracket,\llbracket\operatorname{\mathsf{pred}}\rrbracket,\dots,\llbracket\operatorname{\mathsf{fix}}\rrbracket$ all need to be dcpo morphisms. In the case of $\llbracket\operatorname{\mathsf{succ}}\rrbracket$ and $\llbracket\operatorname{\mathsf{pred}}\rrbracket$, we simply appeal to Theorem 27 and Remark 28. For $\llbracket\operatorname{\mathsf{fix}}\rrbracket$, this is Theorem 16. The continuity of $\llbracket\operatorname{\mathsf{k}}\rrbracket,\llbracket\operatorname{\mathsf{s}}\rrbracket$ and $\llbracket\operatorname{\mathsf{ifz}}\rrbracket$ can be verified directly, as done in the formalisation (k_dcpo, s_dcpo, lifted_ifz). It is however, unenlightning and tedious, so we omit the details here.

As a first result about our denotational semantics, we show that the PCF numerals have a canonical interpretation in the denotational semantics.

Proposition 40**.**

For every natural number $n$, we have $\llbracket\underline{n}\rrbracket=\eta(n)$.

• Proof (denotational_semantics_numerals). We proceed by induction on $n$. The $n\equiv 0$ case is by definition of $\llbracket\underline{0}\rrbracket$. Suppose $\llbracket\underline{m}\rrbracket=\eta(m)$ for a natural number $m$. Then,

[TABLE]

as desired. ∎

7 Soundness and computational adequacy

In this section we show that the denotational semantics and the operational semantics defined above are “in sync”, as expressed by soundness and computational adequacy (cf. Section 1.1.2).

Theorem 41** (Soundness).**

Let $s$ and $t$ be any PCF terms of PCF type $\sigma$. If $s\mathbin{\triangleright}^{\ast}t$, then $\llbracket s\rrbracket=\llbracket t\rrbracket$.

• Proof (soundness). Since the carriers of dcpos are defined to be sets, the type $\llbracket s\rrbracket=\llbracket t\rrbracket$ is a proposition. Therefore, we can use induction on the derivation of $s\mathbin{\triangleright}^{\ast}t$. We use the Kleisli monad laws in proving some of the cases. For example, one step is to prove that

[TABLE]

This may be proved by the following chain of equalities:

[TABLE]

Ideally, we would like a converse to soundness. However, this is not possible, as for example, ${\llbracket\operatorname{\mathsf{k}}{\mathsf{zero}}\rrbracket}={\llbracket\operatorname{\mathsf{k}}(\operatorname{\mathsf{succ}}(\operatorname{\mathsf{pred}}\mathsf{zero}))\rrbracket}$, but neither ${\operatorname{\mathsf{k}}\mathsf{zero}}\mathbin{\triangleright}^{\ast}{\operatorname{\mathsf{k}}(\operatorname{\mathsf{succ}}(\operatorname{\mathsf{pred}}\mathsf{zero}))}$ nor ${\operatorname{\mathsf{k}}(\operatorname{\mathsf{succ}}(\operatorname{\mathsf{pred}}\mathsf{zero}))}\mathbin{\triangleright}^{\ast}{\operatorname{\mathsf{k}}\mathsf{zero}}$ holds. We do, however, have the following.

Theorem 42** (Computational adequacy).**

Let $t$ be a PCF term of PCF type $\iota$. Then,

[TABLE]

Equivalently, for every $n:\mathsf{N}$, it holds that $\llbracket t\rrbracket=\llbracket\underline{n}\rrbracket$ implies $t\mathbin{\triangleright^{\ast}}{\underline{n}}$.

We do not prove computational adequacy directly, as, unlike soundness, it does not allow for a straightforward proof by induction. Instead, we use the standard technique of logical relations [25, Chapter 7] and obtain the result as a direct corollary of Lemma 49.

Definition 43** (adequacy_relation).**

For every PCF type $\sigma$, define a relation

[TABLE]

by induction on $\sigma$:

$tR_{\iota}d\vcentcolon\mspace{-1.2mu}\equiv\prod_{p:\operatorname{\mathsf{isdefined}}(d)}t\mathbin{\triangleright}^{\ast}\underline{\operatorname{\mathsf{value}}(d)(p)}$; 2. 2.

sR_{\tau\Rightarrow\rho}f\vcentcolon\mspace{-1.2mu}\equiv\prod_{t:\text{PCF terms of type \tau}}\prod_{d:\llbracket\tau\rrbracket}\left(tR_{\tau}d\to stR_{\rho}f(d)\right).

We sometimes omit the type subscript $\sigma$ in $R_{\sigma}$.

Lemma 44**.**

Let $s$ and $t$ be PCF terms of type $\sigma$ and let $d$ be an element of $\llbracket\sigma\rrbracket$. If $s\mathbin{\triangleright}^{\ast}t$ and $tR_{\sigma}d$, then $sR_{\sigma}d$.

• Proof (adequacy_step). By induction on $\sigma$, making use of the last part of Lemma 36. ∎

Lemma 45**.**

For $t$ equal to $\mathsf{zero},{\operatorname{\mathsf{succ}}},{\operatorname{\mathsf{pred}}},{\operatorname{\mathsf{ifz}}},{\operatorname{\mathsf{k}}}$ or ${\operatorname{\mathsf{s}}}$, we have: $tR\llbracket t\rrbracket$.

• *Proof *(adequacy_zero, adequacy_succ, adequacy_pred, adequacy_ifz, adequacy_k,

adequacy_s).. By the previous lemma and Lemma 36. ∎

Next, we wish to extend the previous lemma the case where $t\equiv{\operatorname{\mathsf{fix}}_{\sigma}}$ for any PCF type $\sigma$. This is slightly more complicated and we need two intermediate lemmas. Only the second requires a non-trivial proof.

Lemma 46**.**

Let $\sigma$ be a PCF type and let $\bot$ be the least element of $\llbracket\sigma\rrbracket$. Then, $tR_{\sigma}\bot$ for any PCF term $t$ of type $\sigma$.

• Proof (adequacy_bottom). By induction on $\sigma$. For the base type, this holds vacuously. For function types, it follows by induction hypothesis and the pointwise ordering. ∎

Lemma 47**.**

The logical relation is closed under directed suprema. That is, for every PCF term $t$ of type $\sigma$ and every directed family $d:I\to\llbracket\sigma\rrbracket$, if $tR_{\sigma}d_{i}$ for every $i:I$, then $tR_{\sigma}\bigsqcup_{i:I}d_{i}$.

• Proof (adequacy_lubs). This proof is somewhat different from the classical proof, so we spell out the details. We prove the lemma by induction on $\sigma$.

The case when $\sigma$ is a function type is easy, because least upper bounds are calculated pointwise and so it reduces to an application of the induction hypothesis. We concentrate on the case when $\sigma\equiv\iota$ instead.

Recall that $\bigsqcup_{i:I}d_{i}$ is given by $\left(\left\|\sum_{i:I}\operatorname{\mathsf{isdefined}}(d_{i})\right\|,\varphi\right)$, where $\varphi$ is the factorisation of

[TABLE]

through $\left\|\sum_{i:I}\operatorname{\mathsf{isdefined}}(d_{i})\right\|$.

We are tasked with proving that $t\mathbin{\triangleright}^{\ast}\underline{\varphi(p)}$ for every $p:\operatorname{\mathsf{isdefined}}\left(\bigsqcup_{i:I}d_{i}\right)$. So assume that $p:\left\|\sum_{i:I}\operatorname{\mathsf{isdefined}}(d_{i})\right\|$. Since we are trying to prove a proposition (as $\mathbin{\triangleright}^{\ast}$ is proposition-valued), we may actually assume that we have $(j,p_{j}):\sum_{i:I}\operatorname{\mathsf{isdefined}}(d_{i})$. By definition of $\varphi$ we have: $\varphi(p)=\operatorname{\mathsf{value}}(d_{j})(p_{j})$ and by assumption we know that $t\mathbin{\triangleright}^{\ast}\underline{\operatorname{\mathsf{value}}(d_{j})(p_{j})}$, so we are done. ∎

Lemma 48**.**

For every PCF type $\sigma$, we have $\operatorname{\mathsf{fix}}_{\sigma}R_{(\sigma\Rightarrow\sigma)\Rightarrow\sigma}\llbracket\operatorname{\mathsf{fix}}_{\sigma}\rrbracket$.

• Proof (adequacy_fixp). Let $t$ be a PCF term of type $\sigma\Rightarrow\sigma$ and let $f:\llbracket\sigma\Rightarrow\sigma\rrbracket$ such that $tR_{\sigma\Rightarrow\sigma}f$. We are to prove that $\operatorname{\mathsf{fix}}tR_{\sigma}\mu(f)$.

By definition of $\mu$ and the previous lemma, it suffices to prove that $\operatorname{\mathsf{fix}}tR_{\sigma}f^{n}(\bot)$ where $\bot$ is the least element of $\llbracket\sigma\rrbracket$ for every natural number $n$. We do so by induction on $n$.

The base case is an application of Lemma 46.

Now suppose that $\operatorname{\mathsf{fix}}tR_{\sigma}f^{m}(\bot)$. Then, using $tR_{\sigma\Rightarrow\sigma}f$, we find: $t(\operatorname{\mathsf{fix}}t)R_{\sigma}f(f^{m}(\bot))$. Hence, by Lemma 44, we obtain the desired $\operatorname{\mathsf{fix}}tR_{\sigma}f^{m+1}(\bot)$, completing our proof by induction. ∎

Lemma 49** (Fundamental Theorem).**

For every PCF term $t$ of type $\sigma$, we have $tR_{\sigma}\llbracket t\rrbracket$.

• Proof (adequacy_allterms). The proof is by induction on $t$. The base cases are taken care of by Lemma 45 and the previous lemma. For the inductive step, suppose $t$ is a PCF term of type $\sigma\Rightarrow\tau$. By induction hypothesis, $tsR_{\tau}\llbracket ts\rrbracket$ for every PCF term $s$ of type $\sigma$, but $\llbracket ts\rrbracket\equiv\llbracket t\rrbracket\llbracket s\rrbracket$, so we are done. ∎

Computational adequacy is now a direct corollary of Lemma 49.

• Proof of computational adequacy (adequacy, adequacy_alt, alt_adequacy). Take $\sigma$ to be the base type $\iota$ in Lemma 49. ∎

Using computational adequacy to compute.

An interesting use of computational adequacy is that it allows one to argue semantically to obtain results about termination (i.e. reduction to a numeral) in PCF. Classically, every PCF program of type $\iota$ either terminates or it does not. From a constructive point of view, we wait for a program to terminate, with no a priori knowledge of termination. The waiting could be indefinite. Less naively, we could limit the number of computation steps to avoid indefinite waiting, with an obvious shortcoming: how many steps are enough? Instead, one could use computational adequacy to compute as follows.

Let $\sigma$ be a PCF type. A functional of type $\sigma$ is an element of $\llbracket\sigma\rrbracket$. By induction on PCF types, we define when a functional is said to be total:

a functional $i$ of type $\iota$ is total if $i=\llbracket\underline{n}\rrbracket$ for some natural number $n$; 2. 2.

a functional $f$ of type $\sigma\Rightarrow\tau$ is total if it maps total functionals to total functionals, viz. $f(d)$ is a total functional of type $\tau$ for every total functional $d$ of type $\sigma$.

Now, let $s$ be a PCF term of type $\sigma_{1}\Rightarrow\sigma_{2}\Rightarrow\dots\Rightarrow\sigma_{n}\Rightarrow\iota$. If we can prove that $\llbracket s\rrbracket$ is total, then computational adequacy lets us conclude that for all total inputs $\llbracket t_{1}\rrbracket:\llbracket\sigma_{1}\rrbracket,\dots,\llbracket t_{n}\rrbracket:\llbracket\sigma_{n}\rrbracket$, the term $s(t_{1},\dots,t_{n})$ reduces to the numeral representing $\llbracket s\rrbracket(\llbracket t_{1}\rrbracket,\dots,\llbracket t_{n}\rrbracket)$. Thus, the semantic proof of totality plays the role of “enough steps”. Of course, this still requires us to prove that $\llbracket s\rrbracket$ is total, which may be challenging. But the point is that we can use domain-theoretic arguments to prove this about the denotation $\llbracket s\rrbracket$, whereas in a direct proof of termination we would only have the operational semantics available for our argument.

8 Semidecidable propositions and PCF terms of base type

In this section we characterise those propositions that arise from the PCF interpretation, in the following sense. Every PCF term $t$ of base type $\iota$ gives rise to a proposition via the Scott model, namely $\operatorname{\mathsf{isdefined}}(\llbracket t\rrbracket)$. We wish to show that such propositions are semidecidable, which we define now. For ease of notation, we write $\exists$ for the propositional truncation of $\Sigma$.

Definition 50**.**

A proposition $Q$ is semidecidable if it is equivalent to $\exists_{n_{1}:\mathsf{N}}\cdots\exists_{n_{k}:\mathsf{N}}P(n_{1},\dots,n_{k})$ where $k$ is some natural number and $P:\mathsf{N}^{k}\to\Omega$ is a proposition-valued family such that $P(m_{1},\dots,m_{k})$ is decidable for every $(m_{1},\dots,m_{k}):\mathsf{N}^{k}$.

We will prove our goal that $\operatorname{\mathsf{isdefined}}(\llbracket t\rrbracket)$ is semidecidable by showing that it is logically equivalent to $\exists_{n:\mathsf{N}}\exists_{k:\mathsf{N}}\,t\mathbin{\triangleright}^{k}{\underline{n}}$ and by proving that $t\mathbin{\triangleright}^{k}{\underline{n}}$ is decidable. Here $t\mathbin{\triangleright}^{k}{\underline{n}}$ says that $t$ reduces to $\underline{n}$ in at most $k$ steps. A first step towards this is the following, which is a consequence of soundness and computational adequacy.

Lemma 51**.**

Let $t$ be a PCF term of type $\iota$. We have the following logical equivalences

[TABLE]

• Proof (char_pcf_propositions). We start by proving the first logical equivalence. The second then follows from the fact that $\operatorname{\mathsf{isdefined}}(\llbracket t\rrbracket)$ is a proposition. Suppose $p$ is of type $\operatorname{\mathsf{isdefined}}(\llbracket t\rrbracket)$. By computational adequacy, we find that $t\mathbin{\triangleright}^{\ast}{\underline{\operatorname{\mathsf{value}}(\llbracket t\rrbracket)(p)}}$, so we are done.

Conversely, suppose that we are given a natural number $n$ such that $t\mathbin{\triangleright}^{\ast}\underline{n}$. Soundness and Proposition 40 then yield $\llbracket t\rrbracket=\eta(n)$. Now $\star:\operatorname{\mathsf{isdefined}}(\eta(n))$, so we may transport along the equality to get an element of $\operatorname{\mathsf{isdefined}}(\llbracket t\rrbracket)$. ∎

In order to characterise the propositions arising from PCF terms of base type as semidecidable, we wish to prove that $t\mathbin{\triangleright}^{\ast}\underline{n}$ is semidecidable for every PCF term $t$ of type $\iota$ and natural number $n$. We do so by proving some more general results, which we present in Section 8.1 and Section 8.2. Here, we outline our general strategy and highlight the main theorems and their applications to the problem at hand.

Given any (proposition-valued) relation $R$ on a type $X$, we can define the $k$-step reflexive transitive closure $R^{k}$ of $R$ and prove that $xR^{*}y$ if and only if $\exists_{k:\mathsf{N}}xR^{k}y$. Thus we obtain the following (intermediate) result.

Lemma 52**.**

For every PCF term $t$ of type $\iota$, we have:

[TABLE]

• Proof (char_pcf_propositions'). This follows from Lemma 51 and Lemma 57. ∎

Thus, to prove that $s\mathbin{\triangleright^{\ast}}t$ is semidecidable, it suffices to show that $s\mathbin{\triangleright}^{k}t$ is decidable for every natural number $k$. To this end, we prove the following in Section 8.1.

Theorem** (Theorem 61).**

Let $R$ be relation on a type $X$. If

$X$* has decidable equality;* 2. 2.

$R$* is single-valued;* 3. 3.

$\sum_{y:X}xRy$* is decidable for every $x:X$;*

then, the $k$-step reflexive transitive closure $R^{k}$ of $R$ is decidable for every natural number $k$.

Thus, $s\mathbin{\triangleright}^{k}t$ is decidable if it satisfies the assumptions (1)–(3). Assumptions (2) and (3) can be verified by inspection of the small-step operational semantics once (1) has been proved.

Hence, we are to prove that the type of PCF terms has decidable equality. This can be done fairly directly by induction (as pointed out by one of the anonymous referees). However, we take it as an opportunity to study (in Section 8.2) a more general and powerful result on indexed $\mathsf{W}$-types (see Theorem 73), which is interesting in its own right. For now, we take it as proved that the PCF terms have decidable equality and continue our study of propositions coming from PCF terms at the base type.

Theorem 53**.**

The propositions that arise from PCF terms $t$ of type $\iota$ are all semidecidable, as witnessed by the following logical equivalence:

[TABLE]

and the decidability of $t\mathbin{\triangleright}^{k}\underline{n}$.

Given this theorem, it is natural to ask whether we can construct the Scott model of PCF using a restricted version of the lifting monad. Write $\Omega_{\textup{sd}}$ for the type of propositions that are semidecidable. Theorem 53 says that the map

[TABLE]

factors through $\Omega_{\textup{sd}}$. Thus, could we also have constructed the Scott model of PCF using the restricted lifting $\operatorname{\mathcal{L}_{\textup{sd}}}(X)\vcentcolon\mspace{-1.2mu}\equiv\sum_{P:\Omega_{\textup{sd}}}(P\to X)$?

Of course, $\operatorname{\mathcal{L}_{\textup{sd}}}(X)$ is not a dcpo, because, recalling our construction of suprema in $\operatorname{\mathcal{L}}(X)$, given a directed family $u:I\to\operatorname{\mathcal{L}_{\textup{sd}}}(X)$, the proposition $\left\|\sum_{i:I}\operatorname{\mathsf{isdefined}}\left(u_{i}\right)\right\|$ need not be semidecidable. However, one might think that $\operatorname{\mathcal{L}_{\textup{sd}}}(X)$ still has suprema of $\mathsf{N}$-indexed directed families (which would suffice for the Scott model), but proving this requires an instance of the axiom of countable choice, cf. [18, Theorem 5.34] and [12, Theorem 5]. Moreover, $\operatorname{\mathcal{L}_{\textup{sd}}}$ is a monad if and if only a particular choice principle (which is implied by countable choice) holds, see [12, Theorem 3] and [18, Section 5.8]. In fact, this choice principle is the one discussed in Section 1.3; [18, Theorem 5.28] proves that if $X$ is a set then $\operatorname{\mathcal{L}_{\textup{sd}}}(X)$ is equivalent to the quotiented delay monad.

Again, as pointed out in Section 1.3, the problem is that this choice principle cannot be proved in constructive univalent type theory.

8.1 Decidability of the $k$-step reflexive

transitive closure of a relation

In this section we provide sufficient conditions on a relation for its $k$-step reflexive transitive closure to be decidable. The purpose of this section is to prove Theorem 61, whose use we have explained above.

Definition 54** (hrel).**

A relation on $X$ is a term of type $X\to X\to\Omega$.

Definition 55** **(refltransclos_step,

refltransclos_step_hrel).

Let $R$ be a relation on a type $X$. We wish to define the $k$-step reflexive transitive closure of $R$. As in Definition 35, we want this to be proposition-valued again. Therefore, we proceed as follows. For any natural number $k$, define $xR_{k}y$ by induction on $k$:

$xR_{0}y\vcentcolon\mspace{-1.2mu}\equiv x=y$; 2. 2.

$xR_{k+1}z\vcentcolon\mspace{-1.2mu}\equiv\sum_{y:X}xRy\times yR_{k}z$.

The $k$-step reflexive transitive closure $R^{k}$ of $R$ is now defined as the relation on $X$ given by ${xR^{k}y\vcentcolon\mspace{-1.2mu}\equiv\|xR_{k}y\|}$.

We wish to prove that $xR^{\ast}y$ if and only if $\left\|\sum_{k:\mathsf{N}}xR^{k}y\right\|$. The following lemma is the first step towards that.

Lemma 56**.**

Let $R$ be a relation on $X$. Recall the untruncated reflexive transitive closure $R_{\ast}$ from Definition 35. We have a logical equivalence for every $x,y$ in $X$:**

[TABLE]

• Proof (stepleftequiv, left_regular_equiv). Define $xR^{\prime}y$ inductively by:

[TABLE]

It is not hard to verify that $R^{\prime}$ is reflexive, transitive and that it extends $R$. Using this, one shows that $xR^{\prime}y$ and $xR_{\ast}y$ are logically equivalent for every $x,y:X$. Now one easily proves $\prod_{k:\mathsf{N}}(xR_{k}y\to xR^{\prime}y)$ by induction on $k$. This yields $\left(\sum_{k:\mathsf{N}}xR_{k}y\right)\to xR^{\prime}y$. The converse is also easily established. Thus, $xR^{\prime}y$ and $\sum_{k:\mathsf{N}}xR_{k}y$ are logically equivalent, finishing the proof. ∎

The next lemma extends the previous one to the propositional truncations.

Lemma 57**.**

Let $R$ be a relation on $X$. For every $x,y:X$, we have a logical equivalence:

[TABLE]

• Proof (stepleftequiv_hrel, left_regular_equiv).. Let $x$ and $y$ be in $X$. By the previous lemma and functoriality of propositional truncation, we have

[TABLE]

But the latter is equivalent to $\left\|\sum_{k:\mathsf{N}}\left\|xR_{k}y\right\|\right\|\equiv\left\|\sum_{k:\mathsf{N}}xR^{k}y\right\|$ by [28, Theorem 7.3.9]. This may also be proved directly, as done in the formalisation. ∎

Definition 58** (is_singlevalued).**

A relation $R$ on $X$ is said to be single-valued if for every $x,y,z:X$ with $xRy$ and $xRz$ we have $y=z$.

Definition 59** (isdecidable_hrel).**

A relation $R$ on $X$ is said to be decidable if the type $xRy$ is decidable for every $x$ and $y$ in $X$.

Lemma 60**.**

Let $X$ be a type. If $X$ is decidable, then so is $\|X\|$.

• Proof (decidable_ishinh). Suppose that $X$ is decidable. Then there are two cases to consider. Either we have $x:X$ or $\lnot X$. If we have $x:X$, then obviously we have $|x|:\|X\|$.

So suppose that $\lnot X$. We claim that $\lnot\|X\|$. Assuming $\|X\|$, we must find a term of type $\mathsf{0}$. But $\mathsf{0}$ is a proposition, so we may actually assume that we have $x:X$. Using $\lnot X$, we then obtain $\mathsf{0}$, as desired. ∎

Theorem 61**.**

Let $R$ be relation on a type $X$. If

$X$* has decidable equality;* 2. 2.

$R$* is single-valued;* 3. 3.

$\sum_{y:X}xRy$* is decidable for every $x:X$;*

then, the $k$-step reflexive transitive closure $R^{k}$ of $R$ is decidable for every natural number $k$.

• Proof (decidable_step). Suppose $X$ and $R$ satisfy conditions (1)–(3). By Lemma 60, it suffices to prove that the untruncated version of $R^{k}$, that is $R_{k}$, is decidable by induction on $k$.

For the base case, let $x$ and $y$ be elements of $X$. We need to decide $xR_{0}y$. By definition this means deciding $x=y$, which we can, since $X$ is assumed to have decidable equality.

Now suppose $x$ and $z$ are elements of $X$ and that $aR_{k}b$ is decidable for every $a,b:X$. We need to show that $xR_{k+1}z$ is decidable. By definition this means that we must prove

[TABLE]

to be decidable. By (3), we can decide $\sum_{y:X}xRy$. Obviously, if we have $\lnot\sum_{y:X}xRy$, then $\lnot\eqref{toprovedec}$. So assume that we have $y:X$ such that $xRy$. By induction hypothesis, $yR_{k}z$ is decidable. If we have $yR_{k}z$, then we get $\eqref{toprovedec}$. So suppose that $\lnot yR_{k}z$. We claim that $\lnot\eqref{toprovedec}$. For suppose $\eqref{toprovedec}$, then we obtain $y^{\prime}:X$ with $xRy^{\prime}$ and $y^{\prime}R_{k}z$. But $R$ is single-valued, so $y=y^{\prime}$ and hence, $yR_{k}z$, contradicting our assumption. ∎

8.2 Decidable equality and indexed

$\mathsf{W}$-types

We wish to prove that a certain class of indexed $\mathsf{W}$-types has decidable equality. Indexed $\mathsf{W}$-types are a generalisation of $\mathsf{W}$-types that allows for many-sorted terms. One may consult [28, Section 5.3] for an explanation of regular $\mathsf{W}$-types. The PCF terms form a natural example of an indexed $\mathsf{W}$-type, where the sorts will be the formal types of PCF terms. We apply the general result for indexed $\mathsf{W}$-types to see that the PCF terms have decidable equality.

8.2.1 PCF terms as an indexed $\mathsf{W}$-type

In this section we explain what indexed $\mathsf{W}$-types are and how PCF terms can encoded as such an indexed $\mathsf{W}$-type.

Definition 62** (indexedWtype).**

Let $A$ and $I$ be types and let $B$ be a type family over $A$. Suppose we have $t:A\to I$ and $s:\left(\sum_{a:A}B(a)\right)\to I$. The indexed $\mathsf{W}$-type $\mathsf{W}_{s,t}$ specified by $s$ and $t$ is the inductive type family over $I$ generated by the following constructor:

[TABLE]

We have the following induction principle for indexed $\mathsf{W}$-types. If $E:\prod_{i:I}\left(\mathsf{W}_{s,t}(i)\to\mathcal{U}\right)$, then to prove $\prod_{i:I}\prod_{w:\mathsf{W}_{s,t}(i)}E(i,w)$, it suffices to show that for any $a:A$ and $f:\prod_{b:B(a)}\mathsf{W}_{s,t}(s(a,b))$ satisfying $E(s(a,b),f(b))$ for every $b:B(a)$ (the induction hypothesis), we have a term of type $E(t(a),\mathsf{indexedsup}(a,f))$.

Just as with regular $\mathsf{W}$-types, we can think of indexed $\mathsf{W}$-types as encoding a particular class of inductive types. In this interpretation, $A$ encodes the constructors of the inductive type, whereas $B$ encodes the arity of each constructor. However, each constructor has a “sort” given by $t(a):I$. Given a constructor $a:A$ and a label of an argument $b:B(a)$, the sort of this argument is given by $s(a,b)$.

Example 63**.**

In this example, we show that a fragment of the PCF terms can be encoded as an indexed $\mathsf{W}$-type. One could extend the encoding to capture all PCF terms, but we do not spell out the tedious details here, as a fragment suffices to get the idea across.

The type family $\mathsf{T}$ is inductively defined as:

$\mathsf{zero}$* is a term of type $\iota$;* 2. 2.

$\mathsf{succ}$* is a term of type $\iota\Rightarrow\iota$;* 3. 3.

for every PCF type $\sigma$ and $\tau$, we have a term $\mathsf{app}_{\sigma,\tau}$ of type $(\sigma\Rightarrow\tau)\Rightarrow\sigma\Rightarrow\tau$.

We can encode $\mathsf{T}$ as an indexed $\mathsf{W}$-type. Let us write $\mathsf{2}$ for $\mathsf{1}+\mathsf{1}$ and $0_{\mathsf{2}}$ and $1_{\mathsf{2}}$ for its elements. Take $I$ to be the type of PCF types and put $A\vcentcolon\mspace{-1.2mu}\equiv\mathsf{2}+(I\times I)$. Define $B:A\to\mathcal{U}$ by

[TABLE]

Finally, define $t$ by

[TABLE]

and $s$ by

[TABLE]

on the other elements $s$ is defined as the unique function from $\mathsf{0}$.

One can check that given a PCF type $\sigma:I$, there is a type equivalence $T(\sigma)\simeq W_{s,t}(\sigma)$.

8.2.2 Indexed $\mathsf{W}$-types with decidable equality

We wish to isolate some conditions on the parameters of an indexed $\mathsf{W}$-type that are sufficient to conclude that an indexed $\mathsf{W}$-type has decidable equality. We first need a few definitions before we can state the theorem.

Definition 64** **(WeaklyCompactTypes in [14],

picompact).

A type $X$ is called $\Pi$-compact when every type family $Y$ over $X$ satisfies: if $Y(x)$ is decidable for every $x:X$, then so is the dependent product $\prod_{x:X}Y(x)$.

Example 65** **(picompact_empty,

picompact_unit).

The empty type $\mathsf{0}$ is vacuously $\Pi$-compact. The unit type $\mathsf{1}$ is also easily seen to be $\Pi$-compact. There are also interesting examples of infinite types that are $\Pi$-compact, such as $\mathsf{N}_{\infty}$, the one-point compactification of the natural numbers [14, WeaklyCompactTypes].

We are now in position to state the general theorem about decidable equality on indexed $\mathsf{W}$-types.

Theorem 66**.**

Let $A$ and $I$ be types and $B$ a type family over $A$. Suppose $t:A\to I$ and $s:\left(\sum_{a:A}B(a)\right)\to I$. If $A$ has decidable equality, $B(a)$ is $\Pi$-compact for every $a:A$ and $I$ is a set, then $\mathsf{W}_{s,t}(i)$ has decidable equality for every $i:I$.

The proof of Theorem 66 is quite technical, so we postpone it until Section 8.2.4. Instead, we next describe how to apply the theorem to prove that the PCF terms have decidable equality.

8.2.3 PCF terms have decidable equality

In this section we show that the PCF terms have decidable equality by applying Theorem 66. Before we proceed, we record some useful lemmas.

Lemma 67**.**

Let $X$ and $Y$ be logically equivalent types. The type $X$ is decidable if and only if $Y$ is decidable.

• Proof (decidable_iff). Straightforward. ∎

Definition 68**.**

A type $X$ is called a retract of a type $Y$ if there are maps $s:X\to Y$ (the section) and $r:Y\to X$ (the retraction) such that $\prod_{x:X}r(s(x))=x$.

Lemma 69**.**

Let $X$ be a retract of $Y$. If $Y$ has decidable equality, then so does $X$.

• Proof (isdeceq_retract). Let $r:Y\to X$ and $s:X\to Y$ be respectively the retraction and section establishing $X$ as a retract of $Y$. Let $a,b:X$. Since $Y$ has decidable equality, we can consider two cases: $r(a)=r(b)$ and $r(a)\neq r(b)$. In the first case, we find $a=s(r(a))=s(r(b))=b$. In the second case, we immediately see that $a\neq b$. This finishes the proof. ∎

Lemma 70**.**

The $\Pi$-compact types are closed under binary coproducts.

• Proof (picompact_coprod). Let $X$ and $Y$ be $\Pi$-compact types. Suppose $F$ is a type family over $X+Y$ such that $F(z)$ is decidable for every $z:X+Y$. We must show that $\prod_{z:X+Y}F(z)$ is decidable.

Define $F_{X}:X\to\mathcal{U}$ by $F_{X}(x)\vcentcolon\mspace{-1.2mu}\equiv F(\operatorname{\mathsf{inl}}(x))$ and $F_{Y}:Y\to\mathcal{U}$ as $F_{Y}(y)\vcentcolon\mspace{-1.2mu}\equiv F(\operatorname{\mathsf{inr}}(y))$. By our assumption on $F$, the types $F_{X}(x)$ and $F_{Y}(y)$ are decidable for every $x:X$ and $y:Y$. Hence, since $X$ and $Y$ are assumed to be $\Pi$-compact, the dependent products $\prod_{x:X}F_{X}(x)$ and $\prod_{y:Y}F_{Y}(y)$ are decidable.

Finally, $\prod_{z:X+Y}F(z)$ is logically equivalent to $\prod_{x:X}F_{X}(x)\times\prod_{y:Y}F_{Y}(y)$. Since the product of two decidable types is again decidable, an application of Lemma 67 now finishes the proof. ∎

Finally, let us see how to apply Theorem 66 to see that the PCF terms have decidable equality.

Theorem 71**.**

The PCF terms have decidable equality.

• Proof. As with Example 63, we only spell out the details for the fragment $\mathsf{T}$. Recall that $\mathsf{T}$ may be encoded as a $\mathsf{W}$-type, indexed by the PCF types. Using Example 65 and Lemma 70, we see that $B(a)$ is $\Pi$-compact for every $a:A$. Note that $A$ has decidable equality if $I$ does. So it remains to prove that $I$, the type of PCF types, has decidable equality.

This will be another application of Theorem 66. Define $A^{\prime}\vcentcolon\mspace{-1.2mu}\equiv\mathsf{2}$ and define $B^{\prime}:A^{\prime}\to\mathcal{U}$ by $B^{\prime}(\operatorname{\mathsf{inl}}(\star))\vcentcolon\mspace{-1.2mu}\equiv\mathsf{0}$ and $B^{\prime}(\operatorname{\mathsf{inr}}(\star))\vcentcolon\mspace{-1.2mu}\equiv\mathsf{2}$. Let $t^{\prime}$ and $s^{\prime}$ be the unique functions to $\mathsf{1}$ from $A^{\prime}$ and $\sum_{x:A^{\prime}}B^{\prime}(x)$, respectively. One quickly verifies that the type of PCF types is a retract of $\mathsf{W}_{s^{\prime},t^{\prime}}(\star)$. Observe that $B^{\prime}(x)$ is $\Pi$-compact for every $x:A^{\prime}$ because of Example 65 and Lemma 70. Finally, $\mathsf{1}$ and $A^{\prime}\equiv 2$ clearly have decidable equality, so by Theorem 66 the type $\mathsf{W}_{s^{\prime},t^{\prime}}(\star)$ has decidable equality. Thus, by Lemma 69, so do the PCF types. ∎

8.2.4 Proof of Theorem 66

In this section we prove Theorem 66 by deriving it as a corollary of another result, namely Theorem 73 below. This result seems to have been first established by Jasper Hugunin, who reported on it in a post on the Homotopy Type Theory mailing list [16]. Our proof of Theorem 73 is a simplified written-up account of Hugunin’s Coq code [17, FiberProperties.v].

Definition 72** (Definition 2.4.2 in [28], hfiber).**

Let $f:X\to Y$ be a map. The fiber of $f$ over a point $y:Y$ is

[TABLE]

Theorem 73** (Jasper Hugunin).**

Let $A$ and $I$ be types and $B$ a type family over $A$. Suppose $t:A\to I$ and $s:\left(\sum_{a:A}B(a)\right)\to I$. If $B(a)$ is $\Pi$-compact for every $a:A$ and the fiber of $t$ over $i$ has decidable equality for every $i:I$, then $\mathsf{W}_{s,t}(i)$ also has decidable equality for every $i:I$.

Let us see how to obtain Theorem 66 from Theorem 73.

• Proof of Theorem 66 (using Theorem 73) (indexedWtype_deceq'). Suppose that $A$ has decidable equality and $I$ is a set. We are to show that the fiber of $t$ over $i$ has decidable equality for every $i:I$. Let $i:I$ be arbitrary. Suppose we have $(a,p)$ and $(a^{\prime},p^{\prime})$ in the fiber of $t$ over $i$. Since $A$ has decidable equality, we can decide whether $a$ and $a^{\prime}$ are equal or not. If they are not, then certainly $(a,p)\neq(a^{\prime},p^{\prime})$. If they are, then we claim that the dependent pairs $(a,p)$ and $(a^{\prime},p^{\prime})$ are also equal. If $e:a=a^{\prime}$ is the supposed equality, then it suffices to show that $\operatorname{\mathsf{transport}}^{\lambda x:A.t(x)=i}(e,p)=p^{\prime}$, but both these terms are paths in $I$ and $I$ is a set, so they must be equal. ∎

We now embark on a proof of Theorem 73. For the remainder of this section, let us fix types $A$ and $I$, a type family $B$ over $A$ and maps $t:A\to I$ and $s:\left(\sum_{a:A}B(a)\right)\to I$.

We do not prove the theorem directly. The statement makes it impossible to assume two elements $u,v:\mathsf{W}_{s,t}(i)$ and proceed by induction on both $u$ and $v$. Instead, we will state and prove a more general result that is amenable to a proof by induction. But first, we need more general lemmas and some definitions.

Lemma 74**.**

Let $X$ be a type and let $Y$ be a type family over it. If $X$ is a set, then the right pair function is injective, in the following sense: if $(x,y)=(x,y^{\prime})$ as terms of $\sum_{a:X}Y(a)$, then $y=y^{\prime}$.

• Proof (dec_depeq). Suppose $X$ is a set, $x:X$ and $y,y^{\prime}:Y(x)$ with $e:(x,y)=(x,y^{\prime})$. From $e$, we obtain $e_{1}:x=x$ and $e_{2}:\operatorname{\mathsf{transport}}^{Y}(e_{1},y)=y^{\prime}$. Since $X$ is a set, we must have that $e_{1}=\mathsf{refl}_{x}$, so that from $e_{2}$ we obtain a term of type $y\equiv\operatorname{\mathsf{transport}}^{Y}(\mathsf{refl}_{x},y)=y^{\prime}$, as desired. ∎

Definition 75** (subtrees).**

For each $i:I$, define

[TABLE]

by induction:

[TABLE]

For notational convenience, we will omit the subscript of $\mathsf{sub}$.

Lemma 76**.**

Let $a:A$ and $f,g:\prod_{b:B(a)}\mathsf{W}_{s,t}(s(a,b))$. If the fiber of $t$ over $i$ has decidable equality for every $i:I$, then $\mathsf{indexedsup}(a,f)=\mathsf{indexedsup}(a,g)$ implies $f=g$.

• Proof (subtrees_eq). Suppose $\mathsf{indexesup}(a,f)=\mathsf{indexedsup}(a,g)$. Then

[TABLE]

As $\mathsf{fib}_{t}(i)$ is decidable, it is a set by Hedberg’s Theorem [28, Theorem 7.2.5]. Therefore $f=g$ by Lemma 74. ∎

Definition 77** (getfib).**

For every $i:I$, define a function $\mathsf{getfib}_{i}:\mathsf{W}_{s,t}(i)\to\mathsf{fib}_{t}(i)$ inductively by

[TABLE]

In future use, we omit the subscript of $\mathsf{getfib}$.

Lemma 78**.**

Let $i,j:I$ with a path $p:i=j$ and $w:\mathsf{W}_{s,t}(i)$. We have the following equality:

[TABLE]

• Proof (getfib_transport). By path induction on $p$. ∎

We are now in position to state and prove the lemma from which Theorem 73 follows.

Lemma 79**.**

Suppose that $B(a)$ is $\Pi$-compact for every $a:A$ and that the fiber of $t$ over each $i:I$ has decidable equality. For any $i:I$, $u:\mathsf{W}_{s,t}(i)$, $j:I$, path $p:i=j$ and $v:\mathsf{W}_{s,t}(j)$, the type

[TABLE]

is decidable.

• Proof (indexedWtype_deceq_transport). Suppose $i:I$ and $u:\mathsf{W}_{s,t}(i)$. We proceed by induction on $u$ and so we assume that $u\equiv\mathsf{indexedsup}(a,f)$. The induction hypothesis reads:

[TABLE]

Suppose we have $j:I$ with path $p:t(a)=j$ and $v:\mathsf{W}_{s,t}(j)$. By induction, we may assume that $v\equiv\mathsf{indexedsup}(a^{\prime},f^{\prime})$. We are tasked to show that

[TABLE]

is decidable, where $p:t(a)=t(a^{\prime})$.

By assumption the fiber of $t$ over $t(a^{\prime})$ has decidable equality. Hence, we can decide if $\left(a^{\prime},\mathsf{refl}_{t(a^{\prime})}\right)$ and $(a,p)$ are equal or not. Suppose first that the pairs are not equal. We claim that in this case $\lnot\eqref{indexedsupdec}$. For suppose we had $e:\eqref{indexedsupdec}$, then

[TABLE]

By definition, the right hand side is $(a^{\prime},\mathsf{refl}_{t(a^{\prime})})$. By Lemma 78, the left hand side is equal to $(a,\mathsf{refl}_{t(a)}\mathbin{\bullet}p)$ which is in turn equal to $(a,p)$, contradicting our assumption that $\left(a^{\prime},\mathsf{refl}_{t(a^{\prime})}\right)$ and $(a,p)$ were not equal.

Now suppose that $\left(a^{\prime},\mathsf{refl}_{t(a^{\prime})}\right)=(a,p)$. From this, we obtain paths $e_{1}:a^{\prime}=a$ and $e_{2}~{}:~{}\operatorname{\mathsf{transport}}^{\lambda x:A.t(x)=t(a^{\prime})}\left(e_{1},\mathsf{refl}_{t(a^{\prime})}\right)=p$. By path induction, we may assume $e_{1}\equiv\mathsf{refl}_{a^{\prime}}$, so that from $e_{2}$ we obtain a path

[TABLE]

Using this path, we see that the left hand side of ($\dagger$ ‣ ‣ 8.2.4) is equal to $\mathsf{indexedsup}(a^{\prime},f)$, so we are left to show that

[TABLE]

is decidable.

By induction hypothesis ($\ast$ ‣ ‣ 8.2.4) and the fact that $a\equiv a^{\prime}$, the type $f(b)=f^{\prime}(b)$ is decidable for every $b:B(a^{\prime})$. Since $B(a^{\prime})$ is $\Pi$-compact, this implies that $\prod_{b:B(a^{\prime})}f(b)=f^{\prime}(b)$ is decidable.

Suppose first that $\prod_{b:B(a^{\prime})}f(b)=f^{\prime}(b)$. Function extensionality then yields $f=f^{\prime}$, so that $\mathsf{indexedsup}(a^{\prime},f)=\mathsf{indexedsup}(a^{\prime},f^{\prime})$.

On the other hand, suppose $\lnot\prod_{b:B(a^{\prime})}f(b)=f^{\prime}(b)$. We claim that then, $\mathsf{indexedsup}(a^{\prime},f)$ cannot be equal to $\mathsf{indexedsup}(a^{\prime},f^{\prime})$. For suppose that $\mathsf{indexedsup}(a^{\prime},f)=\mathsf{indexedsup}(a^{\prime},f^{\prime})$. Then Lemma 76 yields $f=f^{\prime}$, contradicting our assumption that $\lnot\prod_{b:B(a)}f(b)=f^{\prime}(b)$, and finishing the proof. ∎

• Proof of Theorem 73 (indexedWtype_deceq). Let $i:I$ and $u,v:\mathsf{W}_{s,t}(i)$. Taking $j\vcentcolon\mspace{-1.2mu}\equiv i$ and $p\vcentcolon\mspace{-1.2mu}\equiv\mathsf{refl}_{i}$ in Lemma 79, we see that $u=v$ is decidable, as desired. ∎

9 Size matters

In this penultimate section, we explain some of the subtleties regarding dcpos and universe levels. In particular, we revisit the dcpo of continuous functions while rigorously keeping track of universe levels. In the end, our analysis shows that, even in the absence of propositional resizing, the interpretation function $\llbracket-\rrbracket$ of the Scott model is well-defined (Theorem 80). (For more on predicative domain theory, the reader may wish to consult our recent work [10, 11].)

As mentioned in the introduction, our results are formalised in Agda [14, PCFModules].

To study universe levels, let us suppose that we have a tower of type universes $\mathcal{U}_{0}:\mathcal{U}_{1}:\dots$, indexed by meta natural numbers. (In the end, it will turn out that having just two universes $\mathcal{U}_{0}:\mathcal{U}_{1}$ is sufficient for our purposes.) Let us fix some notation for (raising) universe levels. We write $\mathcal{U}_{i}^{+}$ for $\mathcal{U}_{i+1}$ and $\mathcal{U}_{i}\sqcup\mathcal{U}_{j}$ for $U_{\max(i,j)}$. The universes are assumed to be closed under $+$-, $\Sigma$- and $\Pi$-types and if $X:\mathcal{U}$ and $Y:X\to\mathcal{V}$, then $\sum_{x:X}Y(x),\prod_{x:X}Y(x):\mathcal{U}\sqcup\mathcal{V}$. Finally, since $\mathcal{U}:\mathcal{U}^{+}$, we have $\sum_{X:\mathcal{U}}Y(X):\mathcal{U}^{+}\sqcup\mathcal{V}$ if $Y:\mathcal{U}\to\mathcal{V}$.

9.1 The lifting

In Section 1.2, we introduced $\Omega$ as the type of propositions in the universe $\mathcal{U}_{0}$. To see why we made this particular choice of type universe and to appreciate the considerations involved, it is helpful to consider a more general situation. Let us write $\Omega_{\mathcal{T}}$ for the propositions in some type universe $\mathcal{T}$. Define the (generalised) lifting $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$ of a type $X$ is as $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)\vcentcolon\mspace{-1.2mu}\equiv\sum_{P:\Omega_{\mathcal{T}}}(P\to X)$.

Now observe that if $X$ is a type in a universe $\mathcal{U}$, then lifting (potentially) raises the universe level, as $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$ is a type in universe $\mathcal{T}^{+}\sqcup\mathcal{U}$. However, if $X$ happens to be a type in $\mathcal{T}^{+}$, then $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$ also lives in $\mathcal{T}^{+}$. Moreover, repeated applications of $\operatorname{\mathcal{L}}$ do not raise the universe level any further, because if $X$ is in $\mathcal{T}^{+}\sqcup\mathcal{U}$, then $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$ is as well. Despite the fact that lifting raises the universe level, one can write down the monad laws for $\operatorname{\mathcal{L}}_{\mathcal{T}}$ and they typecheck.

Let $X$ and $I$ be types in universes $\mathcal{U}$ and $\mathcal{V}$, respectively. Suppose that $u:I\to\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$. Note that $\sum_{i:I}\operatorname{\mathsf{isdefined}}(u_{i})$ is in $\mathcal{V}\sqcup\mathcal{T}$. When considering $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$ as a dcpo (cf. Theorem 26), we want $\sum_{i:I}\operatorname{\mathsf{isdefined}}(u_{i})$ to be in $\mathcal{T}$ again. One way to ensure this, is to take $\mathcal{V}$ to be $\mathcal{U}_{0}$. This would make $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$ a $\mathcal{U}_{0}$-dcpo. Indeed, this is what we prove in the Agda formalisation. In particular, this means that $\operatorname{\mathcal{L}}_{\mathcal{T}}(X)$ has $\mathsf{N}$-indexed directed suprema, which suffices for the Scott model of PCF.

9.2 The dcpo of continuous functions

In fact, we should be even more precise when it comes universe levels and dcpos than we have been so far. Write $\mathcal{W}\text{-}\left(\mathsf{DCPO}_{\bot}\right)_{\mathcal{U},\mathcal{V}}$ for the type of $\mathcal{W}$-directed complete posets with a least element whose underlying type is in $\mathcal{U}$ and whose underlying order takes values in $\mathcal{V}$.

Then $\operatorname{\mathcal{L}}_{\mathcal{U}_{0}}(\mathsf{N})\equiv\operatorname{\mathcal{L}}(\mathsf{N})$ is of type $\mathcal{U}_{0}\text{-}\left(\mathsf{DCPO}_{\bot}\right)_{\mathcal{U}_{1},\mathcal{U}_{1}}$, for example. (One easily checks that the order $\sqsubseteq$ from Theorem 26 has values in $\mathcal{U}_{1}$.)

Recall that $\llbracket\sigma\Rightarrow\tau\rrbracket\equiv\llbracket\tau\rrbracket^{\llbracket\sigma\rrbracket}$, the dcpo with $\bot$ of continuous functions from $\llbracket\sigma\rrbracket$ to $\llbracket\tau\rrbracket$, so let us investigate the universe levels surrounding the exponential. In general, we have:

[TABLE]

We explain the universe levels involved as follows.

Let $\mathcal{D}$ be of type $\mathcal{W}\text{-}\left(\mathsf{DCPO}_{\bot}\right)_{\mathcal{U},\mathcal{V}}$ and write $D$ and $\leq_{\mathcal{D}}$ for its underlying type and order, respectively. Further, let $\mathcal{E}$ be of type $\mathcal{W}\text{-}\left(\mathsf{DCPO}_{\bot}\right)_{\mathcal{U}^{\prime},\mathcal{V}^{\prime}}$ and write $E$ and $\leq_{\mathcal{E}}$ for its underlying type and order, respectively.

The underlying type of the exponential $\mathcal{E}^{\mathcal{D}}$ is the type of functions from $D$ to $E$ that are continuous. The underlying order is the pointwise order: if $f$ and $g$ are continuous functions from $D$ to $E$, then $f\leq_{\mathcal{E^{D}}}g$ if $\prod_{x:D}f(x)\leq_{\mathcal{E}}g(x)$.

Because $D$ is in $\mathcal{U}$ and $\leq_{\mathcal{E}}$ takes values in $\mathcal{V}^{\prime}$, we see that $\leq_{\mathcal{E^{D}}}$ takes values in $\mathcal{U}\sqcup\mathcal{V}^{\prime}$.

Furthermore, the type of functions from $D$ to $E$ is in $\mathcal{U}\sqcup\mathcal{U}^{\prime}$. But the type of continuous functions also mentions $\leq_{\mathcal{D}}$ and $\leq_{\mathcal{E}}$ and all directed families indexed by a type in $\mathcal{W}$. In particular, the latter means that the definition of the type of continuous functions contains $\prod_{I:\mathcal{W}}$. Therefore the type of continuous functions is in $\mathcal{W}^{+}\sqcup\mathcal{V}\sqcup\mathcal{V}^{\prime}\sqcup\mathcal{U}\sqcup\mathcal{U}^{\prime}$.

9.3 The Scott model of PCF

Given the increasing universe levels in ($\dagger$ ‣ 9.2), one might ask if there can be universes $\mathcal{U},\mathcal{V},\mathcal{W}$ such that

[TABLE]

typechecks.

As we mentioned, $\operatorname{\mathcal{L}}_{\mathcal{U}_{0}}(\mathsf{N})\equiv\operatorname{\mathcal{L}}(\mathsf{N}):\mathcal{U}_{0}\text{-}\left(\mathsf{DCPO}_{\bot}\right)_{\mathcal{U}_{1},\mathcal{U}_{1}}$. Since, $\llbracket\iota\rrbracket\equiv\operatorname{\mathcal{L}}(\mathsf{N})$, one would hope that

[TABLE]

And indeed, this is the case.

Theorem 80**.**

The interpretation function $\llbracket-\rrbracket$ from PCF types to dcpos with $\bot$ can be typed as:

[TABLE]

• Proof. If, in ($\dagger$ ‣ 9.2), we take $\mathcal{W}$ to be $\mathcal{U}_{0}$ and $\mathcal{U},\mathcal{U}^{\prime},\mathcal{V},\mathcal{V}^{\prime}$ all to be $\mathcal{U}_{1}$, then ($\dagger$ ‣ 9.2) reads:

[TABLE]

as desired. ∎

10 Conclusion and future work

Our development confirms that univalent type theory is well adapted to the constructive formalisation of domain-theoretic denotational semantics of programming languages like PCF, which was the original goal of this investigation. Moreover, our development is predicative. In particular, we have given a predicative version of directed complete posets. Our results show that partiality in univalent type theory via lifting works well. We rely crucially on Voevodsky’s treatment of subsingletons as truth values. In particular, the propositional truncation plays a fundamental and interesting role in this work. Finally, we saw an interesting application of the abstract theory of indexed $\mathsf{W}$-types in characterising the propositions that come from PCF terms of the base type.

Regarding the Scott model of PCF, there are two questions for future research:

Is there a natural extension of the map $\llbracket\iota\rrbracket\xrightarrow{\operatorname{\mathsf{pr_{1}}}}\Omega$ to all PCF types? Can we characterise the propositions at types other than $\iota$, e.g. the propositions at type $\iota\Rightarrow\iota$? Are they still semidecidable? 2. 2.

How can we better understand the fact that only semidecidable propositions occur for the Scott model, but that restricting to such propositions somehow needs a weak form of countable choice?

In [10] we develop domain theory further in predicative and constructive univalent type theory, including continuous and algebraic dcpos, ideal completions and Scott’s famous $D_{\infty}$. Complementing this work, the paper [11] explores some aspects of domain theory that cannot be done predicatively.