Fully Abstract Models of the Lambda Calculus

This post discusses the denotational semantics of the lambda calculus.

Models

Definition (Partial Equivalence Relation - PER). A partial equivalence relation (PER) is a symmetric, transitive relation \(R \subseteq D \times D\) on a set \(D\).

Definition (PER Domain). The domain of a partial equivalence relation \(R\) on a set \(D\) is the set

\[\mathrm{dom}(R) = \{d \in D \mid d \mathrel{R} d\}.\]

Definition (Environment). Given a partial equivalence relation \(R \subseteq D \times D\) on a set \(D\) called a semantic domain, an environment is a map \(\rho : \mathcal{V} \rightarrow \mathrm{dom}(R)\). The set of all environments for a given relation is denoted \(\mathrm{Env}(R)\).

Definition (Environmental Update). Given a partial equivalence relation \(R \subseteq D \times D\) on a semantic domain \(D\) and an environment \(\rho \in \mathrm{Env}(R)\), the environmental update of \(\rho\) with the variable \(x \in \mathcal{V}\) updated to \(d \in \mathrm{dom}(R)\) is defined as

\[\rho[x \mapsto d](x') = \begin{cases} d &\text{if } x = x' \\ \rho(x') & \text{otherwise}.\end{cases}\]

Definition (Model). A model \(\mathcal{M} = (D, R, \cdot, \llbracket \cdot \rrbracket_{(\cdot)})\) consists of the following items:

• A set \(D\) called the carrier or semantic domain;
• A partial equivalence relation \(R \subseteq D \times D\);
• A distinguished element \(\bot \in \mathrm{dom}(R)\) representing divergence;
• A binary operation \(\cdot : D \times D \rightarrow D\) called application;
• A map \(\llbracket \cdot \rrbracket_{(\cdot)} : \Lambda \times \mathrm{Env}(R) \rightarrow \mathrm{dom}(R)\), where \(\llbracket M \rrbracket_{\rho}\) is called the denotation of the term \(M \in \Lambda\) under the environment \(\rho \in \mathrm{Env}(R)\);

these items are subject to the following axioms:

• Congruence: for all \(f,g,x,y \in D\), if \(f \mathrel{R} g\) and \(x \mathrel{R} y\) then \((f \cdot x) \mathrel{R} (g \cdot y)\);
• Variable Assignment: \(\llbracket x \rrbracket_{\rho} = \rho(x)\) for all variables \(x \in \mathcal{V}\) and environments \(\rho \in \mathrm{Env}(R)\);
• Semantic Abstraction: \(\left(\llbracket (\lambda x . M) \rrbracket_{\rho} \cdot d\right) \mathrel{R} \llbracket M \rrbracket_{\rho[x \mapsto d]}\) for all variables \(x \in \mathcal{V}\), terms \(M \in \Lambda\), environments \(\rho \in \mathrm{Env}(R)\), and elements \(d \in \mathrm{dom}(R)\);
• Applicative Consistency: \(\llbracket (MN) \rrbracket_{\rho} \mathrel{R} \left(\llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho}\right)\) for all terms \(M,N \in \Lambda\) and environments \(\rho \in \mathrm{Env}(R)\);
• Environmental Consistency: for all terms \(M \in \Lambda\) and environments \(\rho, \rho' \in \mathrm{Env}(R)\), if \(\rho(x) \mathrel{R} \rho'(x)\) for all \(x \in \mathrm{Free}(M)\), then \(\llbracket M \rrbracket_{\rho} \mathrel{R} \llbracket M \rrbracket_{\rho'}\);
• Extensionality: for all \(f,g \in \mathrm{dom}(R)\), if \((f \cdot x) \mathrel{R} (g \cdot y)\) for all \(x,y \in \mathrm{dom}(R)\) such that \(x \mathrel{R} y\), then \(f \mathrel{R} g\).

Definition (Satisfaction). For a model \(\mathcal{M} = (D, R, \cdot, \llbracket \cdot \rrbracket_{(\cdot)})\), environment \(\rho \in \mathrm{Env}(R)\), and terms \(M,N \in \Lambda\) we make the following definitions:

• \(\mathcal{M},\rho \models M = N\) if and only if \(\llbracket M \rrbracket_{\rho} \mathrel{R} \llbracket N \rrbracket_{\rho}\). If \(M\) and \(N\) are closed terms (\(M, N \in \Lambda(\emptyset)\)), we write \(\mathcal{M} \models M = N\) to indicate that \(\mathcal{M},\rho \models M = N\) for every environment \(\rho \in \mathrm{Env}(R)\).
• \(\mathcal{M},\rho \models M \downarrow\) if and only if \(\llbracket M \rrbracket_{\rho} \ne \bot\). If \(M\) is a closed term (\(M \in \Lambda(\emptyset)\)), we write \(\mathcal{M} \models M \downarrow\) to indicate that \(\mathcal{M},\rho \models M \downarrow\) for every environment \(\rho \in \mathrm{Env}(R)\).

Definition (Adequacy). A model is adequate with respect to an evaluation strategy \(\mathrm{s}\) if, for every closed term \(M \in \Lambda(\emptyset)\),

\[\mathcal{M} \models M \downarrow \Leftrightarrow M \Downarrow_{\mathrm{s}}.\]

Definition (Soundness). A model is sound with respect to an evaluation strategy \(\mathrm{s}\) if, for all closed terms \(M, N \in \Lambda(\emptyset)\),

\[\mathcal{M} \models M = N \Rightarrow M \approx_{\mathrm{s}} N.\]

Definition (Completeness). A model is complete with respect to an evaluation strategy \(\mathrm{s}\) if, for all closed terms \(M, N \in \Lambda(\emptyset)\),

\[M \approx_{\mathrm{s}} N \Rightarrow \mathcal{M} \models M = N.\]

Definition (Full Abstraction). A model is fully abstract with respect to an evaluation strategy if it is both sound and complete with respect to this evaluation strategy, i.e., if, for all closed terms \(M, N \in \Lambda(\emptyset)\),

\[\mathcal{M} \models M = N \Leftrightarrow M \approx_{\mathrm{s}} N.\]

Complete Partial Orders

This section introduces complete partial orders.

Definition (\(\mathbf{\omega}\)-chain). An \(\mathbf{\omega}\)-chain in a partial order \((D, \sqsubseteq)\) is a sequence \((d_n)_{n \in \mathbb{N}}\) such that \(d_n \sqsubseteq d_{n+1}\) for all \(n \in \mathbb{N}\).

Notation (\(\mathbf{\omega}\)-chain Supremum). The supremum (least upper bound) of an \(\omega\)-chain \((d_n)_{n \in \mathbb{N}}\) in a partial order \((D, \sqsubseteq)\) is denoted

\[\bigsqcup_{n \in \mathbb{N}}d_n.\]

Definition (\(\mathbf{\omega}\)-Complete Partial Order). A partial order \((D, \sqsubseteq)\) is \(\mathbf{\omega}\)-complete if it contains all suprema of \(\omega\)-chains.

Definition (Pointed Partial Order). A partial order \((D, \sqsubseteq)\) is pointed if it contains a least element \(\bot \in D\).

Terminological Note: henceforth, we will simply write "complete partial order" or "CPO" to indicate a pointed, \(\omega\)-complete partial order.

Definition (Admissible PER). A partial equivalence relation \(R\) is admissible for a CPO \((D, \sqsubseteq)\) if

\[\left(\bigsqcup_{n \in \mathbb{N}}x_n\right) \mathrel{R} \left(\bigsqcup_{n \in \mathbb{N}}y_n\right)\]

for every pair of \(\omega\)-chains \((x_n)_{n \in \mathbb{N}}\) and \((y_n)_{n \in \mathbb{N}}\) in \(D\) such that \(x_n \mathrel{R} y_n\) for all \(n \in \mathbb{N}\).

Definition (Continuous Map). A map \(F : D \rightarrow E\) between a CPO \((D, \sqsubseteq_D)\) and a CPO \((E, \sqsubseteq_E)\) is continuous if, for every \(\omega\)-chain \((d_n)_{n \in \mathbb{N}}\) in \(D\) the sequence \((F(d_n))_{n \in \mathbb{N}}\) is an \(\omega\)-chain and

\[F\left(\bigsqcup_{n \in \mathbb{N}}d_n\right) = \bigsqcup_{n \in \mathbb{N}}F(d_n).\]

Theorem (Monotonicity of Continuous Maps). Every continuous map between CPOs is monotone.

Proof. Let \(F : D \rightarrow E\) be any continuous map between CPOs \((D, \sqsubseteq_D)\) and \((E, \sqsubseteq_E)\). Suppose that \(x \sqsubseteq_D y\) for any \(x,y \in D\). Define an \(\omega\)-chain \((d_n)_{n \in \mathbb{N}}\) as follows: \(d_0 = x\), \(d_n = y\) for all \(n \ge 1\). Then:

\begin{align*}F(x) &= F(d_0) \\& \sqsubseteq_E \bigsqcup_{n \in \mathbb{N}}F(d_n) \\&= F\left(\bigsqcup_{n \in \mathbb{N}}d_n\right) \\&= F(y).\end{align*}

Theorem (Least Fixed Point). For any CPO \((D, \sqsubseteq)\) and continuous map \(F : D \rightarrow D\), the least fixed point of \(F\) is given by

\[\mu F = \bigsqcup_{n \in \mathbb{N}}F^n(\bot).\]

Proof. First note that \(\bot \sqsubseteq F^0(\bot) = \bot\) and, if \(F^n(\bot) \sqsubseteq F^{n+1}(\bot)\) then, since \(F\) is continuous, it is also monotone, and so \(F^{n+1}(\bot) = F(F^n(\bot)) \sqsubseteq F(F^{n+1}(\bot)) = F^{n+2}(\bot)\). Thus, by induction, it follows that \((F^n(\bot))_{n \in \mathbb{N}}\) is an \(\omega\)-chain and therefore \(\bigsqcup_{n \in \mathbb{N}}F^n(\bot) \in D\) and \(\mu F\) is well-defined. Next, note that

\begin{align*}F\left(\bigsqcup_{n \in \mathbb{N}}F^n(\bot)\right) &= \bigsqcup_{n \in \mathbb{N}}F(F^n(\bot)) \\&= \bigsqcup_{n \in \mathbb{N}}F^{n+1}(\bot) \\&= \bigsqcup_{n \in \mathbb{N}}F^n(\bot).\end{align*}

Finally, if \(F(p) = p\) (and hence \(F(p) \sqsubseteq p\) by reflexivity) for some \(p \in D\), then \(F^0(\bot) = \bot \sqsubseteq p\), and, if \(F^n(\bot) \sqsubseteq p\), then, by monotonicity, \(F^{n+1}(p) = F(F^n(\bot)) \sqsubseteq F(p) \sqsubseteq p\). Thus, by induction, \(F^n(\bot) \sqsubseteq p\) for all \(n \in \mathbb{N}\) and \(p\) is an upper bound of the \(\omega\)-chain \((F^n(\bot))_{n \in \mathbb{N}}\) and therefore, by definition, \(\bigsqcup_{n \in \mathbb{N}}F^n(\bot) \sqsubseteq p\). \(\square\)

Theorem (Interchange of Suprema). For any family of elements \(d_{m,n}\) for \(m,n \in \mathbb{N}\) in a CPO \((D, \sqsubseteq)\), if \((d_{m,n})_{n \in \mathbb{N}}\) is an \(\omega\)-chain for each \(m \in \mathbb{N}\) and \((d_{m,n})_{m \in \mathbb{N}}\) is an \(\omega\)-chain for each \(n \in \mathbb{N}\), then

\[\bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}d_{m,n} = \bigsqcup_{n \in \mathbb{N}}\bigsqcup_{m \in \mathbb{N}}d_{m,n}.\]

Proof. First, we verify that \(\left(\bigsqcup_{n \in \mathbb{N}}d_{m,n}\right)_{m \in \mathbb{N}}\) is an \(\omega\)-chain. By hypothesis, \(d_{m,n} \sqsubseteq d_{m+1,n}\) for all \(n \in \mathbb{N}\) and since \(d_{m+1,n} \sqsubseteq \bigsqcup_{n \in \mathbb{N}}d_{m+1,n}\) by definition, it follows that \(d_{m,n} \sqsubseteq \bigsqcup_{n \in \mathbb{N}}d_{m+1,n}\). Since \(n\) was arbitrary, \(\bigsqcup_{n \in \mathbb{N}}d_{m+1,n}\) is an upper bound of the \(\omega\)-chain \((d_{m,n})_{n \in \mathbb{N}}\) and thus \(\bigsqcup_{n \in \mathbb{N}}d_{m,n} \sqsubseteq \bigsqcup_{n \in \mathbb{N}}d_{m+1,n}\).

A symmetric argument shows that \(\left(\bigsqcup_{m \in \mathbb{N}}d_{m,n}\right)_{n \in \mathbb{N}}\) is an \(\omega\)-chain.

Let \(m,n \in \mathbb{N}\) be arbitrary. Then

\[d_{m,n} \sqsubseteq \bigsqcup_{m \in \mathbb{N}}d_{m,n} \sqsubseteq \bigsqcup_{n \in \mathbb{N}}\bigsqcup_{m \in \mathbb{N}}d_{m,n}.\]

It follows that

\[\bigsqcup_{n \in \mathbb{N}}d_{m,n} \sqsubseteq \bigsqcup_{n \in \mathbb{N}}\bigsqcup_{m \in \mathbb{N}}d_{m,n}\]

and also that

\[\bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}d_{m,n} \sqsubseteq \bigsqcup_{n \in \mathbb{N}}\bigsqcup_{m \in \mathbb{N}}d_{m,n}.\]

A symmetric argument shows that

\[\bigsqcup_{n \in \mathbb{N}}\bigsqcup_{m \in \mathbb{N}}d_{m,n} \sqsubseteq \bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}d_{m,n}.\]

\(\square\)

Theorem (Diagonalization of Suprema). For any CPO \((D, \sqsubseteq)\) and family of elements \((d_{m,n})_{m,n \in \mathbb{N}}\) in \(D\) that are jointly monotonic, i.e., \(d_{m,n} \sqsubseteq d_{m',n'}\) whenever \(m \le m'\) and \(n \le n'\), then

\[\bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}d_{m,n} = \bigsqcup_{k \in \mathbb{N}} d_{k,k}.\]

Proof. Note that for any \(k \in \mathbb{N}\),

\[d_{k,k} \sqsubseteq \bigsqcup_{n \in \mathbb{N}} d_{k,n} \sqsubseteq \bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}} d_{m,n}.\]

This means that \(\bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}d_{m,n}\) is an upper bound of the \(\omega\)-chain \((d_{k,k})_{k \in \mathbb{N}}\) and thus

\[\bigsqcup_{k \in \mathbb{N}} d_{k,k} \sqsubseteq \bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}d_{m,n}.\]

Conversely, for any \(m,n \in \mathbb{N}\), if \(p = \mathrm{max}(m,n)\), then \(d_{m,n} \sqsubseteq d_{p,p}\) and thus

\[d_{m,n} \sqsubseteq d_{p,p} \sqsubseteq \bigsqcup_{k \in \mathbb{N}}d_{k,k}\]

and thus \(\bigsqcup_{k \in \mathbb{N}}d_{k,k}\) is an upper bound of the \(\omega\)-chain \((d_{m,n})_{n \in \mathbb{N}}\) and so

\[\bigsqcup_{n \in \mathbb{N}}d_{m,n} \sqsubseteq \bigsqcup_{k \in \mathbb{N}}d_{k,k}\]

and hence \(\bigsqcup_{k \in \mathbb{N}}d_{k,k}\) is an upper bound of the \(\omega\)-chain \((\bigsqcup_{n \in \mathbb{N}}d_{m,n})_{m \in \mathbb{N}}\) and thus

\[\bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}d_{m,n} \sqsubseteq \bigsqcup_{k \in \mathbb{N}} d_{k,k}.\]

\(\square\)

Theorem (Function Space). For any CPOs \((D, \sqsubseteq_D)\) and \((E, \sqsubseteq_E)\), the set of all continuous maps \(\mathrm{Cont}(D, E)\) is a CPO under the following ordering for any \(F, G \in \mathrm{Cont}(D, E)\):

\[F \sqsubseteq G \Leftrightarrow \forall d \in D(F(d) \sqsubseteq_E G(d)).\]

Proof. For any map \(F \in \mathrm{Cont}(D, E)\) and every \(d \in D\), \(F(d) \sqsubseteq_E F(d)\) by reflexivity and thus \(F \sqsubseteq F\), so the order is reflexive.

For any maps \(F, G \in \mathrm{Cont}(D, E)\), if \(F \sqsubseteq G\) and \(G \sqsubseteq F\), then, for any \(d \in D\), \(F(d) \sqsubseteq_E G(d)\) and \(G(d) \sqsubseteq_E F(d)\), so, by antisymmetry, \(F(d) = G(d)\). Since \(d\) was arbitrary, \(F = G\) and the order is thus antisymmetric.

For any maps \(F,G,H \in \mathrm{Cont}(D,E)\), if \(F \sqsubseteq G\) and \(G \sqsubseteq H\), then, for any \(d \in D\), \(F(d) \sqsubseteq_E G(d)\) and \(G(d) \sqsubseteq_E H(d)\), so, by transitivity, \(F(d) \sqsubseteq_E H(d)\). Since \(d\) was arbitrary, \(F \sqsubseteq H\) and the order is thus transitive.

Since the order is reflexive, antisymmetric, and transitive, it is a partial order and is thus well-defined.

We define

\[\bot = d \mapsto \bot\]

so that, for any map \(F \in \mathrm{Cont}(D, E)\) and any \(d \in D\), \(\bot(d) = \bot \sqsubseteq_E F(d)\) and hence \(\bot \sqsubseteq F\). Note also that \(\bot\) is continuous: for any \(\omega\)-chain \((d_n)_{n \in \mathbb{N}}\) in \(D\),

\[\bot\left(\bigsqcup_{n \in \mathbb{N}}d_n\right) = \bot = \bigsqcup_{n \in \mathbb{N}}\bot(d_n).\]

We claim that, for any \(\omega\)-chain \((F_n)_{n \in \mathbb{N}}\) in \(\mathrm{Cont}(D, E)\),

\[\left(\bigsqcup_{n \in \mathbb{N}}F_n\right)(x) = \bigsqcup_{n \in \mathbb{N}}F_n(x).\]

We will show that \(\bigsqcup_{n \in \mathbb{N}}F_n\) is continuous. Let \((d_m)_{m \in \mathbb{N}}\) be any \(\omega\)-chain in \(D\). Observe that

\begin{align*}\left(\bigsqcup_{n \in \mathbb{N}}F_n\right)\left(\bigsqcup_{m \in \mathbb{N}}d_m\right) &= \bigsqcup_{n \in \mathbb{N}}F_n\left(\bigsqcup_{m \in \mathbb{N}}d_m\right) \\&= \bigsqcup_{n \in \mathbb{N}}\left(\bigsqcup_{m \in \mathbb{N}}F_n(d_m)\right) \\&= \bigsqcup_{m \in \mathbb{N}}\left(\bigsqcup_{n \in \mathbb{N}}F_n(d_m)\right) \\&= \bigsqcup_{m \in \mathbb{N}}\left(\left(\bigsqcup_{n \in \mathbb{N}}F_n\right)(d_m)\right). \end{align*}

For any \(d \in D\) and \(n \in \mathbb{N}\), \(F_n(d) \sqsubseteq \bigsqcup_{n \in \mathbb{N}}F_n(d)\) and thus \(F_n \sqsubseteq \bigsqcup_{n \in \mathbb{N}}F_n\) and \(\bigsqcup_{n \in \mathbb{N}}F_n\) is an upper bound of the \(\omega\)-chain \((F_n)_{n \in \mathbb{N}}\).

If \(U \in \mathrm{Cont}(D, E)\) is any other upper bound of \((F_n)_{n \in \mathbb{N}}\), then, for any \(d \in D\), \(\left(\bigsqcup_{n \in \mathbb{N}}F_n\right)(d) = \bigsqcup_{n \in \mathbb{N}}F_n(d) \sqsubseteq_E U(d)\), and hence \(\bigsqcup_{n \in \mathbb{N}}F_n \sqsubseteq U\), so \(\bigsqcup_{n \in \mathbb{N}}F_n\) is the least upper bound of the \(\omega\)-chain \((F_n)_{n \in \mathbb{N}}\). \(\square\)

The Categories

In this section, we define several important categories.

Definition (\(\mathbf{CPO}^{ep}\)). The category \(\mathbf{CPO}^{ep}\) is defined as follows:

• Objects: CPOs \(D\);
• Arrows: an arrow between objects \(D\) and \(E\) is a pair \((i, p)\) consisting of a continuous map \(i : D \rightarrow E\) called an embedding and a continuous map \(p : E \rightarrow D\) called a projection such that the following conditions are met:
  • \(p \circ i = \mathrm{id}_D\);
  • \(i \circ p \sqsubseteq \mathrm{id}_E\);
• Identity: the identity arrow on an object \(D\) is the arrow \((\mathrm{id}_D, \mathrm{id}_D)\);
• Composition: the composition of an arrow \((i_1, p_1) : (D_1, R_1) \rightarrow (D_2, R_2)\) and an arrow \((i_2, p_2) : (D_2, R_2) \rightarrow (D_3, R_3)\) is given by \((i_2, p_2) \circ (i_1, p_1) = (i_2 \circ i_1, p_1 \circ p_2)\).

Definition (\(\mathbf{CPO}^e\)). The category \(\mathbf{CPO}^e\) is defined as follows:

• Objects: CPOs \(D\);
• Arrows: an arrow between objects \(D\) and \(E\) is a continuous map \(i : D \rightarrow E\) called an embedding such that there exists a continuous map \(p : E \rightarrow D\) called a projection such that the following conditions are met:
  • \(p \circ i = \mathrm{id}_D\);
  • \(i \circ p \sqsubseteq \mathrm{id}_E\);
• Identity: the identity arrow on an object \(D\) is the arrow \(\mathrm{id}_D : D \rightarrow D\);
• Composition: the composition of an arrow \(i_1 : (D_1, R_1) \rightarrow (D_2, R_2)\) and an arrow \(i_2 : (D_2, R_2) \rightarrow (D_3, R_3)\) is given by \(i_2 \circ i_1\).

Definition (\(\mathbf{CPO}^p\)). The category \(\mathbf{CPO}^p\) is defined as follows:

• Objects: CPOs \(D\);
• Arrows: an arrow between objects \(E\) and \(D\) is a continuous map \(p : E \rightarrow D\) called a projection such that there exists a continuous map \(i : D \rightarrow E\) called an embedding such that the following conditions are met:
  • \(p \circ i = \mathrm{id}_D\);
  • \(i \circ p \sqsubseteq \mathrm{id}_E\);
• Identity: the identity arrow on an object \(D\) is the arrow \(\mathrm{id}_D : D \rightarrow D\);
• Composition: the composition of an arrow \(p_1 : (D_3, R_3) \rightarrow (D_2, R_2)\) and an arrow \(p_2 : (D_2, R_2) \rightarrow (D_1, R_1)\) is given by \(p_2 \circ p_1\).

Lemma (Uniqueness of Embeddings). For any continuous map \(p : E \rightarrow D\) between CPOs \(E\) and \(D\), if there exists a continuous map \(i : D \rightarrow E\) such that

• \(p \circ i = \mathrm{id}_D\), and
• \(i \circ p \sqsubseteq \mathrm{id}_E\),

then \(i\) is unique.

Proof. Suppose there exists another continuous map \(i'\) satisfying these properties. Since \(i \circ p \sqsubseteq \mathrm{id}_E\), it follows that \(i \circ p \circ i' \sqsubseteq \mathrm{id}_E \circ i'\) and hence \(i \sqsubseteq i'\). A symmetric argument shows that \(i' \sqsubseteq i\) and hence \(i = i'\). \(\square\)

Lemma (Uniqueness of Projections). For any continuous map \(i : D \rightarrow E\) between CPOs \(D\) and \(E\), if there exists a continuous map \(p : E \rightarrow D\) such that

• \(p \circ i = \mathrm{id}_D\), and
• \(i \circ p \sqsubseteq \mathrm{id}_E\),

then \(p\) is unique.

Proof. Suppose there exists another continuous map \(p'\) satisfying these properties. Since \(i \circ p \sqsubseteq \mathrm{id}_E\) and \(p'\) is continuous (and hence monotone), it follows that \(p' \circ i \circ p \sqsubseteq p' \circ \mathrm{id}_E\) and hence \(p \sqsubseteq p'\). A symmetric argument shows that \(p' \sqsubseteq p\) and hence \(p = p'\). \(\square\)

Theorem (Isomorphism). \(\mathbf{CPO}^{ep} \cong \mathbf{CPO}^e\).

Proof. Define a functor \(F^e : \mathbf{CPO}^{ep} \rightarrow \mathbf{CPO}^e\) as follows:

• Objects: \(F^e(D) = D\);
• Arrows: \(F^e(i, p) = i\).

Define a functor \((F^e)^{-1} : \mathbf{CPO}^e \rightarrow \mathbf{CPO}^{ep}\) as follows:

• Objects: \((F^e)^{-1}(D) = D\);
• Arrows: \((F^e)^{-1}(i) = (i, p_i)\), where \(p_i\) is the projection corresponding to \(i\).

Note that for any \(i : D \rightarrow E\), \(F^e((F^e)^{-1}(i)) = i\) and (F^e)^{-1}(F^e(i, p)) = (i, p_i) and \(p_i = p\) by the uniqueness of projections. \(\square\)

Theorem (Isomorphism). \(\mathbf{CPO}^{ep} \cong (\mathbf{CPO}^p)^{op}\).

Proof. Define a functor \(F^p : \mathbf{CPO}^{ep} \rightarrow (\mathbf{CPO}^p)^{op}\) as follows:

• Objects: \(F^p(D) = D\);
• Arrows: \(F^p(i, p) = p\).

Define a functor \((F^p)^{-1} : (\mathbf{CPO}^p)^{op} \rightarrow \mathbf{CPO}^{ep}\) as follows:

• Objects: \((F^p)^{-1}(D) = D\);
• Arrows: \((F^p)^{-1}(p) = (i_p, p)\), where \(i_p\) is the embedding corresponding to \(p\).

Note that for and \(p : E \rightarrow D\), \(F^p((F^p)^{-1}(p)) = p\) and \((F^p)^{-1}(F^p(i, p)) = (i_p, p)\) and \(i_p = i\) by the uniqueness of embeddings. \(\square\)

Theorem (Bilimit). Let \(F : J \rightarrow \mathbf{CPO}^{ep}\) be any diagram and suppose that \((B, \psi_D)\) is a colimit of \(F\). Then \((B, F^e(\psi_D))\) is a colimit of the diagram \(F^e \circ F\) and \((B, F^p(\psi_D))\) is a limit of the diagram \((F^p)^{op} \circ F\).

Proof. The isomorphism \(F^e\) preserves colimits, so \((F^e(B), F^e(\psi_D)) = (B, F^e(\psi_D))\) is a colimit of the diagram \(F^e \circ F\). Likewise, the isomorphism \(F^p\) preserves colimits, so \((F^p(B), F^p(\psi_D)) = (B, F^p(\psi_D))\) is a colimit of the diagram \(F^p \circ F\) in \((\mathbf{CPO}^p)^{op}\) and thus a limit of the diagram \((F^p \circ F)^{op} = (F^p)^{op} \circ F\) in \(\mathbf{CPO}^p\). \(\square\)

The Colimit Characterization Lemma

In this section, we will prove an important lemma that characterizes \(\omega\)-colimits.

Definition (\(\omega\)-chain). An \(\mathbf{\omega}\)-chain in a category \(\mathcal{C}\) is a sequence \((X_n, \gamma_n)_{n \in \mathbb{N}}\) where \(X_n\) is an object of \(\mathcal{C}\) and \(\gamma_n : X_n \rightarrow X_{n+1}\) is an arrow of \(\mathcal{C}\).

Definition (Composite maps in \(\omega\)-chains). For any \(\omega\)-chain \((X_n, \gamma_n)_{n \in \mathbb{N}}\) in a category \(\mathcal{C}\), the arrow \(\gamma_m^n : X_m \rightarrow X_n\) is defined for any \(m,n \in \mathbb{N}\) such that \(m \le n\) as follows:

• \(\gamma_m^m = \mathrm{id}_{X_m}\);
• \(\gamma_m^{m + (k+1)} = \gamma_{m+ k} \circ \gamma_m^{m+k}\).

Definition (Composite Maps of Embedding-Projection Pairs). For any \(\omega\)-chain \(X_n, \gamma_n = (i_n, p_n))_{n \in \mathbb{N}}\) in \(\mathbf{CPO}^{ep}\), for any \(m,n \in \mathbb{N}\) such that \(m \le n\), we write \(\gamma_m^n = (i_m^n, p_m^n)\). It follows that

• \((i_m^m, p_m^m) = (\mathrm{id}_{X_m}, \mathrm{id}_{X_m})\), and
• \((i_m^{m + (k+1)}, p_m^{m + (k+1)}) = (i_{m+ k}, p_{m+ k}) \circ (i_m^{m+k}, p_m^{m+k})\),

and hence the following identities hold:

• embeddings:
  • \(i_m^m = \mathrm{id}_{X_m}\);
  • \(i_m^{m + (k+1)} = i_{m+ k} \circ i_m^{m+k}\).
• projections:
  • \(p_m^m = \mathrm{id}_{X_m}\);
  • \(p_m^{m + (k+1)} = p_m^{m+k} \circ p_{m+ k}\).

Definition (\(\omega\)-cocone). An \(\mathbf{\omega}\)-cocone over an \(\omega\)-chain \((X_n, \gamma_n)_{n \in \mathbb{N}}\) in a category \(\mathcal{C}\) is a pair \((X_{\infty}, (\gamma^{\infty}_n)_{n \in \mathbb{N}})\) consisting of an object \(X_{\infty}\) of \(\mathcal{C}\) (called the vertex of the cocone) together with a sequence \((\gamma^{\infty}_n)_{n \in \mathbb{N}}\) of arrows in \(\mathcal{C}\) (called injections), where \(\gamma^{\infty}_n : X_n \rightarrow X_{\infty}\) for all \(n \in \mathbb{N}\), such that \(\gamma^{\infty}_n = \gamma^{\infty}_{n+1} \circ \gamma_n\) for all \(n \in \mathbb{N}\).

Lemma. For any \(\omega\)-cocone \((X_{\infty}, (\gamma^{\infty}_n)_{n \in \mathbb{N}})\) over an \(\omega\)-chain \((X_n, \gamma_n)_{n \in \mathbb{N}}\) in a category \(\mathcal{C}\), for all \(m, n \in \mathbb{N}\) such that \(m \le n\),

\[\gamma^{\infty}_n \circ \gamma^n_m = \gamma^{\infty}_m.\]

Proof. For any \(m,n \in \mathbb{N}\) such that \(m \le n\), by definition, there exists a \(k \in \mathbb{N}\) such that \(m + k = n\). We will prove by induction on \(k\) that, for all \(k \in \mathbb{N}\) it is the case that, for all \(m,n \in \mathbb{N}\), if \(m + k = n\), then \(\gamma^{\infty}_{m+k} \circ \gamma^{m+k}_m = \gamma^{\infty}_m\). If \(k = 0\), then \(m = n\) and \(\gamma^{\infty}_m \circ \gamma^m_m = \gamma^{\infty}_m \circ \mathrm{id}_{X_m} = \gamma^{\infty}_m\), as required. Suppose that, for some \(k \gt 0\), for all \(m,n \in \mathbb{N}\), \(\gamma^{\infty}_{m+k} \circ \gamma^{m+k}_m = \gamma^{\infty}_m\) whenever \(m \le n\). Then:

\begin{align*}\gamma^{\infty}_{m+k+1} \circ \gamma_m^{m+k+1} &= \gamma^{\infty}_{m+k+1} \circ \gamma_{m+k} \circ \gamma_m^{m+k} & \text{(by definition of \(\gamma_m^{m+k+1}\))} \\&= \gamma^{\infty}_{m+k} \circ \gamma_m^{m+k} & \text{(by definition of \(\omega\)-cocone)} \\&= \gamma^{\infty}_m & \text{(by inductive hypothesis)}.\end{align*}

\(\square\)

Definition (\(\omega\)-colimit). An \(\mathbf{\omega}\)-colimit of an \(\omega\)-chain \((X_n, \gamma_n)_{n \in \mathbb{N}}\) in a category \(\mathcal{C}\) is an \(\omega\)-cocone \((X_{\infty}, (\gamma^{\infty}_n)_{n \in \mathbb{N}})\), such that, for any other \(\omega\)-cocone \((Y, (\mu_n)_{n \in \mathbb{N}})\) over the \(\omega\)-chain, there exists a unique arrow \(\mu : X_{\infty} \rightarrow Y\) such that \(\mu \circ \gamma_n = \mu_n\) for all \(n \in \mathbb{N}\).

Notation. For any \(\omega\)-chain \(((D_n, R_n), \gamma_n)_{n \in \mathbb{N}}\) in \(\mathbf{PER}(CPO^{ep})\), for all \(m,n \in \mathbb{N}\) such that \(m \le n\), we write

\[\gamma_m^n = (i_m^n, p_m^n).\]

Lemma (Characterization of \(\mathbf{\omega}\)-colimits). Let \((D_n, \gamma_n)_{n \in \mathbb{N}}\) be an \(\omega\)-chain in \(\mathbf{CPO}^{ep}\), where \(\gamma_n = (i_n, p_n) : D_n \rightarrow D_{n+1}\) is an admissible embedding-projection pair for every \(n \in \mathbb{N}\). A co-cone \((D_{\infty}, (\gamma^{\infty}_n)_{n \in \mathbb{N}})\) in \(\mathbf{CPO}^{ep}\), where \(\gamma^{\infty}_n = (i^{\infty}_n, p^{\infty}_n)\) is an admissible embedding-projection pair for all \(n \in \mathbb{N}\), is an \(\omega\)-colimit of the \(\omega\)-chain if and only if

\[\bigsqcup_{n \in \mathbb{N}}(i^{\infty}_n \circ p^{\infty}_n) = \mathrm{id}_{D_{\infty}}.\]

Proof.

Sufficiency

Suppose \(\bigsqcup_{n \in \mathbb{N}}(i^{\infty}_n \circ p^{\infty}_n) = \mathrm{id}_{(D_{\infty}, R_{\infty})}\). Consider the following diagram:

Let \((E, \mu_n)_{n \in \mathbb{N}}\) be any co-cone over the \(\omega\)-chain \((D_n, \gamma_n)_{n \in \mathbb{N}}\), where \(\mu_n = (j_n, q_n)\) is an embedding-projection pair for all \(n \in \mathbb{N}\) and \(\mu_n : D_n \rightarrow E\) satisfies \(\mu_{n+1} \circ \gamma_n = \mu_n\) for all \(n \in \mathbb{N}\).

Define the embedding-projection pair \(\mu=(j, q) : D_{\infty}\rightarrow E\) as follows:

\[j = \bigsqcup_{n=0}^{\infty}(j_n \circ p^{\infty}_n),\]

\[q = \bigsqcup_{n=0}^{\infty}(i^{\infty}_n \circ q_n).\]

Properties

• Identity A: \(j \circ i^{\infty}_k = j_k\). For all \(k \in \mathbb{N}\) and \(x \in D_k\),

\begin{align*}j(i^{\infty}_k(x)) &= \bigsqcup_{n=0}^{\infty}j_n(p^{\infty}_n(i^{\infty}_k(x))) \\&= \bigsqcup_{n=k}^{\infty}j_n(p^{\infty}_n(i^{\infty}_k(x))).\end{align*}

For all \(n \ge k\), \(p^{\infty}_n \circ i^{\infty}_k = i^n_k\) and \(j_n \circ i^n_k = j_k\), so we continue

\begin{align*}j(i^{\infty}_k(x)) &= \bigsqcup_{n=k}^{\infty}j_n(p^{\infty}_n(i^{\infty}_k(x))) \\&= \bigsqcup_{n=k}^{\infty}j_n( i^n_k(x)) \\&=\bigsqcup_{n=k}^{\infty}j_k(x) \\&= j_k(x).\end{align*}

• Identity B: \(q \circ j_n = i^{\infty}_n\). For any \(n \in \mathbb{N}\) and \(z \in D_n\):

\begin{align*}q(j_n(z)) &= \bigsqcup_{m=0}^{\infty}i^{\infty}_m(q_m(j_n(z))) \\&= \bigsqcup_{m=n}^{\infty}i^{\infty}_m(q_m(j_n(z))).\end{align*}

For all \(m \ge n\), \(q_m \circ j_n = p^m_n\) and \(i^{\infty}_m \circ p^m_n = i^{\infty}_n\), so we continue

\begin{align*}q(j_n(z)) &= \bigsqcup_{m=n}^{\infty}i^{\infty}_m(q_m(j_n(z))) \\&= \bigsqcup_{m=n}^{\infty}i^{\infty}_m(p^m_n(z))) \\&= \bigsqcup_{m=n}^{\infty} i^{\infty}_n(z) \\&= i^{\infty}_n(z).\end{align*}

Embedding-Projection Pair Verification

• \(q \circ j = \mathrm{id}_D\): We apply Identity B and exploit the continuity of \(q\):

\begin{align*}q(j(x)) &= q\left(\bigsqcup_{n=0}^{\infty} j_n(p^{\infty}_n(x))\right) \\&= \bigsqcup_{n=0}^{\infty} q(j_n(p^{\infty}_n(x))) \\&= \bigsqcup_{n=0}^{\infty}i^{\infty}_n(p^{\infty}_n(x)) \\&= \mathrm{id}_D(x).\end{align*}

• \(j \circ q \sqsubseteq \mathrm{id}_E\). We apply Identity B and exploit the continuity of \(j\):

\begin{align*}j(q(y)) &= j\left(\bigsqcup_{m=0}^{\infty}i^{\infty}_m(q_m(y))\right) \\&= \bigsqcup_{m=0}^{\infty}j(i^{\infty}_m(q_m(y))) \\&= \bigsqcup_{m=0}^{\infty}j_m(q_m(y)) \\&\sqsubseteq \bigsqcup_{m=0}^{\infty}\mathrm{id}_E(y) \\&= y.\end{align*}

Commutativity and Uniqueness

• Commutativity: (\(\mu \circ \gamma^{\infty}_k = \mu_k\)). Note that \(j \circ i^{\infty}_k = j_k\) holds by Identity A. Also, note that

\begin{align*}p^{\infty}_k(q(y)) &= \bigsqcup_{m=0}^{\infty} p^{\infty}_k(i^{\infty}_m(q_m(y))) \\&= \bigsqcup_{m=k}^{\infty} p^{\infty}_k(i^{\infty}_m(q_m(y))) \\&= \bigsqcup_{m=k}^{\infty} i^m_k(q_m(y)) \\&= q_k(y).\end{align*}

• Uniqueness: if \(\mu' = (j', q')\) satisfies \(\mu' \circ \gamma^{\infty}_n = \mu_n\) for all \(n \in \mathbb{N}\), then

\begin{align*}j'(x) &= j'\left( \bigsqcup_{n=0}^\infty i_n^\infty(p_n^\infty(x)) \right) \\&= \bigsqcup_{n=0}^\infty j'(i_n^\infty(p_n^\infty(x))) \\&= \bigsqcup_{n=0}^\infty j_n(p_n^\infty(x)) \\&= j(x),\end{align*}

and similarly, \(q' = q\), so \(\mu' = \mu\) and \(\mu\) is unique.

Necessity

Consider the following diagram:

Suppose \((D, \gamma^{\infty}_n)_{n \in \mathbb{N}}\) is a colimit of \((D_n, \gamma_n)_{n \in \mathbb{N}}\) in \(\mathbf{CPO}^{ep}\). Define \(g : D \rightarrow D\) as

\[g = \bigsqcup_{n=0}^{\infty}(i^{\infty}_n \circ p^{\infty}_n).\]

Since \(i^{\infty}_n \circ p^{\infty}_n \le \mathrm{id}_D\) for all \(n \in \mathbb{N}\), it follows that \(g \le \mathrm{id}_D\).

• Fixed Point CPO: We define a sub-CPO consisting of the fixed points of \(g\) as follows:

\[D' = \{x \in D \mid g(x) = x\}.\]

Note that this is indeed a CPO. Since \(g\) is pointed by construction, it follows that \(g(\bot) = \bot\) and hence \(\bot \in D'\). Since \(g\) is continuous by construction, for any \(\omega\)-chain \((d_n)_{n \in \mathbb{N}}\) in \(D'\), it follows that

\begin{align*}g\left(\bigsqcup_{n \in \mathbb{N}}d_n\right) &= \bigsqcup_{n \in \mathbb{N}}g(d_n) \\&= \bigsqcup_{n \in \mathbb{N}}d_n,\end{align*}

and thus \(\bigsqcup_{n \in \mathbb{N}}d_n \in D'\).

• Co-cone: Because \(g(i^{\infty}_n(x)) = i^{\infty}_n(x)\), it follows that \(i^{\infty}_n(x) \in D'\) for all \(x \in D\), and hence we define \(i'_n : D_n \rightarrow D'\) as \(i'_n = i^{\infty}_n \vert_{D_n}^{D'}\) for all \(n \in \mathbb{N}\). We likewise define \(p'_n = p^{\infty}_n \circ j\) for all \(n \in \mathbb{N}\). Thus, we define \(\gamma'_n = (i'_n, p'_n)\) for all \(n \in \mathbb{N}\) and \(D', \gamma'_n)_{n \in \mathbb{N}}\) is an embedding-projection co-cone over \((D_n, \gamma_n)_{n \in \mathbb{N}}\).
• Universal Property: By the universal property of \((D_n, \gamma_n)_{n \in \mathbb{N}}\), there exists a unique mediating map \(\mu = (j_{\mu}, q_{\mu}) : D \rightarrow D'\) such that \(\mu \circ \gamma^{\infty}_n = \gamma'_n\). The composite \(\gamma \circ \mu : D \rightarrow D\) satisfies

\begin{align*}(\gamma \circ \mu) \circ \gamma^{\infty}_n &= \gamma \circ \gamma'_n \\&= (j \circ i'_n, p'_n \circ q) \\&= (i^{\infty}_n, p^{\infty}_n \circ j \circ q) \\&= (i^{\infty}_n, p^{\infty}_n \circ g) \\&= (i^{\infty}_n, p^{\infty}_n) \\&= \gamma^{\infty}_n.\end{align*}

By the uniqueness of mediating maps for colimits, it follows that \(\gamma \circ \mu = (\mathrm{id}_D, \mathrm{id}_D)\), which implies that \(j \circ j_{\mu} = \mathrm{id}_D\). Since \(j : D' \rightarrow D\) is an inclusion map, it follows that \(D = D'\) and hence \(g = \mathrm{id}_D\). \(\square\)

Construction of Colimits

We will now indicate how to construct colimits in \(\mathbf{CPO}^{ep}\).

Theorem (Construction of Colimits). Given an \(\omega\)-chain \((X_n, (i_n, p_n))_{n \in \mathbb{N}}\) in \(\mathbf{CPO}^{ep}\), the \(\omega\)-cocone \((X_{\infty}, (\varphi_n, \pi_n)_{n \in \mathbb{N}})\) defined as follows is an \(\omega\)-colimit of the \(\omega\)-chain:

\[X_{\infty} = \left\{x \in \prod_{n \in \mathbb{N}}X_n ~\middle|~ \forall n \in \mathbb{N}(x_n = p_n(x_{n+1}))\right\},\]

\[x \sqsubseteq y \Leftrightarrow \forall n \in \mathbb{N}(x_n \sqsubseteq_{X_n} y_n),\]

\[\left[\varphi_n(x)\right]_k = \begin{cases}p_k^n(x) & \text{if } k \lt n \\ x & \text{if } k = n \\ i_n^k & \text{if } k \gt n,\end{cases}\]

\[\pi_n(x) = x_n.\]

Proof. First, we confirm that \((X_{\infty}, \sqsubseteq)\) is a CPO.

Partial Order

Note that, since the order is defined pointwise and each order \(\sqsubseteq_{X_n}\) is a partial order, \(\sqsubseteq\) is likewise a partial order.

Suprema

For any \(\omega\)-chain \((x_n)_{n \in \mathbb{N}}\) in \(X_{\infty}\), the supremum is given by

\[\left(\bigsqcup_{n \in \mathbb{N}}x_n\right)(k) = \bigsqcup_{n \in \mathbb{N}}x_n(k).\]

Note that, for all \(n \in \mathbb{N}\), since \(x_n \sqsubseteq x_{n+1}\), by definition, \(x_n(k) \sqsubseteq x_{n+1}(k)\) and thus \((x_n(k))_{n \in \mathbb{N}}\) is an \(\omega\)-chain in \(X_k\) and thus the supremum \(\bigsqcup_{n \in \mathbb{N}}x_n(k)\) exists, so this is well-defined.

Note that this sequence is coherent:

\begin{align*}p_k\left[\left(\bigsqcup_{n \in \mathbb{N}}x_n\right)(k+1)\right] &= p_k\left(\bigsqcup_{n \in \mathbb{N}}x_n(k+1)\right) \\&= \bigsqcup_{n \in \mathbb{N}}p_k(x_n(k+1)) \\&= \bigsqcup_{n \in \mathbb{N}} x_n(k) \\&= \left(\bigsqcup_{n \in \mathbb{N}} x_n\right)(k).\end{align*}

By definition, \(x_n(k) \sqsubseteq_{X_k} \bigsqcup_{n \in \mathbb{N}}x_n(k)\) for all \(k \in \mathbb{N}\), so \(x_n \sqsubseteq \bigsqcup_{n \in \mathbb{N}}x_n\) and \(\bigsqcup_{n \in \mathbb{N}}x_n\) is an upper bound of the \(\omega\)-chain \((x_n)_{n \in \mathbb{N}}\).

Let \(y \in X_{\infty}\) be any other upper bound of the \(\omega\)-chain \((x_n)_{n \in \mathbb{N}}\). Then, by definition, \(x_n \sqsubseteq y\) for all \(n \in \mathbb{N}\), and thus, for all \(k \in \mathbb{N}\), \(x_n(k) \sqsubseteq y(k)\) and so \(y(k)\) is an upper bound of \((x_n(k))_{n \in \mathbb{N}}\) and thus \(\bigsqcup_{n \in \mathbb{N}} x_n(k) \sqsubseteq y(k)\) and hence \(\bigsqcup_{n \in \mathbb{N}} x_n \sqsubseteq y\) and so \(\bigsqcup_{n \in \mathbb{N}} x_n\) is the least upper bound of \((x_n)_{n \in \mathbb{N}}\).

Least Element

The least element \(\bot_{\infty} \in X_{\infty}\) is defined as

\[\bot_{\infty}(n) = \bot_n \in X_n.\]

For any element \(x \in X_{\infty}\), \(\bot_{\infty}(n) = \bot_n \sqsubseteq x_n\) for all \(n \in \mathbb{N}\) and so \(\bot_{\infty} \sqsubseteq x\).

Note that this sequence is coherent:

\[p_n(\bot_{\infty}(n+1)) = p_n(\bot_{n+1}) = \bot_n = \bot_{\infty}(n).\]

Embeddings

Next, we confirm that the embedding maps \(\varphi_n : X_n \rightarrow X_{\infty}\) are well-defined, i.e., that \(\varphi_n(x)\) is a coherent sequence for all \(x \in X_n\) and \(n \in \mathbb{N}\). Let \(n \in \mathbb{N}\) and \(x \in X_n\). We must show that \(p_k((\varphi_n(x))_{k+1}) = (\varphi_n(x))_k\) for all \(k \in \mathbb{N}\). There are three cases:

• \(k + 1 \lt n\): then \(k \lt n\) and thus \(p_k((\varphi_n(x))_{k+1}) = p_k(p_{k+1}^n(x)) = p_k^n(x) = (\varphi_n(x))_k\);
• \(k + 1 = n\): then \(k \lt n\) and thus \(p_k((\varphi_n(x))_{k+1}) = p_k(x) = (\varphi_n(x))_k\);
• \(k + 1 \gt n\): if \(k \gt n\) then \((\varphi_n(x))_k = i_n^k(x)\) and \(p_k((\varphi_n(x))_{k+1}) = p_k(i_n^{k+1}(x)) = p_k(i_k(i_n^k(x))) = i_n^k(x) = (\varphi_n(x))_k\); if \(k=n\), then \((\varphi_n(x))_k = x\) and \(p_k((\varphi_n(x))_{k+1}) = p_k(i_n^{k+1}(x)) = p_k(i_k^{k+1}(x)) = p_k(i_k(x)) = x = (\varphi_n(x))_k\).

Embedding-Projection Pairs

Next, we confirm that the pairs \((\varphi_n, \pi_n)\) are embedding-projection pairs for all \(n \in \mathbb{N}\).

First, note that, for all \(n \in \mathbb{N}\) and \(x \in X_n\),

\[\pi_n(\varphi_n(x)) = (\varphi_n(x))_n = x,\]

and thus \(\pi_n \circ \varphi_n = \mathrm{id}_{X_n}.\)

Next, we confirm that \(\varphi_n \circ \pi_n \sqsubseteq \mathrm{id}_{X_{\infty}}\) for all \(n \in \mathbb{N}\), i.e., that \(\varphi_n(\pi_n(x)) \sqsubseteq x\) for all \(x \in X_{\infty}\) which means that \((\varphi_n(x_n))_k \sqsubseteq x_k\) for all \(k \in \mathbb{N}\). There are three cases:

• \(k \lt n\): \((\varphi_n(x_n))_k = p_k^n(x_n) = x_k\); we can show by induction that, for any \(k \in \mathbb{N}\), \(p_k^{k+m}(x_{k+m}) = x_k\) for all \(m \in \mathbb{N}\):
  • Base Case: \(m = 0\); \(p_k^k(x_k) = x_k\) holds by definition;
  • Induction: suppose \(p_k^{k+m}(x_{k+m}) = x_k\) for some \(m \in \mathbb{N}\); then \(p_k^{k+m+1}(x_{k+m+1}) = p_k^{k+m}(p_{k+m}(x_{k+m+1})) = p_k^{k+m}(x_{k+m}) = x_k\);
• \(k = n\): \((\varphi_n(x_n))_k = x_n = x_k\);
• \(k \gt n\): \((\varphi_n(x_n))_k = i_n^k(x_n) \sqsubseteq x_k\); we can show by induction that, for any \(n \in \mathbb{N}\), \(i_n^{n+m}(x_n) \sqsubseteq x_{n+m}\):
  • Base Case: \(m=0\); \(i_n^n(x_n) \sqsubseteq x_n\) holds by definition;
  • Induction: suppose \(i_n^{n+m}(x_n) \sqsubseteq x_{n+m}\) for some \(m \in \mathbb{N}\); then \(i_n^{n+m+1}(x_n) = i_{n+m}(i_n^{n+m}(x_n)) \sqsubseteq i_{n+m}(x_{n+m})\) (by inductive hypothesis and monotonicity) and thus, since \(p_{n+m}(x_{n+m+1}) = x_{n+m}\), it follows that \(i_{n+m}(x_{n+m}) = i_{n+m}(p_{n+m}(x_{n+m+1})) \sqsubseteq x_{n+m+1}\).

Commutativity

We now indicate that \((X_{\infty}, (\varphi_n, \pi_n))_{n \in \mathbb{N}}\) is a cocone, i.e., that the following identities hold:

• \(\varphi_{n+1} \circ i_n = \varphi_n\),
• \(p_n \circ \pi_{n+1} = \pi_n\).

Let \(x \in X_n\). For all \(k \in \mathbb{N}\), the following identities hold:

• \((\varphi_{n+1}(i_n(x)))_k = (\varphi_n(x))_k\):
  • Case 1: \(k \lt n+1\);
    • Case 1a: \(k \lt n\): \((\varphi_{n+1}(i_n(x)))_k = p_k^{n+1}(i_n(x)) = p_k^n(p_n(i_n(x))) = p_k^n(x) = (\varphi_n(x))_k\);
    • Case 1b: \(k = n\): \((\varphi_{n+1}(i_n(x)))_k = p_k^{n+1}(i_n(x)) = p_n^{n+1}(i_n(x)) = p_n(i_n(x)) = x = p_n^n(x) = (\varphi_n(x))_k\);
  • Case 2: \(k=n+1\); \((\varphi_{n+1}(i_n(x)))_k = i_n(x) = i_n^{n+1}(x) = (\varphi_n(x))_k\);
  • Case 3: \(k \gt n+1\); \((\varphi_{n+1}(i_n(x)))_k = i_{n+1}^k(i_n(x)) = i_n^k(x) = \varphi_n(x))_k\);

Let \(x \in X_{\infty}\). For all \(n \in \mathbb{N}\), \(p_n(\pi_{n+1}(x)) = p_n(x_{n+1}) = x_n = \pi_n(x)\).

Colimit

When \(k=n\), \((\varphi_n(\pi_n(x)))_k = \pi_n(x) = \pi_k(x) = x_k\). When \(k \gt n\), \((\varphi_n(\pi_n(x)))_k = p_k^n(\pi_n(x)) = p_k^n(x_n) = x_k\). Thus,

\begin{align*}\bigsqcup_{n=0}^{\infty}\varphi_n(\pi_n(x)) &= \bigsqcup_{n=k}^{\infty}\varphi_n(\pi_n(x)) \\&= \bigsqcup_{n=k}^{\infty}x_k \\&= x_k.\end{align*}

It then follows that

\[\left(\bigsqcup_{n=0}^{\infty}\varphi_n(\pi_n(x))\right)(k) = x_k\]

and thus

\[\bigsqcup_{n=0}^{\infty}\varphi_n(\pi_n(x)) = x\]

so

\[\bigsqcup_{n \in \mathbb{N}}(\varphi_n \circ \pi_n) = \mathrm{id}_{X_{\infty}}.\]

Thus, by the Characterization Lemma for \(\omega\)-colimits, \((X_{\infty}, (\varphi_n, \pi_n))_{n \in \mathbb{N}})\) is a colimit of the \(\omega\)-chain \((X_n, (i_n, p_n))_{n \in \mathbb{N}}\). \(\square\)

Functors

In this section, we will define the functors that characterize the recursive domain equations.

Definition (Lifting of a CPO). For any CPO \((D, \sqsubseteq)\), its lifting \((D_{\bot}, \sqsubseteq_{\bot})\) adjoins a least element \(\bot\) as follows:

• \(\bot \notin D\);
• \(D_{\bot} = D \cup \{\bot\}\);
• \(x \sqsubseteq_{\bot} y \Leftrightarrow x = \bot \text{ or } x,y \in D \text{ and } x \sqsubseteq y\).

The supremum of an \(\omega\)-chain in \(D_{\bot}\) is given by

\[\bigsqcup_{n \in \mathbb{N}} d_n = \begin{cases} \bot & \text{if } \forall n \in \mathbb{N} (d_n = \bot) \\ \bigsqcup_{n=N}^{\infty}d_n & \text{if } \exists N \in \mathbb{N} (d_N \ne \bot).\end{cases}\]

Definition (Lifting of a Map). For any continuous map \(f : D \rightarrow E\) between CPOs \(D\) and \(E\), the lifting \(f_{\bot} : D_{\bot} \rightarrow E_{\bot}\) is defined as follows:

\[f_{\bot}(x) = \begin{cases}\bot & \text{if } x = \bot \\ f(x) & \text{otherwise} \end{cases}.\]

Lemma. Let \((d_n)_{n \in \mathbb{N}}\) be an \(\omega\)-chain of continuous maps in \(\mathrm{Cont}(D, D)\) for a CPO \(D\) and let \((e_n)_{n \in \mathbb{N}}\) be an \(\omega\)-chain of continuous maps in \(\mathrm{Cont}(E, E)\) for a CPO \(E\) such that

\[\bigsqcup_{n \in \mathbb{N}}d_n = \mathrm{id}_{D}\]

and

\[\bigsqcup_{n \in \mathbb{N}}e_n = \mathrm{id}_{E};\]

then, for any map \(f \in \mathrm{Cont}(D, E)\),

\[\bigsqcup_{n \in \mathbb{N}}(e_n \circ f \circ d_n) = f.\]

Proof. Note that the sequence \((e_n(f(d_n(x))))_{n \in \mathbb{N}}\) is jointly monotone. Then:

\begin{align}\left(\bigsqcup_{n \in \mathbb{N}}(e_n \circ f \circ d_n)\right)(x) &= \bigsqcup_{n \in \mathbb{N}}(e_n \circ f \circ d_n)(x) \\&= \bigsqcup_{n \in \mathbb{N}}e_n(f(d_n(x))) \\&= \bigsqcup_{m \in \mathbb{N}}\bigsqcup_{n \in \mathbb{N}}e_m(f(d_n(x))) \\&= \bigsqcup_{m \in \mathbb{N}}e_m\left(\bigsqcup_{n \in \mathbb{N}}f(d_n(x))\right) \\&= \left(\bigsqcup_{m \in \mathbb{N}}e_m\right)\left(\bigsqcup_{n \in \mathbb{N}}f(d_n(x))\right) \\&= \left(\bigsqcup_{m \in \mathbb{N}}e_m\right)\left(f\left(\bigsqcup_{n \in \mathbb{N}}d_n(x)\right)\right) \\&= \left(\bigsqcup_{m \in \mathbb{N}}e_m\right)\left(f\left(\left(\bigsqcup_{n \in \mathbb{N}}d_n\right)(x)\right)\right) \\&= \left(\left(\bigsqcup_{m \in \mathbb{N}}e_m\right) \circ f \circ \left(\bigsqcup_{n \in \mathbb{N}}d_n\right)\right)(x) \\&= (\mathrm{id}_E \circ f \circ \mathrm{id}_D)(x) \\&= f(x).\end{align}

\(\square\)

Call-by-Name

For the call-by-name strategy, it is necessary to distinguish the bottom element of \(\mathrm{Cont}(D, D)\) (which is the constant map \(d \mapsto \bot\)) from non-termination; the former applies to terms like \((\lambda x . \Omega)\) for a divergent term \(\Omega\).

Definition (Call-by-name Functor). The call-by-name functor \(F_{\mathrm{n}} : \mathbf{CPO}^{ep} \rightarrow \mathbf{CPO}^{ep}\) is defined as follows:

• Objects: \(F_{\mathrm{n}}(D) = (\mathrm{Cont}(D, D))_{\bot}\);
• Arrows: \(F_{\mathrm{n}}(i, p) = (F_{\mathrm{n}}(i), F_{\mathrm{n}}(p))\), where
  • \(F_{\mathrm{n}}(i) = f \mapsto \begin{cases}\bot & \text{if } f = \bot \\ i \circ f \circ p & \text{otherwise} \end{cases}\),
  • \(F_{\mathrm{n}}(p) = g \mapsto \begin{cases}\bot & \text{if } g = \bot \\ p \circ g \circ i & \text{otherwise} \end{cases}\).

Theorem (Preservation of Colimits). The functor \(F_{\mathrm{n}}\) preserves all colimits of \(\omega\)-chains, i.e., for any \(\omega\)-chain \((X_n, (i_n, p_n))_{n \in \mathbb{N}}\) in \(\mathbf{CPO}^{ep}\), if the \(\omega\)-cocone \((X_{\infty}, (\varphi_n, \pi_n)_{n \in \mathbb{N}})\) is a colimit of this \(\omega\)-chain, then the \(\omega\)-cocone \((F_{\mathrm{n}}(X_{\infty}), (F_{\mathrm{n}}(\varphi_n), F_{\mathrm{n}}(\pi_n))_{n \in \mathbb{N}})\) is a colimit of the \(\omega\)-chain \((F_{\mathrm{n}}(X_n), (F_{\mathrm{n}}(i_n), F_{\mathrm{n}}(p_n)))_{n \in \mathbb{N}}\).

Proof. For any \(f \in (\mathrm{Cont}(X_{\infty}, X_{\infty}))_{\bot}\), if \(f = \bot\) then

\[(F_{\mathrm{n}}(\varphi_n) \circ F_{\mathrm{n}}(\pi_n))(\bot) = \bot = \mathrm{id}_{F_{\mathrm{n}}(X_{\infty})}(\bot).\]

If \(f \in \mathrm{Cont}(X_{\infty}, X_{\infty})\), the observe the following (where we utilize the above lemma and the Characterization Lemma):

\begin{align*}\left(\bigsqcup_{n \in \mathbb{N}}F_{\mathrm{n}}(\varphi_n) \circ F_{\mathrm{n}}(\pi_n)\right)(f) &= \bigsqcup_{n \in \mathbb{N}}(F_{\mathrm{n}}(\varphi_n) \circ F_{\mathrm{n}}(\pi_n))(f) \\&= \bigsqcup_{n \in \mathbb{N}}F_{\mathrm{n}}(\varphi_n)(F_{\mathrm{n}}(\pi_n)(f)) \\&= \bigsqcup_{n \in \mathbb{N}}F_{\mathrm{n}}(\varphi_n)(\pi_n \circ f \circ \varphi_n) \\&= \bigsqcup_{n \in \mathbb{N}}(\varphi_n \circ (\pi_n \circ f \circ \varphi_n) \circ \pi_n) \\&= \bigsqcup_{n \in \mathbb{N}}((\varphi_n \circ \pi_n) \circ f \circ (\varphi_n \circ \pi_n)) \\&= f \\&= \mathrm{id}_{F_{\mathrm{n}}(X_{\infty})}(f).\end{align*}

Thus, in all cases,

\[\bigsqcup_{n \in \mathbb{N}}F_{\mathrm{n}}(\varphi_n) \circ F_{\mathrm{n}}(\pi_n) = \mathrm{id}_{F_{\mathrm{n}}(X_{\infty})},\]

and so the result follows by the Characterization Lemma. \(\square\)

Call-by-Value

For the call-by-value strategy, computations are distinguished from values. Implicitly, we solve the recursive equation \((V, C) \cong (\mathrm{Cont}(V, C), V_{\bot})\) which implies that \(V \cong (\mathrm{Cont}(V, V_{\bot}))_{\bot}\).

Definition (Call-by-value Functor). The call-by-value functor \(F_{\mathrm{v}} : \mathbf{CPO}^{ep} \rightarrow \mathbf{CPO}^{ep}\) is defined as follows:

• Objects: \(F_{\mathrm{v}}(D, R) = (\mathrm{Cont}(D, D_{\bot}))_{\bot}\);
• Arrows: \(F_{\mathrm{v}}(i, p) = (F_{\mathrm{v}}(i), F_{\mathrm{v}}(p))\), where
  • \(F_{\mathrm{v}}(i) = f \mapsto \begin{cases}\bot & \text{if } f = \bot \\ i_{\bot} \circ f \circ p & \text{otherwise} \end{cases}\),
  • \(F_{\mathrm{v}}(p) = g \mapsto \begin{cases}\bot & \text{if } g = \bot \\ p_{\bot} \circ g \circ i & \text{otherwise} \end{cases}\).

Theorem (Preservation of Colimits). The functor \(F_{\mathrm{v}}\) preserves all colimits of \(\omega\)-chains, i.e., for any \(\omega\)-chain \((X_n, (i_n, p_n))_{n \in \mathbb{N}}\) in \(\mathbf{CPO}^{ep}\), if the \(\omega\)-cocone \((X_{\infty}, (\varphi_n, \pi_n)_{n \in \mathbb{N}})\) is a colimit of this \(\omega\)-chain, then the \(\omega\)-cocone \((F_{\mathrm{v}}(X_{\infty}), (F_{\mathrm{v}}(\varphi_n), F_{\mathrm{v}}(\pi_n))_{n \in \mathbb{N}})\) is a colimit of the \(\omega\)-chain \((F_{\mathrm{v}}(X_n), (F_{\mathrm{v}}(i_n), F_{\mathrm{v}}(p_n)))_{n \in \mathbb{N}}\).

Proof. For any \(f \in (\mathrm{Cont}(X_{\infty}, (X_{\infty})_{\bot}))_{\bot}\), if \(f = \bot\) then

\[(F_{\mathrm{v}}(\varphi_n) \circ F_{\mathrm{v}}(\pi_n))(\bot) = \bot = \mathrm{id}_{F_{\mathrm{v}}(X_{\infty})}(\bot).\]

Note that

\[\bigsqcup_{n \in \mathbb{N}}(\varphi_n \circ \pi_n)_{\bot} = \mathrm{id}_{(X_{\infty})_{\bot}}.\]

If \(f \in \mathrm{Cont}(X_{\infty}, (X_{\infty})_{\bot})\), the observe the following (where we utilize the above lemma and the Characterization Lemma):

\begin{align*}\left(\bigsqcup_{n \in \mathbb{N}}F_{\mathrm{v}}(\varphi_n) \circ F_{\mathrm{v}}(\pi_n)\right)(f) &= \bigsqcup_{n \in \mathbb{N}}(F_{\mathrm{v}}(\varphi_n) \circ F_{\mathrm{v}}(\pi_n))(f) \\&= \bigsqcup_{n \in \mathbb{N}}F_{\mathrm{v}}(\varphi_n)(F_{\mathrm{v}}(\pi_n)(f)) \\&= \bigsqcup_{n \in \mathbb{N}}F_{\mathrm{v}}(\varphi_n)((\pi_n)_{\bot} \circ f \circ \varphi_n) \\&= \bigsqcup_{n \in \mathbb{N}}((\varphi_n)_{\bot} \circ ((\pi_n)_{\bot} \circ f \circ \varphi_n) \circ \pi_n) \\&= \bigsqcup_{n \in \mathbb{N}}((\varphi_n \circ \pi_n)_{\bot} \circ f \circ (\varphi_n \circ \pi_n)) \\&= f \\&= \mathrm{id}_{F_{\mathrm{v}}(X_{\infty})}(f).\end{align*}

Thus, in all cases,

\[\bigsqcup_{n \in \mathbb{N}}F_{\mathrm{v}}(\varphi_n) \circ F_{\mathrm{v}}(\pi_n) = \mathrm{id}_{F_{\mathrm{v}}(X_{\infty})},\]

and so the result follows by the Characterization Lemma. \(\square\)

Initial Object

The initial object \(D_0\) in \(\mathbf{CPO}^{ep}\) is defined as follows:

\[D_0 = \{\bot\}.\]

For any object \(D\), since maps are pointed, there is a unique map \((i, p) : D_0 \rightarrow D\) defined as \(i(\bot) = \bot\) and \(p(d) = \bot\). These maps satisfy \((p \circ i)(\bot) = \bot\) and \((i \circ p)(d) = \bot \sqsubseteq d\) as required.

Initial Algebras and Fixed Points

In this section, we prove an important lemma about the construction of initial algebras.

Definition (Algebra for a Functor). An algebra for an functor \(F : \mathcal{C} \rightarrow \mathcal{C}\) on a category \(\mathcal{C}\) is a pair \((A, a)\) consisting of an object \(A\) of \(\mathcal{C}\) (called the carrier of the algebra) and an arrow \(a : F(A) \rightarrow A\) (called the operation of the algebra).

Definition (Initial Algebra). An initial algebra for a functor \(F : \mathcal{C} \rightarrow \mathcal{C}\) on a category \(\mathcal{C}\) is an algebra \((A, a)\) for \(F\) such that, for any algebra \((B, b)\) for \(F\), there exists a unique arrow \(\rho : A \rightarrow B\) such that \(\rho \circ a = b \circ F(\rho)\), i.e., the following diagram commutes:

Lemma (Fixed Point). Let \((A,a)\) be an initial algebra for a functor \(F\) on a category \(\mathcal{C}\). Then \(a\) is an isomorphism and \(F(A) \cong A\).

Proof. Consider the following diagram:

Since \((F(A), F(a))\) is an algebra for \(F\) and \((A,a)\) is initial, by definition, there exists a unique arrow \(\rho : A \rightarrow F(A)\) such that \(\rho \circ a = F(a) \circ F(\rho)\). It then follows that

\begin{align*}(a \circ \rho) \circ a &= a \circ (\rho \circ a) \\&= a \circ (F(a) \circ F(\rho)) \\&= a \circ F(a \circ \rho).\end{align*}

Since \((A,a)\) is initial, there exists a unique map, namely \(\mathrm{id}_A : A \rightarrow A\) such that \(\mathrm{id}_A \circ a = a \circ F(\mathrm{id}_A)\). However, \(a \circ \rho\) is another map such that \((a \circ \rho) \circ a = a \circ F(a \circ \rho)\), so \(a \circ \rho = \mathrm{id}_A\). It then follows that

\begin{align*}\rho \circ a &= F(a) \circ F(\rho) \\&= F(a \circ \rho) \\&= F(\mathrm{id}_A) \\&= \mathrm{id}_{F(A)}.\end{align*}

Since \(a \circ \rho = \mathrm{id}_A\) and \(\rho \circ a = \mathrm{id}_{F(A)}\), \(F(A) \cong A\). \(\square\)

Lemma (Initial Algebra). Let \(\mathcal{C}\) be any category with an initial object \(0_{\mathcal{C}}\) and all colimits of \(\omega\)-chains and \(F : \mathcal{C} \rightarrow \mathcal{C}\) be any functor that preserves colimits of \(\omega\)-chains. Let \((C_{\infty}, (\varphi_n)_{n \in \mathbb{N}})\) be the colimit of the \(\omega\)-chain \((F^n(0_{\mathcal{C}}), F^n(i))_{n \in \mathbb{N}}\), where \(i : 0_{\mathcal{C}} \rightarrow F(0_{\mathcal{C}})\) is the unique map from the initial object to \(F(0_{\mathcal{C}})\). Then there exists an arrow \(\theta : F(C_{\infty}) \rightarrow C_{\infty}\) such that \((C_{\infty}, \theta)\) is an initial algebra for \(F\).

Proof. Since \((C_{\infty}, (\varphi_n)_{n \in \mathbb{N}})\) is the colimit of the \(\omega\)-chain \((F^n(0_{\mathcal{C}}), F^n(i))_{n \in \mathbb{N}}\), the following diagram commutes for all \(n \in \mathbb{N}\):

Since \(F\) preserves colimits of \(\omega\)-chains, the \(\omega\)-cocone \((F(C_{\infty}), (F(\varphi_n))_{n \in \mathbb{N}})\) is a colimit of the \(\omega\)-chain \((F(F^n(0_{\mathcal{C}})), F(F^n(i)))_{n \in \mathbb{N}}\) (equivalently \((F^{n+1}(0_{\mathcal{C}}), F^{n+1}(i))_{n \in \mathbb{N}}\)), and hence the following diagram commutes for all \(n \in \mathbb{N}\):

Since \((C_{\infty}, (\varphi_{n+1})_{n \in \mathbb{N}})\) is an \(\omega\)-cocone for the \(\omega\)-chain \((F^{n+1}(0_{\mathcal{C}}), F^{n+1}(i))_{n \in \mathbb{N}}\), by the universal property of colimits of \(\omega\)-chains, there exists a unique map \(\theta : F(C_{\infty}) \rightarrow C_{\infty}\) such that \(\theta \circ F(\varphi_n) = \varphi_{n+1}\) for all \(n \in \mathbb{N}\), i.e., the following diagram commutes:

Let \((C, c)\) be any algebra for \(F\). We define an \(\omega\)-cocone \((C, (c_n)_{n \in \mathbb{N}})\) where the maps \(c_n : F^{n+1}(0_{\mathcal{C}}) \rightarrow C\) are defined recursively as follows in terms of the unique map \(j : 0_{\mathcal{C}} \rightarrow C\) from the initial object into \(C\):

• \(c_0 = c \circ F(j)\),
• \(c_{n+1} = c \circ F(c_n)\).

We will verify by induction that this is indeed an \(\omega\)-cocone, i.e., that \(c_{n+1} \circ F^{n+1}(i) = c_n\) for all \(n \in \mathbb{N}\). When \(n=0\), note that

\begin{align*}c_1 \circ F(i) &= c \circ F(c_0) \circ F(i) \\&= c \circ F(c_0 \circ i),\end{align*}

and, since \(c_0 \circ i : 0_{\mathcal{C}} \rightarrow C\) and \(j : 0_{\mathcal{C}} \rightarrow C\) is unique, it follows that \(c_0 \circ i = j\) and hence \(c \circ F(c_0 \circ i) = c \circ F(j)\) and \(c_1 \circ F(i) = c \circ F(j) = c_0\). Next, suppose that \(c_{n+1} \circ F^{n+1}(i) = c_n\) for some \(n \in \mathbb{N}\). Then,

\begin{align*}c_{n+2} \circ F^{n+2}(i) &= c \circ F(c_{n+1}) \circ F^{n+2}(i) \\&= c \circ F(c_{n+1}) \circ F(F^{n+1}(i)) \\&= c \circ F(c_{n+1} \circ F^{n+1}(i)) \\&= c \circ F(c_n) \\&= c_{n+1}.\end{align*}

Since \((C_{\infty}, (\varphi_{n+1})_{n \in \mathbb{N}})\) is also a colimit of the \(\omega\)-chain \((F^{n+1}(0_{\mathcal{C}}), F^{n+1}(i))_{n \in \mathbb{N}}\), by the universal property of colimits of \(\omega\)-chains, there exists a unique arrow \(\rho : C_{\infty} \rightarrow C\) such that \(\rho \circ \varphi_{n+1} = c_n\) for all \(n \in \mathbb{N}\), i.e., the following diagram commutes:

Similarly, since \((F(C_{\infty}), (F(\varphi_n))_{n \in \mathbb{N}})\) is a colimit of the \(\omega\)-chain \((F^{n+1}(0_{\mathcal{C}}), F^{n+1}(i))_{n \in \mathbb{N}}\), by the universal property of colimits of \(\omega\)-chains, there exists a unique arrow \(\mu : F(C_{\infty}) \rightarrow C\) such that \(\mu \circ F(\varphi_n) = c_n\) for all \(n \in \mathbb{N}\), i.e., the following diagram commutes:

Our goal is to indicate that \(\rho\) is the unique map such that \(\rho \circ \theta = c \circ F(\rho)\), i.e., the unique map making the following diagram commute:

Note that, when \(n=0\), since \(\rho \circ \varphi_0 : 0_{\mathcal{C}} \rightarrow C\), it follows that \(\rho \circ \varphi_0 = j\), and thus

\begin{align*}c \circ F(\rho) \circ F(\varphi_0) &= c \circ F(\rho \circ \varphi_0) \\&= c \circ F(j) \\&= c_0.\circ\end{align*}

Likewise,

\begin{align*}c \circ F(\rho) \circ F(\varphi_{n+1}) &= c \circ F(\rho \circ \varphi_{n+1}) \\&= c \circ F(c_n) \\&= c_{n+1}.\end{align*}

Thus, for all \(n \in \mathbb{N}\), \((c \circ F(\rho)) \circ F(\varphi_n) = c_n\), and, since \(\mu\) is the unique mediating map, it follows that \(c \circ F(\rho) = \mu\).

Note also that

\begin{align*}\rho \circ \theta \circ F(\varphi_n) &= \rho \circ \varphi_{n+1} \\&= c_n.\end{align*}

It follows that \(\rho \circ \theta = \mu\) and hence \(\rho \circ \theta = c \circ F(\rho)\).

Finally, suppose that there exists another map \(\rho' : C_{\infty} \rightarrow C\) such that \(\rho' \circ \theta = c \circ F(\rho')\). When \(n=0\),

\begin{align*}\rho' \circ \varphi_1 &= \rho' \circ \theta \circ F(\varphi_0) \\&= c \circ F(\rho') \circ F(\varphi_0) \\&= c \circ F(\rho' \circ \varphi_0) \\&= c \circ F(j) \\&= c_0.\end{align*}

Likewise,

\begin{align*}\rho' \circ \varphi_{n+2} &= \rho' \circ \theta \circ F(\varphi_{n+1}) \\&= c \circ F(\rho') \circ F(\varphi_{n+1}) \\&= c \circ F(\rho' \circ \varphi_{n+1}) \\&= c \circ F(c_n) \\&= c_{n+1}.\end{align*}

Thus, for all \(n \in \mathbb{N}\), \(\rho' \circ \varphi_{n+1} = c_n\). Since \(\rho\) is the unique such mediating map, it follows that \(\rho = \rho'\). \(\square\)

Summary

We now summarize the results up to this point.

1. The category \(\mathbf{CPO}^{ep}\) has all colimits of \(\omega\)-chains.
2. The functors \(F_{\mathrm{v}}\) and \(F_{\mathrm{n}}\) used to define the call-by-value and call-by-name models, respectively, are locally continuous.
3. By the local continuity lemma, the functors \(F_{\mathrm{v}}\) and \(F_{\mathrm{n}}\) preserve all colimits of \(\omega\)-chains.
4. By the initial algebra lemma, there exist fixed points \(\mu F_{\mathrm{v}}\) and \(\mu F_{\mathrm{n}}\) in the category \(\mathbf{CPO}^{ep}\) such that \(F_{\mathrm{v}}(\mu F_{\mathrm{v}}) \cong \mu F_{\mathrm{v}}\) and \(F_{\mathrm{n}}(\mu F_{\mathrm{n}}) \cong \mu F_{\mathrm{n}}\) and \(\mu F_{\mathrm{v}}\) is the carrier of the initial algebra for \(F_{\mathrm{v}}\) and \(\mu F_{\mathrm{n}}\) is the carrier of the initial algebra for \(F_{\mathrm{n}}\). We designate these fixed points as \(D_{\infty}^{\mathrm{v}} = \mu F_{\mathrm{v}}\) and \(D_{\infty}^{\mathrm{n}} = \mu F_{\mathrm{n}}\). Thus, \(D_{\infty}^{\mathrm{v}} \cong (\mathrm{Cont}(D_{\infty}^{\mathrm{v}}, (D_{\infty}^{\mathrm{v}})_{\bot}))_{\bot}\) and \(D_{\infty}^{\mathrm{n}} \cong (\mathrm{Cont}(D_{\infty}^{\mathrm{n}}, D_{\infty}^{\mathrm{n}}))_{\bot}\).
5. By the bilimit lemma, since these fixed points are colimits within \(\mathbf{CPO}^{ep}\), there is a corresponding colimit in \(\mathbf{CPO}^e\). By the isomorphism lemma, the carrier of this colimit is also the carrier of an initial algebra and so \(D_{\infty}^{\mathrm{v}}\) is the fixed point of \(F_{\mathrm{v}}^e\) and \(D_{\infty}^{\mathrm{n}}\) is the fixed point of \(F_{\mathrm{n}}^e\) in the category \(\mathbf{CPO}^e\).
6. By the bilimit lemma and isomorphism lemma, since \(\mathbf{CPO}^{ep}\) has all colimits, so does \((\mathbf{CPO}^p)^{op}\). Likewise, since the functor \(F_{\mathrm{v}}\) preserves all colimits, so does the functor \((F_{\mathrm{v}}^p)^{op}\). This means that there exists a fixed point \(\mu (F_{\mathrm{v}}^p)^{op}\) in \((\mathbf{CPO}^p)^{op}\), which is a fixed point \(\nu F_{\mathrm{v}}^p\) of \(F_{\mathrm{v}}^p\) in \(\mathbf{CPO}^p\) (and carries the respective final coalgebra). Moreover, \(\nu F_{\mathrm{v}}^p = D_{\infty}^{\mathrm{v}}\). Thus, there is a coincidence of the carriers for the initial and final coalgebras. Similarly, there is a fixed point \(\nu F_{\mathrm{n}}^p = D_{\infty}^{\mathrm{n}}\).

The PERs

We will now define the PERs used for each model.

Call-by-Name

We define a PER as follows: first, we define a monotone map \(F : \mathcal{P}(D^{\mathrm{n}}_{\infty} \times D^{\mathrm{n}}_{\infty})\) as follows:

\[F(R) = \left\{(d_1, d_2) \in D^{\mathrm{n}}_{\infty} \times D^{\mathrm{n}}_{\infty} \middle| \begin{aligned}& d_1 \ne \bot \Rightarrow d_2 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{n}}_{\infty}(e_1 \mathrel{R} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R} (d_2 \cdot e_2)) \\ &\land \\ & d_2 \ne \bot \Rightarrow d_1 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{n}}_{\infty}(e_1 \mathrel{R} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R} (d_2 \cdot e_2)) \end{aligned}\right\}.\]

By the Tarski-Knaster theorem, there exists a greatest fixed point of this map:

\[R^{\mathrm{n}}_{\infty} = \nu F.\]

Thus, since \(F(R^{\mathrm{n}}_{\infty}) = R^{\mathrm{n}}_{\infty}\), it follows that

\[d_1 \mathrel{R^{\mathrm{n}}_{\infty}} d_2 \Leftrightarrow \begin{aligned}& d_1 \ne \bot \Rightarrow d_2 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{n}}_{\infty}(e_1 \mathrel{R^{\mathrm{n}}_{\infty}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R^{\mathrm{n}}_{\infty}} (d_2 \cdot e_2)) \\ &\land \\ & d_2 \ne \bot \Rightarrow d_1 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{n}}_{\infty}(e_1 \mathrel{R^{\mathrm{n}}_{\infty}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R^{\mathrm{n}}_{\infty}} (d_2 \cdot e_2)) \end{aligned}.\]

Call-by-Value

We define a PER as follows: first, we define a monotone map \(F : \mathcal{P}(D^{\mathrm{v}}_{\infty} \times D^{\mathrm{v}}_{\infty})\) as follows:

\[F(R) = \left\{(d_1, d_2) \in D^{\mathrm{v}}_{\infty} \times D^{\mathrm{v}}_{\infty} \middle| \begin{aligned}& d_1 \ne \bot \Rightarrow d_2 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{v}}_{\infty}(e_1 \ne \bot \land e_2 \ne \bot \land e_1 \mathrel{R} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R} (d_2 \cdot e_2)) \\ &\land \\ & d_2 \ne \bot \Rightarrow d_1 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{v}}_{\infty}(e_1 \ne \bot \land e_2 \ne \bot \land e_1 \mathrel{R} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R} (d_2 \cdot e_2)) \end{aligned}\right\}.\]

By the Tarski-Knaster theorem, there exists a greatest fixed point of this map:

\[R^{\mathrm{v}}_{\infty} = \nu F.\]

Thus, since \(F(R^{\mathrm{v}}_{\infty}) = R^{\mathrm{v}}_{\infty}\), it follows that

\[d_1 \mathrel{R^{\mathrm{v}}_{\infty}} d_2 \Leftrightarrow \begin{aligned}& d_1 \ne \bot \Rightarrow d_2 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{v}}_{\infty}(e_1 \ne \bot \land e_2 \ne \bot \land e_1 \mathrel{R^{\mathrm{v}}_{\infty}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R^{\mathrm{v}}_{\infty}} (d_2 \cdot e_2)) \\ &\land \\ & d_2 \ne \bot \Rightarrow d_1 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{v}}_{\infty}(e_1 \ne \bot \land e_2 \ne \bot \land e_1 \mathrel{R^{\mathrm{v}}_{\infty}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{R^{\mathrm{v}}_{\infty}} (d_2 \cdot e_2)) \end{aligned}.\]

The Models

Now we are prepared to define the models.

Call-by-Name

The call-by-name model \(\mathcal{M}_{\mathrm{n}}\) is defined as follows:

• Semantic Domain: \(D_{\infty}^{\mathrm{n}}\);
• PER: \(R_{\infty}^{\mathrm{n}}\);
• Application: for all \(d_1, d_2 \in D_{\infty}^{\mathrm{n}}\), \[d_1 \cdot d_2 = \begin{cases}\bot & \text{if } \theta_{\mathrm{n}}(d_1) = \bot \\ \theta_{\mathrm{n}}(d_1)(d_2) & \text{otherwise} \end{cases}\];
• Denotation:
  • Variables: \(\llbracket x \rrbracket_{\rho} = \rho(x)\) for all variables \(x \in \mathcal{V}\) and environments \(\rho \in \mathrm{Env}(R_{\infty}^{\mathrm{n}})\);
  • Abstraction: \(\llbracket (\lambda x . M) \rrbracket_{\rho} = \theta^{-1}_{\mathrm{n}}\left(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\right)\) for all variables \(x \in \mathcal{V}\), terms \(M \in \Lambda\), and environments \(\rho \in \mathrm{Env}(R_{\infty}^{\mathrm{n}})\);
  • Application: \(\llbracket (MN) \rrbracket_{\rho} = \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho}\) for all terms \(M, N \in \Lambda\), and environments \(\rho \in \mathrm{Env}(R_{\infty}^{\mathrm{n}})\).

We verify the model axioms.

Lemma (Bottom Uniqueness). For any \(x \in D^{\mathrm{n}}_{\infty}\), \(x \mathrel{R_{\infty}^{\mathrm{n}}} \bot\) if and only if \(x = \bot\) and hence the equivalence class of \(\bot\) is a singleton set, i.e., \([\bot] = \{\bot\}\).

Proof. Suppose \(x \mathrel{R_{\infty}^{\mathrm{n}}} \bot\). Then, if \(x \ne \bot\), it follows that \(\bot \ne \bot\), a contradiction, so \(x = \bot\). Conversely, it is vacuously the case that \(\bot \mathrel{R_{\infty}^{\mathrm{n}}} \bot\). \(\square\)

Continuity

We confirm that the denotation of abstractions \(\llbracket (\lambda x . M) \rrbracket_{\rho} = \theta_{\mathrm{n}}^{-1}\left(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\right)\) is well-defined, i.e., that the function \(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\) is indeed a continuous map. We proceed by structural induction on the body \(M\) of the abstraction.

• Variables \((M=y)\).
  • Case 1: \((y=x)\). Then \(d \mapsto \llbracket x \rrbracket_{\rho[x \mapsto d]}\) is simply the identity map \(d \mapsto d\), which is continuous.
  • Case 2: \((y \ne x)\). Then \(d \mapsto \llbracket y \rrbracket_{\rho[x \mapsto d]}\) is simply the constant map \(d \mapsto \rho(y)\), which is continuous.
• Abstractions \((M = (\lambda y . M'))\). By definition, \[d \mapsto \llbracket (\lambda y . M') \rrbracket_{\rho[x \mapsto d]} = d \mapsto \theta_{\mathrm{n}}^{-1}\left(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\right).\] By inductive hypothesis on the subterm \(M'\), the map \(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\) is continuous for every value of \(d\), and hence the expression \(\theta_{\mathrm{n}}^{-1}\left(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\right)\) is well-defined and the composite map \(d \mapsto \theta_{\mathrm{n}}^{-1}\left(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\right)\) is continuous since it is the composition of two continuous maps.
• Applications \(M = (M_1M_2)\). By definition, \begin{align*}d \mapsto \llbracket (M_1M_2) \rrbracket_{\rho[x \mapsto d]} &= d \mapsto \llbracket M_1 \rrbracket_{\rho[x \mapsto d]} \cdot \llbracket M_1 \rrbracket_{\rho[x \mapsto d]} \\&= d \mapsto \theta_{\mathrm{n}}\left(\llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\right)\left(\llbracket M_2 \rrbracket_{\rho[x \mapsto d]}\right).\end{align*} By inductive hypothesis on the sub-terms \(M_1\) and \(M_2\), the maps \(d \mapsto \llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\) and \(d \mapsto \llbracket M_2 \rrbracket_{\rho[x \mapsto d]}\) are continuous. By definition, the map \(\theta_{\mathrm{n}}\left(\llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\right)\) is continuous, and hence so is the composite map \(d \mapsto \theta_{\mathrm{n}}\left(\llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\right)\left(\llbracket M_2 \rrbracket_{\rho[x \mapsto d]}\right)\).

Well-Definedness
We confirm that \(\llbracket M \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{n}}_{\infty})\) for all terms \(M \in \Lambda\). we proceed by structural induction on \(M\).

• Variables: \((M=x)\); \(\llbracket x \rrbracket_{\rho} = \rho(x) \in \mathrm{dom}(R^{\mathrm{n}}_{\infty})\) by construction;
• Abstractions: \((M = (\lambda x . M'))\). Suppose \(\llbracket (\lambda x . M') \rrbracket_{\rho} \ne \bot\). By definition, \(\llbracket (\lambda x . M') \rrbracket_{\rho} = \theta_{\mathrm{n}}^{-1}(d \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d]})\). Suppose \(e_1, e_2 \in D^{\mathrm{n}}_{\infty}\) and \(e_1 \mathrel{R^{\mathrm{n}}_{\infty}} e_2\). By definition, since \(\llbracket (\lambda x . M') \rrbracket_{\rho} \ne \bot\), it follows that \(\llbracket (\lambda x . M') \rrbracket_{\rho} \cdot e_1 = \theta_{\mathrm{n}}(\theta_{\mathrm{n}}^{-1}(d \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d]}))(e_1) = \llbracket M' \rrbracket_{\rho[x \mapsto e_1]}\). Likewise, \(\llbracket (\lambda x . M') \rrbracket_{\rho} \cdot e_2 = \llbracket M' \rrbracket_{\rho[x \mapsto e_2]}\). By Environmental Consistency, since \(e_1 \mathrel{R^{\mathrm{n}}_{\infty}} e_2\), it follows that \(\llbracket M' \rrbracket_{\rho[x \mapsto e_1]} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket M' \rrbracket_{\rho[x \mapsto e_2]}\). Thus \(\llbracket (\lambda x . M') \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket (\lambda x . M') \rrbracket_{\rho}\) and so \(\llbracket (\lambda x . M') \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{n}}_{\infty})\).
• Applications: \((M = (NP))\). By inductive hypothesis, \(\llbracket N \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{n}}_{\infty})\) and \(\llbracket P \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{n}}_{\infty})\). By definition, \(\llbracket (NP) \rrbracket_{\rho} = \llbracket N \rrbracket_{\rho} \cdot \llbracket P \rrbracket_{\rho}\), and by Congruence, \(\llbracket (MN) \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket (MN) \rrbracket_{\rho}\).

Thus, the semantic denotation map is well-defined.

Congruence

Let \(f,g,x,y \in D^{\mathrm{n}}_{\infty}\) and suppose that \(f \mathrel{R^{\mathrm{n}}_{\infty}} g\) and \(x \mathrel{R^{\mathrm{n}}_{\infty}} y\).

• If \(f = \bot\) and \(g = \bot\), then \(f \cdot x = \bot\) and \(g \cdot y = \bot\) and it is vacuously the case that \(\bot \mathrel{R^{\mathrm{n}}_{\infty}} \bot\).
• If \(f \ne \bot\), then, since \(f \mathrel{R^{\mathrm{n}}_{\infty}} g\), it follows that \(g \ne \bot\) and \((f \cdot x) \mathrel{R^{\mathrm{n}}_{\infty}} (g \cdot y)\).
• Similarly, if \(g \ne \bot\), then, since \(f \mathrel{R^{\mathrm{n}}_{\infty}} g\), it follows that \(f \ne \bot\) and \((f \cdot x) \mathrel{R^{\mathrm{n}}_{\infty}} (g \cdot y)\).

Thus, in all cases, congruence is satisfied.

Extensionality

Let \(f,g \in D^{\mathrm{n}}_{\infty}\) and suppose that, for all \(x,y \in D^{\mathrm{n}}_{\infty}\), \((f \cdot x) \mathrel{R^{\mathrm{n}}_{\infty}} (g \cdot y)\) whenever \(x \mathrel{R^{\mathrm{n}}_{\infty}} y\).

If \(f \ne \bot\), then \(\theta_{\mathrm{n}}(f) \ne \bot\) since \(\theta_{\mathrm{n}}\) is a pointed map and a one-to-one map. This means that \(\theta_{\mathrm{n}}(f) \in \mathrm{Cont}(D^{\mathrm{n}}_{\infty}, D^{\mathrm{n}}_{\infty})\); thus, for all \(x \in D^{\mathrm{n}}_{\infty}\), \(f \cdot x = \theta_{\mathrm{n}}(f)(x) \ne \bot\). Suppose that \(g = \bot\). Then \(g \cdot x = \bot\) for all \(x \in D^{\mathrm{n}}_{\infty}\). It follows by the Bottom Uniqueness lemma that \(g \cdot x \mathrel{R^{\mathrm{n}}_{\infty}} \bot\) and \(f \cdot x \not \mathrel{R^{\mathrm{n}}_{\infty}} \bot\) and \(\bot \mathrel{R^{\mathrm{n}}_{\infty}} \bot\), which contradicts the hypothesis above; thus, \(g \ne \bot\). The condition \((f \cdot x) \mathrel{R^{\mathrm{n}}_{\infty}} (g \cdot y)\) whenever \(x \mathrel{R^{\mathrm{n}}_{\infty}} y\) is satisfied by hypothesis. A symmetric argument shows that if \(g \ne \bot\) the \(f \ne \bot\) and the condition \((f \cdot x) \mathrel{R^{\mathrm{n}}_{\infty}} (g \cdot y)\) whenever \(x \mathrel{R^{\mathrm{n}}_{\infty}} y\) is satisfied by hypothesis.

Thus, extensionality is satisfied.

Variable Assigment

This is satisfied by the very definition of \(\llbracket x \rrbracket_{\rho}\).

Semantic Abstraction

By definition, \(\llbracket (\lambda x . M) \rrbracket_{\rho} \cdot d = \llbracket M \rrbracket_{\rho[x \mapsto d]}\), so, since \(\llbracket M \rrbracket_{\rho[x \mapsto d]} \in \mathrm{dom}(R_{\infty}^{\mathrm{n}})\), then \(\llbracket (\lambda x . M) \rrbracket_{\rho} \cdot d \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket M \rrbracket_{\rho[x \mapsto d]}\).

Applicative Consistency

Note that, if \(a,b \in \mathrm{dom}(R^{\mathrm{n}}_{\infty})\), then, by congruence, it follows that \((a \cdot b) \mathrel{R^{\mathrm{n}}_{\infty}} (a \cdot b)\).

By definition, \(\llbracket (MN) \rrbracket_{\rho} = \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho}\), so, since \(\llbracket M\rrbracket_{\rho} \in \mathrm{dom}(R_{\infty}^{\mathrm{n}})\) and \(\llbracket N \rrbracket_{\rho} \in \mathrm{dom}(R_{\infty}^{\mathrm{n}})\), it follows that \(\llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho} \in \mathrm{dom}(R_{\infty}^{\mathrm{n}})\) and thus \(\llbracket (MN) \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho}\).

Environmental Consistency

We proceed by structural induction on terms.

• Variables: there is only one free variable in a term \(x\) consisting of a single variable, namely \(x\) itself; if \(\rho(x) = \rho'(x)\) then \(\llbracket x \rrbracket_{\rho} = \llbracket x \rrbracket_{\rho'}\).
• Abstractions: Suppose that\(\rho(y) = \rho'(y)\) for all \(y \in \mathrm{Free}(\lambda x . M)\). Since \(\mathrm{Free}(M) = \mathrm{Free}(\lambda x . M) \cup \{x\}\), it follows that \(\rho[x \mapsto d](y) = \rho'[x \mapsto d](y)\) for all \(y \in \mathrm{Free}(M)\) and \(d \in \mathrm{dom}(R_{\infty}^{\mathrm{n}})\), and hence, by inductive hypothesis, \(\llbracket M \rrbracket_{\rho[x \mapsto d]} \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket M \rrbracket_{\rho'[x \mapsto d]}\). It follows that \((d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]})(d) \mathrel{R_{\infty}^{\mathrm{n}}} (d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]})(d)\) for all \(d \in \mathrm{dom}(R_{\infty}^{\mathrm{n}})\). This means that \(\theta_{\mathrm{n}}(\theta^{-1}_{\mathrm{n}}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}))(d) \mathrel{R_{\infty}^{\mathrm{n}}} \theta_{\mathrm{n}}(\theta^{-1}_{\mathrm{n}}(d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]}))(d)\) and hence \(\theta^{-1}_{\mathrm{n}}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}) \cdot d \mathrel{R_{\infty}^{\mathrm{n}}} \theta^{-1}_{\mathrm{n}}(d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]}) \cdot d\), which, by extensionality, implies that \(\theta^{-1}_{\mathrm{n}}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}) \mathrel{R_{\infty}^{\mathrm{n}}} \theta^{-1}_{\mathrm{n}}(d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]})\). Thus, \(\llbracket (\lambda x . M) \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket (\lambda x . M) \rrbracket_{\rho'}\).
• Applications: Suppose that\(\rho(y) = \rho'(y)\) for all \(y \in \mathrm{Free}(MN)\). Then, since \(\mathrm{Free}(MN) = \mathrm{Free}(M) \cup \mathrm{Free}(N)\), it follows, by inductive hypothesis, that \(\llbracket M \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket M \rrbracket_{\rho'}\) and \(\llbracket N \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket N \rrbracket_{\rho'}\). Then, by congruence, it follows that \(\llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho'}\) and hence \(\llbracket (MN) \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket (MN) \rrbracket_{\rho'}\).

Call-by-Value

The call-by-value model \(\mathcal{M}_{\mathrm{v}}\) is defined as follows:

• Semantic Domain: \(D_{\infty}^{\mathrm{v}}\);
• PER: \(R_{\infty}^{\mathrm{v}}\);
• Application: for all \(d_1, d_2 \in D_{\infty}^{\mathrm{v}}\), \[d_1 \cdot d_2 = \begin{cases}\bot & \text{if } \theta_{\mathrm{v}}(d_1) = \bot \text{ or } \theta_{\mathrm{v}}(d_1)(d_2) = \bot \\ \theta_{\mathrm{v}}(d_1)(d_2) & \text{otherwise} \end{cases}\];
• Denotation:
  • Variables: \(\llbracket x \rrbracket_{\rho} = \rho(x)\) for all variables \(x \in \mathcal{V}\) and environments \(\rho \in \mathrm{Env}(R_{\infty}^{\mathrm{v}})\);
  • Abstraction: \(\llbracket (\lambda x . M) \rrbracket_{\rho} = \theta^{-1}_{\mathrm{v}}\left(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\right)\) for all variables \(x \in \mathcal{V}\), terms \(M \in \Lambda\), and environments \(\rho \in \mathrm{Env}(R_{\infty}^{\mathrm{v}})\);
  • Application: \(\llbracket (MN) \rrbracket_{\rho} = \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho}\) for all terms \(M, N \in \Lambda\), and environments \(\rho \in \mathrm{Env}(R_{\infty}^{\mathrm{v}})\).

We verify the model axioms.

Lemma (Bottom Uniqueness). For all \(x \in D^{\mathrm{v}}_{\infty}\), \(x \mathrel{R^{\mathrm{v}}_{\infty}} \bot\) if and only if \(x = \bot\).

Proof. If \(x \mathrel{R^{\mathrm{v}}_{\infty}} \bot\), then if \(x \ne \bot\), it follows that \(\bot \ne \bot\), a contradiction. Thus \(x = \bot\). Conversely, \(\bot \mathrel{R^{\mathrm{v}}_{\infty}} \bot\) holds vacuously. \(\square\)

Continuity

We confirm that the denotation of abstractions \(\llbracket (\lambda x . M) \rrbracket_{\rho} = \theta_{\mathrm{v}}^{-1}\left(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\right)\) is well-defined, i.e., that the function \(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\) is indeed a continuous map. We proceed by structural induction on the body \(M\) of the abstraction.

• Variables \((M=y)\).
  • Case 1: \((y=x)\). Then \(d \mapsto \llbracket x \rrbracket_{\rho[x \mapsto d]}\) is simply the identity map \(d \mapsto d\), which is continuous.
  • Case 2: \((y \ne x)\). Then \(d \mapsto \llbracket y \rrbracket_{\rho[x \mapsto d]}\) is simply the constant map \(d \mapsto \rho(y)\), which is continuous.
• Abstractions \((M = (\lambda y . M'))\). By definition, \[d \mapsto \llbracket (\lambda y . M') \rrbracket_{\rho[x \mapsto d]} = d \mapsto \theta_{\mathrm{v}}^{-1}\left(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\right).\] By inductive hypothesis on the subterm \(M'\), the map \(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\) is continuous for every value of \(d\), and hence the expression \(\theta_{\mathrm{v}}^{-1}\left(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\right)\) is well-defined and the composite map \(d \mapsto \theta_{\mathrm{v}}^{-1}\left(d' \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d][y \mapsto d']}\right)\) is continuous since it is the composition of two continuous maps.
• Applications \(M = (M_1M_2)\). By definition, \begin{align*}d \mapsto \llbracket (M_1M_2) \rrbracket_{\rho[x \mapsto d]} &= d \mapsto \llbracket M_1 \rrbracket_{\rho[x \mapsto d]} \cdot \llbracket M_1 \rrbracket_{\rho[x \mapsto d]} \\&= d \mapsto \theta_{\mathrm{v}}\left(\llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\right)\left(\llbracket M_2 \rrbracket_{\rho[x \mapsto d]}\right).\end{align*} By inductive hypothesis on the sub-terms \(M_1\) and \(M_2\), the maps \(d \mapsto \llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\) and \(d \mapsto \llbracket M_2 \rrbracket_{\rho[x \mapsto d]}\) are continuous. By definition, the map \(\theta_{\mathrm{v}}\left(\llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\right)\) is continuous, and hence so is the composite map \(d \mapsto \theta_{\mathrm{v}}\left(\llbracket M_1 \rrbracket_{\rho[x \mapsto d]}\right)\left(\llbracket M_2 \rrbracket_{\rho[x \mapsto d]}\right)\).

Well-Definedness
We confirm that \(\llbracket M \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{v}}_{\infty})\) for all terms \(M \in \Lambda\). we proceed by structural induction on \(M\).

• Variables: \((M=x)\); \(\llbracket x \rrbracket_{\rho} = \rho(x) \in \mathrm{dom}(R^{\mathrm{v}}_{\infty})\) by construction;
• Abstractions: \((M = (\lambda x . M'))\). Suppose \(\llbracket (\lambda x . M') \rrbracket_{\rho} \ne \bot\). By definition, \(\llbracket (\lambda x . M') \rrbracket_{\rho} = \theta_{\mathrm{v}}^{-1}(d \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d]})\). Suppose \(e_1, e_2 \in D^{\mathrm{v}}_{\infty}\), \(e_1 \ne \bot\), \(e_2 \ne \bot\), and \(e_1 \mathrel{R^{\mathrm{v}}_{\infty}} e_2\). By definition, since \(\llbracket (\lambda x . M') \rrbracket_{\rho} \ne \bot\), \(e_1 \ne \bot\), and \(e_2 \ne \bot\), it follows that \(\llbracket (\lambda x . M') \rrbracket_{\rho} \cdot e_1 = \theta_{\mathrm{v}}(\theta_{\mathrm{v}}^{-1}(d \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d]}))(e_1) = \llbracket M' \rrbracket_{\rho[x \mapsto e_1]}\). Likewise, \(\llbracket (\lambda x . M') \rrbracket_{\rho} \cdot e_2 = \llbracket M' \rrbracket_{\rho[x \mapsto e_2]}\). By Environmental Consistency, since \(e_1 \mathrel{R^{\mathrm{v}}_{\infty}} e_2\), it follows that \(\llbracket M' \rrbracket_{\rho[x \mapsto e_1]} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket M' \rrbracket_{\rho[x \mapsto e_2]}\). Thus \(\llbracket (\lambda x . M') \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket (\lambda x . M') \rrbracket_{\rho}\) and so \(\llbracket (\lambda x . M') \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{v}}_{\infty})\).
• Applications: \((M = (NP))\). By inductive hypothesis, \(\llbracket N \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{v}}_{\infty})\) and \(\llbracket P \rrbracket_{\rho} \in \mathrm{dom}(R^{\mathrm{v}}_{\infty})\). By definition, \(\llbracket (NP) \rrbracket_{\rho} = \llbracket N \rrbracket_{\rho} \cdot \llbracket P \rrbracket_{\rho}\), and by Congruence, \(\llbracket (MN) \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket (MN) \rrbracket_{\rho}\).

Thus, the semantic denotation map is well-defined.

Congruence

Let \(f,g,x,y \in D^{\mathrm{v}}_{\infty}\) and suppose that \(f \mathrel{R^{\mathrm{v}}_{\infty}} g\) and \(x \mathrel{R^{\mathrm{v}}_{\infty}} y\).

• If \(f = \bot\) and \(g = \bot\), then it is vacuously the case that \(\bot \mathrel{R^{\mathrm{v}}_{\infty}} \bot\).
• if \(f \ne \bot\), then, since \(f \mathrel{R^{\mathrm{v}}_{\infty}} g\), it follows that \(g \ne \bot\).
  • If \(x \ne \bot\) and \(y \ne \bot\), then \((f \cdot x) \mathrel{R^{\mathrm{v}}_{\infty}} (g \cdot y\)\).
  • If \(x = \bot\), then, by the Bottom Uniqueness Lemma, \(y = \bot\), and \(f \cdot x = g \cdot y = \bot\) and \(\bot \mathrel{R^{\mathrm{v}}_{\infty}} \bot\).
  • If \(y = \bot\), then, by the Bottom Uniqueness Lemma, \(x = \bot\), and \(f \cdot x = g \cdot y = \bot\) and \(\bot \mathrel{R^{\mathrm{v}}_{\infty}} \bot\).

Thus, in all cases, congruence holds.

Extensionality

Let \(f,g \in D^{\mathrm{v}}_{\infty}\) and suppose that, for all \(x,y \in D^{\mathrm{v}}_{\infty}\), \((f \cdot x) \mathrel{R^{\mathrm{v}}_{\infty}} (g \cdot y)\) whenever \(x \mathrel{R^{\mathrm{v}}_{\infty}} y\).

If \(f \ne \bot\), then \(\theta_{\mathrm{v}}(f) \ne \bot\) since \(\theta_{\mathrm{v}}\) is a pointed map and a one-to-one map. This means that \(\theta_{\mathrm{v}}(f) \in \mathrm{Cont}(D^{\mathrm{v}}_{\infty}, (D^{\mathrm{v}}_{\infty})_{\bot})\); thus, for all \(x \in D^{\mathrm{v}}_{\infty}\), \(f \cdot x = \theta_{\mathrm{v}}(f)(x) \ne \bot\). Suppose that \(g = \bot\). Then \(g \cdot x = \bot\) for all \(x \in D^{\mathrm{v}}_{\infty}\). It follows by the Bottom Uniqueness lemma that \(g \cdot x \mathrel{R^{\mathrm{v}}_{\infty}} \bot\) and \(f \cdot x \not \mathrel{R^{\mathrm{v}}_{\infty}} \bot\) and \(\bot \mathrel{R^{\mathrm{v}}_{\infty}} \bot\), which contradicts the hypothesis above; thus, \(g \ne \bot\). If \(x \ne \bot\) \and \(y \ne \bot\), the condition \((f \cdot x) \mathrel{R^{\mathrm{v}}_{\infty}} (g \cdot y)\) whenever \(x \mathrel{R^{\mathrm{v}}_{\infty}} y\) is satisfied by hypothesis. If \(x = \bot\), then, by the Bottom Uniqueness Lemma, \(y = \bot\) and so \(f \cdot x = g \cdot y = \bot\) and \(\bot \mathrel{R^{\mathrm{v}}_{\infty}} \bot\). A symmetric argument shows that if \(g \ne \bot\) then \(f \ne \bot\) and the condition \((f \cdot x) \mathrel{R^{\mathrm{v}}_{\infty}} (g \cdot y)\) whenever \(x \mathrel{R^{\mathrm{v}}_{\infty}} y\) is satisfied.

Thus, extensionality is satisfied.

Variable Assigment

This is satisfied by the very definition of \(\llbracket x \rrbracket_{\rho}\).

Semantic Abstraction

By definition, \(\llbracket (\lambda x . M) \rrbracket_{\rho} \cdot d = \llbracket M \rrbracket_{\rho[x \mapsto d]}\), so, since \(\llbracket M \rrbracket_{\rho[x \mapsto d]} \in \mathrm{dom}(R_{\infty}^{\mathrm{n}})\), then \(\llbracket (\lambda x . M) \rrbracket_{\rho} \cdot d \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket M \rrbracket_{\rho[x \mapsto d]}\).

Applicative Consistency

Note that, if \(a,b \in \mathrm{dom}(R^{\mathrm{v}}_{\infty})\), then, by congruence, it follows that \((a \cdot b) \mathrel{R^{\mathrm{v}}_{\infty}} (a \cdot b)\).

By definition, \(\llbracket (MN) \rrbracket_{\rho} = \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho}\), so, since \(\llbracket M\rrbracket_{\rho} \in \mathrm{dom}(R_{\infty}^{\mathrm{v}})\) and \(\llbracket N \rrbracket_{\rho} \in \mathrm{dom}(R_{\infty}^{\mathrm{v}})\), it follows that \(\llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho} \in \mathrm{dom}(R_{\infty}^{\mathrm{v}})\) and thus \(\llbracket (MN) \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho}\).

Environmental Consistency

We proceed by structural induction on terms.

• Variables: there is only one free variable in a term \(x\) consisting of a single variable, namely \(x\) itself; if \(\rho(x) = \rho'(x)\) then \(\llbracket x \rrbracket_{\rho} = \llbracket x \rrbracket_{\rho'}\).
• Abstractions: Suppose that\(\rho(y) = \rho'(y)\) for all \(y \in \mathrm{Free}(\lambda x . M)\). Since \(\mathrm{Free}(M) = \mathrm{Free}(\lambda x . M) \cup \{x\}\), it follows that \(\rho[x \mapsto d](y) = \rho'[x \mapsto d](y)\) for all \(y \in \mathrm{Free}(M)\) and \(d \in \mathrm{dom}(R_{\infty}^{\mathrm{v}})\), and hence, by inductive hypothesis, \(\llbracket M \rrbracket_{\rho[x \mapsto d]} \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket M \rrbracket_{\rho'[x \mapsto d]}\). It follows that \((d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]})(d) \mathrel{R_{\infty}^{\mathrm{v}}} (d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]})(d)\) for all \(d \in \mathrm{dom}(R_{\infty}^{\mathrm{v}})\). This means that \(\theta_{\mathrm{v}}(\theta^{-1}_{\mathrm{v}}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}))(d) \mathrel{R_{\infty}^{\mathrm{v}}} \theta_{\mathrm{v}}(\theta^{-1}_{\mathrm{v}}(d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]}))(d)\) and hence \(\theta^{-1}_{\mathrm{v}}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}) \cdot d \mathrel{R_{\infty}^{\mathrm{v}}} \theta^{-1}_{\mathrm{v}}(d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]}) \cdot d\), which, by extensionality, implies that \(\theta^{-1}_{\mathrm{v}}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}) \mathrel{R_{\infty}^{\mathrm{v}}} \theta^{-1}_{\mathrm{v}}(d \mapsto \llbracket M \rrbracket_{\rho'[x \mapsto d]})\). Thus, \(\llbracket (\lambda x . M) \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket (\lambda x . M) \rrbracket_{\rho'}\).
• Applications: Suppose that\(\rho(y) = \rho'(y)\) for all \(y \in \mathrm{Free}(MN)\). Then, since \(\mathrm{Free}(MN) = \mathrm{Free}(M) \cup \mathrm{Free}(N)\), it follows, by inductive hypothesis, that \(\llbracket M \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket M \rrbracket_{\rho'}\) and \(\llbracket N \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket N \rrbracket_{\rho'}\). Then, by congruence, it follows that \(\llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket M \rrbracket_{\rho} \cdot \llbracket N \rrbracket_{\rho'}\) and hence \(\llbracket (MN) \rrbracket_{\rho} \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket (MN) \rrbracket_{\rho'}\).

Supporting Lemmas

We now prove a collection of lemmas intended to support the proofs of adequacy, soundness, and completeness.

Abstraction Lemma

This lemma indicates that abstractions are always non-bottom.

Call-by-Name

Lemma (Abstraction). For any lambda abstraction \((\lambda x . M)\) and environment \(\rho \in \mathrm{Env}(R^{\mathrm{n}}_{\infty})\),

\[\mathcal{M}_{\mathrm{n}} \models \llbracket (\lambda x . M) \rrbracket_{\rho} \downarrow.\]

Proof. By definition,

\[\llbracket (\lambda x . M) \rrbracket_{\rho} = \theta_{\mathrm{n}}^{-1}\left(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\right).\]

Since \(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\) is a continuous map, it is not the bottom element of \((\mathrm{Cont}(D^{\mathrm{n}}_{\infty}, D^{\mathrm{n}}_{\infty}))_{\bot}\) (by construction, since the bottom element is disjoint from all continuous maps by definition) and hence, since \(\theta_{\mathrm{n}}^{-1}\) is pointed and one-to-one, it follows that \(\theta_{\mathrm{n}}^{-1}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}) \ne \bot\). Thus, \(\llbracket (\lambda x . M) \rrbracket_{\rho} \ne \bot\) and \(\mathcal{M}_{\mathrm{n}} \models \llbracket (\lambda x . M) \rrbracket_{\rho} \downarrow\). \(\square\)

Call-by-Value

Lemma (Abstraction). For any lambda abstraction \((\lambda x . M)\) and environment \(\rho \in \mathrm{Env}(R^{\mathrm{v}}_{\infty})\),

\[\mathcal{M}_{\mathrm{v}} \models \llbracket (\lambda x . M) \rrbracket_{\rho} \downarrow.\]

Proof. By definition,

\[\llbracket (\lambda x . M) \rrbracket_{\rho} = \theta_{\mathrm{v}}^{-1}\left(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\right).\]

Since \(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}\) is a continuous map, it is not the bottom element of \((\mathrm{Cont}(D^{\mathrm{v}}_{\infty}, (D^{\mathrm{v}}_{\infty})_{\bot}))_{\bot}\) (by construction, since the bottom element is disjoint from all continuous maps by definition) and hence, since \(\theta_{\mathrm{v}}^{-1}\) is pointed and one-to-one, it follows that \(\theta_{\mathrm{v}}^{-1}(d \mapsto \llbracket M \rrbracket_{\rho[x \mapsto d]}) \ne \bot\). Thus, \(\llbracket (\lambda x . M) \rrbracket_{\rho} \ne \bot\) and \(\mathcal{M}_{\mathrm{v}} \models \llbracket (\lambda x . M) \rrbracket_{\rho} \downarrow\). \(\square\)

Substitution Lemma

This lemma indicates that syntactic and environmental substitution are compatible.

Call-by-Name

Lemma (Substitution). For any terms \(M, N \in \Lambda\), variable \(x \in \mathcal{V}\), and environment \(\rho \in \mathrm{Env}(R^{\mathrm{n}}_{\infty})\),

\[\llbracket M[N/x] \rrbracket_{\rho} =\llbracket M \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\]

Proof. We proceed by structural induction on the term \(M\).

• Variables \((M=y)\):
  • Case 1 \((y=x)\): \begin{align*}\llbracket y[N/x] \rrbracket_{\rho} &= \llbracket x[N/x] \rrbracket_{\rho} \\&= \llbracket N \rrbracket_{\rho} \\&= \rho\left[x \mapsto \llbracket N \rrbracket_{\rho}\right](x) \\&= \llbracket x \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]} \\&= \llbracket y \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}
  • Case 2 \((y \ne x)\): \begin{align*}\llbracket y[N/x] \rrbracket_{\rho} &= \llbracket y \rrbracket_{\rho} \\&= \llbracket y \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}
• Abstractions \((M = (\lambda y . M'))\): without loss of generality, we may assume that \(y \ne x\) and \(y \notin \mathrm{Free}(N)\). Thus, \((\lambda y . M')[N/x] = (\lambda y . M'[N/x])\). By definition, \[\llbracket (\lambda y . M'[N/x]) \rrbracket_{\rho} = \theta_{\mathrm{n}}^{-1}\left(d \mapsto \llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]}\right).\] Applying the inductive hypothesis on the sub-term \(M'\) at environment \(\rho[y \mapsto d]\) yields \[\llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]} = \llbracket M' \rrbracket_{\rho[y \mapsto d][x \mapsto \llbracket N \rrbracket_{\rho[y \mapsto d]}]}.\] Since \(y \notin \mathrm{Free}(N)\), it follows that \(\llbracket N \rrbracket_{\rho[y \mapsto d]} = \llbracket N \rrbracket_{\rho}\). Thus, \[\llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]} = \llbracket M' \rrbracket_{\rho[y \mapsto d][x \mapsto \llbracket N \rrbracket_{\rho}]}.\] Since \(y \ne x\), it follows that \[\rho[y \mapsto d][x \mapsto \llbracket N \rrbracket_{\rho}] = \rho[x \mapsto \llbracket N \rrbracket_{\rho}][y \mapsto d].\] It follows that \[\llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]} = \llbracket M' \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}][y \mapsto d]}.\] It then follows that \begin{align*}\llbracket (\lambda y . M'[N/x]) \rrbracket_{\rho} &= \theta_{\mathrm{n}}^{-1}\left(d \mapsto \llbracket M'[N/x] \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}][y \mapsto d]}\right) \\&= \llbracket (\lambda y . M') \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}
• Applications \((M = (M_1M_2))\): by definition, \((M_1M_2)[N/x] = (M_1[N/x]M_2[N/x])\). Applying the inductive hypothesis to the sub-terms \(M_1\) and \(M_2\) yields \begin{align*}\llbracket (M_1[N/x]M_2[N/x]) \rrbracket_{\rho} &= \llbracket M_1[N/x] \rrbracket_{\rho} \cdot \llbracket M_2[N/x] \rrbracket_{\rho} \\&= \llbracket M_1 \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]} \cdot \llbracket M_2 \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]} \\&= \llbracket (M_1M_2) \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}

\(\square\)

Call-by-Value

Lemma (Substitution). For any terms \(N, L \in \Lambda\), variable \(x \in \mathcal{V}\), and environment \(\rho \in \mathrm{Env}(R^{\mathrm{v}}_{\infty})\),

\[\llbracket N[L/x] \rrbracket_{\rho} =\llbracket N \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}.\]

Proof. We proceed by structural induction on the term \(M\).

• Variables \((M=y)\):
  • Case 1 \((y=x)\): \begin{align*}\llbracket y[N/x] \rrbracket_{\rho} &= \llbracket x[N/x] \rrbracket_{\rho} \\&= \llbracket N \rrbracket_{\rho} \\&= \rho\left[x \mapsto \llbracket N \rrbracket_{\rho}\right](x) \\&= \llbracket x \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]} \\&= \llbracket y \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}
  • Case 2 \((y \ne x)\): \begin{align*}\llbracket y[N/x] \rrbracket_{\rho} &= \llbracket y \rrbracket_{\rho} \\&= \llbracket y \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}
• Abstractions \((M = (\lambda y . M'))\): without loss of generality, we may assume that \(y \ne x\) and \(y \notin \mathrm{Free}(N)\). Thus, \((\lambda y . M')[N/x] = (\lambda y . M'[N/x])\). By definition, \[\llbracket (\lambda y . M'[N/x]) \rrbracket_{\rho} = \theta_{\mathrm{v}}^{-1}\left(d \mapsto \llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]}\right).\] Applying the inductive hypothesis on the sub-term \(M'\) at environment \(\rho[y \mapsto d]\) yields \[\llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]} = \llbracket M' \rrbracket_{\rho[y \mapsto d][x \mapsto \llbracket N \rrbracket_{\rho[y \mapsto d]}]}.\] Since \(y \notin \mathrm{Free}(N)\), it follows that \(\llbracket N \rrbracket_{\rho[y \mapsto d]} = \llbracket N \rrbracket_{\rho}\). Thus, \[\llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]} = \llbracket M' \rrbracket_{\rho[y \mapsto d][x \mapsto \llbracket N \rrbracket_{\rho}]}.\] Since \(y \ne x\), it follows that \[\rho[y \mapsto d][x \mapsto \llbracket N \rrbracket_{\rho}] = \rho[x \mapsto \llbracket N \rrbracket_{\rho}][y \mapsto d].\] It follows that \[\llbracket M'[N/x] \rrbracket_{\rho[y \mapsto d]} = \llbracket M' \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}][y \mapsto d]}.\] It then follows that \begin{align*}\llbracket (\lambda y . M'[N/x]) \rrbracket_{\rho} &= \theta_{\mathrm{v}}^{-1}\left(d \mapsto \llbracket M'[N/x] \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}][y \mapsto d]}\right) \\&= \llbracket (\lambda y . M') \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}
• Applications \((M = (M_1M_2))\): by definition, \((M_1M_2)[N/x] = (M_1[N/x]M_2[N/x])\). Applying the inductive hypothesis to the sub-terms \(M_1\) and \(M_2\) yields \begin{align*}\llbracket (M_1[N/x]M_2[N/x]) \rrbracket_{\rho} &= \llbracket M_1[N/x] \rrbracket_{\rho} \cdot \llbracket M_2[N/x] \rrbracket_{\rho} \\&= \llbracket M_1 \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]} \cdot \llbracket M_2 \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]} \\&= \llbracket (M_1M_2) \rrbracket_{\rho[x \mapsto \llbracket N \rrbracket_{\rho}]}.\end{align*}

\(\square\)

Big-Step Soundness Lemma

This lemma indicates the the operational semantics preserves denotations.

Call-by-Name

Lemma (Big-Step Soundness). For any closed terms \(M, V \in \Lambda(\emptyset)\), if \(M \Downarrow_{\mathrm{n}} V\), then \(\llbracket M \rrbracket_{\rho} = \llbracket V \rrbracket_{\rho}\) for all \(\rho \in \mathrm{Env}(R^{\mathrm{n}}_{\infty})\).

Proof. We proceed by structural induction on the derivation of \(M \Downarrow_{\mathrm{n}} V\). Recall the structural rules for the call-by-name evaluation strategy:

1. Val: \[\frac{v \in V(\emptyset)}{v \Downarrow_{\mathrm{n}} v}\]
2. App: \[\frac{e \in \Lambda, e_1, e_2 \in \Lambda(\emptyset), x \in \mathcal{V}, v \in V(\emptyset), e_1 \Downarrow_{\mathrm{n}} (\lambda x . e), e[e_2/x] \Downarrow_{\mathrm{n}} v}{(e_1e_2) \Downarrow_{\mathrm{n}} v}.\]

• Case 1: Val. \(M = (\lambda x . M') = V\), so it is trivially the case that \(\llbracket M \rrbracket_{\rho} = \llbracket V \rrbracket_{\rho}\).
• Case 2: App. \(M = (M_1 M_2)\) with the following premises:
  • \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\);
  • \(M_1'[M_2/x] \Downarrow_{\mathrm{n}} V\).

By induction hypothesis on each premise, the following hold:

• \(\llbracket M_1 \rrbracket_{\rho} = \llbracket (\lambda x . M_1') \rrbracket_{\rho}\);
• \(\llbracket M_1'[M_2/x] \rrbracket_{\rho} = \llbracket V \rrbracket_{\rho}\).

Observe the following:

\begin{align*}\llbracket (M_1M_2) \rrbracket_{\rho} &= \llbracket M_1 \rrbracket \cdot \llbracket M_2 \rrbracket_{\rho} \\&= \llbracket (\lambda x . M_1' \rrbracket_{\rho} \cdot \llbracket M_2 \rrbracket_{\rho} \\&= \theta_{\mathrm{n}}^{-1}\left(d \mapsto \llbracket M_1' \rrbracket_{\rho[x \mapsto d]}\right) \cdot \llbracket M_2 \rrbracket_{\rho} \\&= \theta_{\mathrm{n}}\left(\theta_{\mathrm{n}}^{-1}\left(d \mapsto \llbracket M_1' \rrbracket_{\rho[x \mapsto d]}\right)\right)\left(\llbracket M_2 \rrbracket_{\rho}\right) \\&= \left(d \mapsto \llbracket M_1' \rrbracket_{\rho[x \mapsto d]}\right)\left(\llbracket M_2 \rrbracket_{\rho}\right) \\&= \llbracket M_1' \rrbracket_{\rho\left[x \mapsto \llbracket M_2 \rrbracket_{\rho}\right]} \\&= \llbracket M_1'[M_2/x] \rrbracket_{\rho} & \text{(Substitution Lemma)} \\&= \llbracket V \rrbracket_{\rho}.\end{align*}

\(\square\)

Call-by-Value

Lemma (Big-Step Soundness). For any closed terms \(M, V \in \Lambda(\emptyset)\), if \(M \Downarrow_{\mathrm{v}} V\), then \(\llbracket M \rrbracket_{\rho} = \llbracket V \rrbracket_{\rho}\) for all \(\rho \in \mathrm{Env}(R^{\mathrm{v}}_{\infty})\).

Proof. We proceed by induction on the derivation of \(M \Downarrow_{\mathrm{v}} V\). Recall that the structural rules for the call-by-value evaluation strategy are as follows:

1. Val: \[\frac{v \in V(\emptyset)}{v \Downarrow_{\mathrm{v}} v};\]
2. App: \[\frac{e \in \Lambda, e_1, e_2 \in \Lambda(\emptyset), x \in \mathcal{V}, e_1 \Downarrow_{\mathrm{v}} (\lambda x . e), e_2 \Downarrow_{\mathrm{v}} v, e[v/x] \Downarrow_{\mathrm{v}} v'}{(e_1e_2) \Downarrow_{\mathrm{v}} v'}.\]

• Case 1: Val. \(M = (\lambda x . M') = V\), so it is trivially the case that \(\llbracket M \rrbracket_{\rho} = \llbracket V \rrbracket_{\rho}\).
• Case 2: App. \(M = (M_1 M_2)\) with the following premises:
  • \(M_1 \Downarrow_{\mathrm{v}} (\lambda x . M_1')\);
  • \(M_2 \Downarrow_{\mathrm{v}} V_2\);
  • \(M_1'[V_2/x] \Downarrow_{\mathrm{v}} V\).

By induction hypothesis on each premise, the following hold:

• \(\llbracket M_1 \rrbracket_{\rho} = \llbracket (\lambda x . M_1') \rrbracket_{\rho}\);
• \(\llbracket M_2 \rrbracket_{\rho} = \llbracket V_2 \rrbracket_{\rho}\);
• \(\llbracket M_1'[V_2/x] \rrbracket_{\rho} = \llbracket V \rrbracket_{\rho}\).

Observe the following:

\begin{align*}\llbracket (M_1M_2) \rrbracket_{\rho} &= \llbracket M_1 \rrbracket \cdot \llbracket M_2 \rrbracket_{\rho} \\&= \llbracket (\lambda x . M_1' \rrbracket_{\rho} \cdot \llbracket V_2 \rrbracket_{\rho} \\&= \theta_{\mathrm{v}}^{-1}\left(d \mapsto \llbracket M_1' \rrbracket_{\rho[x \mapsto d]}\right) \cdot \llbracket V_2 \rrbracket_{\rho} \\&= \theta_{\mathrm{v}}\left(\theta_{\mathrm{v}}^{-1}\left(d \mapsto \llbracket M_1' \rrbracket_{\rho[x \mapsto d]}\right)\right)\left(\llbracket V_2 \rrbracket_{\rho}\right) \\&= \left(d \mapsto \llbracket M_1' \rrbracket_{\rho[x \mapsto d]}\right)\left(\llbracket V_2 \rrbracket_{\rho}\right) \\&= \llbracket M_1' \rrbracket_{\rho\left[x \mapsto \llbracket V_2 \rrbracket_{\rho}\right]} \\&= \llbracket M_1'[V_2/x] \rrbracket_{\rho} & \text{(Substitution Lemma)} \\&= \llbracket V \rrbracket_{\rho}.\end{align*}

\(\square\)

Adequacy

In this section, we will establish adequacy.

Call-by-Name

We define a hybrid relation for the call-by-name evaluation strategy as follows.

Definition (Environmental Relatedness). We say that an environment \(\rho \in \mathrm{Env}(R^{\mathrm{n}}_{\infty})\) is related to a closing syntactic substitution \(\sigma : \Gamma \rightarrow \Lambda(\emptyset)\) at context \(\Gamma\), written \(\rho \mathrel{\mathcal{R}_{\infty}^{\mathrm{n}}[\Gamma] }\sigma\), if, for every variable \(x \in \Gamma\),

\[\rho(x) \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} \sigma(x).\]

Definition (Hybrid Relation). The call-by-name hybrid relation \(\mathcal{R}^{\mathrm{n}}_{\infty} \subseteq D^{\mathrm{n}}_{\infty} \times \Lambda(\emptyset)\) is defined as the greatest fixed point

\[\mathcal{R}^{\mathrm{n}}_{\infty} = \nu F\]

where

\[F(R) = \{(d, M) \in D^{\mathrm{n}}_{\infty} \times \Lambda(\emptyset) \mid d \ne \bot \Rightarrow \exists x \in \mathcal{V} \exists M' \in \Lambda (M \Downarrow (\lambda x . M') \land \forall e \in D^{\mathrm{n}}_{\infty} \forall N \in \Lambda(\emptyset) (e \mathrel{R} N \Rightarrow (d \cdot e) \mathrel{R} M'[N/x])).\}\]

Thus:

\[d \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M \Leftrightarrow d \ne \bot \Rightarrow \exists x \in \mathcal{V} \exists M' \in \Lambda (M \Downarrow (\lambda x . M') \land \forall e \in D^{\mathrm{n}}_{\infty} \forall N \in \Lambda(\emptyset) (e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} N \Rightarrow (d \cdot e) \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M'[N/x])).\]

Theorem (Fundamental). For any context \(\Gamma \subseteq \mathcal{V}\), term \(M \in \Lambda(\Gamma)\), environment \(\rho \in \mathrm{Env}(R^{\mathrm{n}}_{\infty})\), and closing substitution \(\sigma : \Gamma \rightarrow \Lambda(\emptyset)\), if \(\rho \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}}[\Gamma] \sigma\), then

\[\llbracket M \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M[\sigma].\]

Proof. We proceed by structural induction on the term \(M\).

• Variables \((M=x)\). By definition, \(\llbracket x \rrbracket_{\rho} = \rho(x)\) and \(x[\sigma] = \sigma(x)\), so, since \(\rho \mathrel{\mathcal{R}_{\infty}^{\mathrm{n}}[\Gamma] }\sigma\), it follows that \(\rho(x) \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} \sigma(x)\), and hence \(\llbracket x \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} x[\sigma]\).
• Abstractions \((M = (\lambda x . M'))\). By the Abstraction Lemma, \(\llbracket (\lambda x . M') \rrbracket_{\rho} \ne \bot\). By definition, \((\lambda x . M')[\sigma] = (\lambda x . M'[\sigma'])\), where \(\sigma' = \sigma \vert_{\Gamma \setminus \{x\}}\). Since the evaluation of closed lambda terms is idempotent, \((\lambda x . M')[\sigma] \Downarrow_{\mathrm{n}} (\lambda x . M'[\sigma'])\). Suppose \(e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} P\) for some \(e \in D^{\mathrm{n}}_{\infty}\) and closed term \(P\). Note that \(\llbracket (\lambda x . M') \rrbracket_{\rho} \cdot e = \theta_{\mathrm{n}}\left(\theta_{\mathrm{n}}^{-1}\left(d \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d]}\right)\right)(e) = \llbracket M' \rrbracket_{\rho[x \mapsto e]}\). Note that \(\rho[x \mapsto e] \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}[\Gamma \cup \{x\}]} \sigma'[P/x]\). By the induction hypothesis applied to sub-term \(M'\), \(\llbracket M' \rrbracket_{\rho[x \mapsto e]} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M'[\sigma'[P/x]]\). Since \(M'[\sigma'[P/x]] = (M'[\sigma'])[P/x]\), it follows that \(\llbracket (\lambda x . M') \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} (\lambda x . M')[\sigma]\).
• Applications \((M = (M_1 M_2))\). By the inductive hypothesis applied to sub-terms \(M_1\) and \(M_2\), \(\llbracket M_1 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_1[\sigma]\) and \(\llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_2[\sigma]\). Suppose \(\llbracket (M_1 M_2) \rrbracket_{\rho} \ne \bot\). Then \(\llbracket M_1 \rrbracket_{\rho} \ne \bot\) (since \(\llbracket (M_1 M_2) \rrbracket_{\rho} = \llbracket M_1 \rrbracket_{\rho} \cdot \llbracket M_2 \rrbracket_{\rho}\) and \(\bot \cdot \llbracket M_2 \rrbracket_{\rho} = \bot\) always). Since \(\llbracket M_1 \rrbracket_{\rho} \ne \bot\) and \(\llbracket M_1 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_1[\sigma]\), it follows that \(M_1[\sigma] \Downarrow_{\mathrm{n}} (\lambda x . M_1')\) and \(\llbracket M_1 \rrbracket_{\rho} \cdot e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_1'[P/x]\) whenever \(e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} P\). Since \(\llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_2[\sigma]\), choosing \(e = \llbracket M_2 \rrbracket_{\rho}\) and \(P = M_2[\sigma]\) yields \(\llbracket M_1 \rrbracket_{\rho} \cdot \llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_1'[M_2[\sigma]/x]\). Since \(\llbracket (M_1M_2) \rrbracket_{\rho} = \llbracket M_1 \rrbracket_{\rho} \cdot \llbracket M_2 \rrbracket_{\rho}\), it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_1'[M_2[\sigma]/x]\). Then, since \(\llbracket (M_1M_2) \rrbracket_{\rho} \ne \bot\), it follows that \(M_1'[M_2[\sigma]/x] \Downarrow_{\mathrm{n}} V\). Combined with the fact that \(M_1[\sigma] \Downarrow_{\mathrm{n}} (\lambda x . M_1')\), the operational rules of call-by-name indicate that \((M_1[\sigma]M_2[\sigma]) \Downarrow_{\mathrm{n}} V\). Let \(V = (\lambda y . V')\). Then, since \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M_1'[M_2[\sigma]/x]\), \(\llbracket (M_1M_2) \rrbracket_{\rho} \ne \bot\), and \(M_1'[M_2[\sigma]/x] \Downarrow_{\mathrm{n}} (\lambda y . V')\), it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \cdot e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} V'[P/x]\) for any \(e \in D^{\mathrm{n}}_{\infty}\) and closed term \(P\). Now, as demonstrated, if \(\llbracket (M_1 M_2) \rrbracket_{\rho} \ne \bot\), then \((M_1[\sigma]M_2[\sigma]) \Downarrow_{\mathrm{n}} (\lambda y . V')\), and, if \(e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} P\), then \(\llbracket (M_1M_2) \rrbracket_{\rho} \cdot e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} V'[P/x]\). Thus, it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} (M_1[\sigma]M_2[\sigma])\), and, since \((M_1M_2)[\sigma] = (M_1[\sigma]M_2[\sigma])\), it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} (M_1M_2)[\sigma]\).

\(\square\)

Theorem (Adequacy). For any closed term \(M \in \Lambda(\emptyset)\),

\[\mathcal{M}_{\mathrm{n}} \models M \downarrow \Leftrightarrow M \Downarrow_{\mathrm{n}}.\]

Proof. Suppose \(\mathcal{M} \models M \downarrow\). Then, by definition, \(\llbracket M \rrbracket \ne \bot\). By the Fundamental Lemma (applied with the empty context and empty environment), \(\llbracket M \rrbracket \mathrel{\mathcal{R}_{\infty}^{\mathrm{n}}} M\), which, together with \(\llbracket M \rrbracket \ne \bot\), implies that there exists a variable \(x \in \mathcal{V}\) and a term \(M' \in \Lambda(\emptyset)\) such that \(M \Downarrow_{\mathrm{n}} (\lambda x . M')\) and hence \(M \Downarrow_{\mathrm{n}}\).

Conversely, suppose \(M \Downarrow_{\mathrm{n}}\). Then there exists a variable \(x \in \mathcal{V}\) and a term \(M' \in \Lambda(\emptyset)\) such that \(M \Downarrow_{\mathrm{n}} (\lambda x . M')\). By the Abstraction Lemma, \(\mathcal{M}_{\mathrm{n}} \models (\lambda x . M') \downarrow\). By the Big-Step Soundness Lemma, \(\llbracket M \rrbracket \mathrel{R_{\infty}^{\mathrm{n}}} \llbracket (\lambda x . M') \rrbracket\) and thus, by the Bottom Uniqueness Lemma, \(\llbracket M \rrbracket \ne \bot\), and thus \(\mathcal{M}_{\mathrm{n}} \models M \downarrow\). \(\square\)

Call-by-Value

We define a hybrid relation for the call-by-value evaluation strategy as follows.

Definition (Environmental Relatedness). We say that an environment \(\rho \in \mathrm{Env}(R^{\mathrm{v}}_{\infty})\) is related to a closing syntactic substitution \(\sigma : \Gamma \rightarrow \Lambda(\emptyset)\) at context \(\Gamma\), written \(\rho \mathrel{\mathcal{R}_{\infty}^{\mathrm{v}}[\Gamma] }\sigma\), if, for every variable \(x \in \Gamma\),

\[\rho(x) \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} \sigma(x).\]

Definition (Hybrid Relation). The call-by-name hybrid relation \(\mathcal{R}^{\mathrm{v}}_{\infty} \subseteq D^{\mathrm{v}}_{\infty} \times \Lambda(\emptyset)\) is defined as the greatest fixed point

\[\mathcal{R}^{\mathrm{v}}_{\infty} = \nu F\]

where

\[F(R) = \{(d, M) \in D^{\mathrm{v}}_{\infty} \times \Lambda(\emptyset) \mid d \ne \bot \Rightarrow \exists x \in \mathcal{V} \exists M' \in \Lambda (M \Downarrow (\lambda x . M') \land \forall e \in D^{\mathrm{n}}_{\infty} \forall N \in V(\emptyset) (e \ne \bot \land e \mathrel{R} N \Rightarrow (d \cdot e) \mathrel{R} M'[N/x])).\}\]

Thus:

\[d \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M \Leftrightarrow d \ne \bot \Rightarrow \exists x \in \mathcal{V} \exists M' \in \Lambda (M \Downarrow (\lambda x . M') \land \forall e \in D^{\mathrm{n}}_{\infty} \forall N \in V(\emptyset) (e \ne \bot \land e \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} N \Rightarrow (d \cdot e) \mathrel{\mathcal{R}^{\mathrm{n}}_{\infty}} M'[N/x])).\]

Theorem (Fundamental). For any context \(\Gamma \subseteq \mathcal{V}\), term \(M \in \Lambda(\Gamma)\), environment \(\rho \in \mathrm{Env}(R^{\mathrm{n}}_{\infty})\), and closing substitution \(\sigma : \Gamma \rightarrow V(\emptyset)\), if \(\rho \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}}[\Gamma] \sigma\), then

\[\llbracket M \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M[\sigma].\]

Proof. We proceed by structural induction on the term \(M\).

• Variables \((M=x)\). By definition, \(\llbracket x \rrbracket_{\rho} = \rho(x)\) and \(x[\sigma] = \sigma(x)\), so, since \(\rho \mathrel{\mathcal{R}_{\infty}^{\mathrm{v}}[\Gamma] }\sigma\), it follows that \(\rho(x) \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} \sigma(x)\), and hence \(\llbracket x \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} x[\sigma]\).
• Abstractions \((M = (\lambda x . M'))\). By the Abstraction Lemma, \(\llbracket (\lambda x . M') \rrbracket_{\rho} \ne \bot\). By definition, \((\lambda x . M')[\sigma] = (\lambda x . M'[\sigma'])\), where \(\sigma' = \sigma \vert_{\Gamma \setminus \{x\}}\). Since the evaluation of closed lambda terms is idempotent, \((\lambda x . M')[\sigma] \Downarrow_{\mathrm{v}} (\lambda x . M'[\sigma'])\). Suppose \(e \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} P\) for some \(e \in D^{\mathrm{v}}_{\infty}\) such that \(e \ne \bot\) and closed value \(P \in V(\emptyset)\). Note that \(\llbracket (\lambda x . M') \rrbracket_{\rho} \cdot e = \theta_{\mathrm{v}}\left(\theta_{\mathrm{v}}^{-1}\left(d \mapsto \llbracket M' \rrbracket_{\rho[x \mapsto d]}\right)\right)(e) = \llbracket M' \rrbracket_{\rho[x \mapsto e]}\). Note that \(\rho[x \mapsto e] \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}[\Gamma \cup \{x\}]} \sigma'[P/x]\). By the induction hypothesis applied to sub-term \(M'\), \(\llbracket M' \rrbracket_{\rho[x \mapsto e]} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M'[\sigma'[P/x]]\). Since \(M'[\sigma'[P/x]] = (M'[\sigma'])[P/x]\), it follows that \(\llbracket (\lambda x . M') \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} (\lambda x . M')[\sigma]\).
• Applications \((M = (M_1 M_2))\). By the inductive hypothesis applied to sub-terms \(M_1\) and \(M_2\), \(\llbracket M_1 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_1[\sigma]\) and \(\llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_2[\sigma]\). Suppose \(\llbracket (M_1 M_2) \rrbracket_{\rho} \ne \bot\). Then \(\llbracket M_1 \rrbracket_{\rho} \ne \bot\) (since \(\llbracket (M_1 M_2) \rrbracket_{\rho} = \llbracket M_1 \rrbracket_{\rho} \cdot \llbracket M_2 \rrbracket_{\rho}\) and \(\bot \cdot \llbracket M_2 \rrbracket_{\rho} = \bot\) always) and also \(\llbracket M_2 \rrbracket_{\rho} \ne \bot\) (since \(\llbracket M_1 \rrbracket_{\rho} \cdot \bot = \bot\) always). Since \(\llbracket M_2 \rrbracket_{\rho} \ne \bot\) and \(\llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_2[\sigma]\), it follows that \(M_2[\sigma] \Downarrow_{\mathrm{v}} V_2\) for some closed lambda abstraction \(V_2\) and it also follows that \(\llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} V_2\) (since \(V_2 \Downarrow_{\mathrm{v}} V_2\) and \(V_2\) satisfies the requisite properties also). Since \(\llbracket M_1 \rrbracket_{\rho} \ne \bot\) and \(\llbracket M_1 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_1[\sigma]\), it follows that \(M_1[\sigma] \Downarrow_{\mathrm{v}} (\lambda x . M_1')\) and \(\llbracket M_1 \rrbracket_{\rho} \cdot e \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_1'[P/x]\) whenever \(e \ne \bot\) and \(e \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} P\). Since \(\llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} V_2\), choosing \(e = \llbracket M_2 \rrbracket_{\rho}\) and \(P = V_2\) yields \(\llbracket M_1 \rrbracket_{\rho} \cdot \llbracket M_2 \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_1'[V_2/x]\). Since \(\llbracket (M_1M_2) \rrbracket_{\rho} = \llbracket M_1 \rrbracket_{\rho} \cdot \llbracket M_2 \rrbracket_{\rho}\), it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_1'[V_2/x]\). Then, since \(\llbracket (M_1M_2) \rrbracket_{\rho} \ne \bot\), it follows that \(M_1'[V_2/x] \Downarrow_{\mathrm{v}} V_1\). Combined with the facts that \(M_1[\sigma] \Downarrow_{\mathrm{v}} (\lambda x . M_1')\) and \(M_2[\sigma] \Downarrow_{\mathrm{v}} V_2\), the operational rules of call-by-value indicate that \((M_1[\sigma]M_2[\sigma]) \Downarrow_{\mathrm{v}} V_1\). Let \(V_1 = (\lambda y . V_1')\). Then, since \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} M_1'[V_2/x]\), \(\llbracket (M_1M_2) \rrbracket_{\rho} \ne \bot\), and \(M_1'[V_2/x] \Downarrow_{\mathrm{v}} (\lambda y . V_1')\), it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \cdot e \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} V_1'[P/x]\) for any \(e \in D^{\mathrm{v}}_{\infty}\) and closed term \(P\). Now, as demonstrated, if \(\llbracket (M_1 M_2) \rrbracket_{\rho} \ne \bot\), then \((M_1[\sigma]M_2[\sigma]) \Downarrow_{\mathrm{v}} (\lambda y . V_1')\), and, if \(e \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} P\), then \(\llbracket (M_1M_2) \rrbracket_{\rho} \cdot e \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} V_1'[P/x]\). Thus, it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} (M_1[\sigma]M_2[\sigma])\), and, since \((M_1M_2)[\sigma] = (M_1[\sigma]M_2[\sigma])\), it follows that \(\llbracket (M_1M_2) \rrbracket_{\rho} \mathrel{\mathcal{R}^{\mathrm{v}}_{\infty}} (M_1M_2)[\sigma]\).

\(\square\)

Theorem (Adequacy). For any closed term \(M \in \Lambda(\emptyset)\),

\[\mathcal{M}_{\mathrm{v}} \models M \downarrow \Leftrightarrow M \Downarrow_{\mathrm{v}}.\]

Proof. Suppose \(\mathcal{M} \models M \downarrow\). Then, by definition, \(\llbracket M \rrbracket \ne \bot\). By the Fundamental Lemma (applied with the empty context and empty environment), \(\llbracket M \rrbracket \mathrel{\mathcal{R}_{\infty}^{\mathrm{v}}} M\), which, together with \(\llbracket M \rrbracket \ne \bot\), implies that there exists a variable \(x \in \mathcal{V}\) and a term \(M' \in \Lambda(\emptyset)\) such that \(M \Downarrow_{\mathrm{v}} (\lambda x . M')\) and hence \(M \Downarrow_{\mathrm{v}}\).

Conversely, suppose \(M \Downarrow_{\mathrm{v}}\). Then there exists a variable \(x \in \mathcal{V}\) and a term \(M' \in \Lambda(\emptyset)\) such that \(M \Downarrow_{\mathrm{v}} (\lambda x . M')\). By the Abstraction Lemma, \(\mathcal{M}_{\mathrm{v}} \models (\lambda x . M') \downarrow\). By the Big-Step Soundness Lemma, \(\llbracket M \rrbracket \mathrel{R_{\infty}^{\mathrm{v}}} \llbracket (\lambda x . M') \rrbracket\) and thus, by the Bottom Uniqueness Lemma, \(\llbracket M \rrbracket \ne \bot\), and thus \(\mathcal{M}_{\mathrm{v}} \models M \downarrow\). \(\square\)

Soundness

In this section, we will establish soundness.

Call-by-Name

In this section, we establish soundness for the call-by-name evaluation strategy.

Theorem (Soundness). For any closed terms \(M, N \in \Lambda(\emptyset)\),

\[\mathcal{M}_{\mathrm{n}} \models M = N \Rightarrow M \approx_{\mathrm{n}} N.\]

Proof. Define a binary relation \(\mathcal{S}\) as follows:

\[\mathcal{S} = \{(M, N) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \mid \llbracket M \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket N \rrbracket\}.\]

We will show that this relation is an applicative bisimulation.

1. Suppose \((P, Q) \in \mathcal{S}\) and \(P \Downarrow (\lambda x . P')\) for some variable \(x \in \mathcal{V}\) and term \(P' \in \Lambda(\emptyset)\).
   1. Since \((P, Q) \in \mathcal{S}\), by definition, \(\llbracket P \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q \rrbracket\).
   2. By the Big-Step Soundness Lemma \(\llbracket P \rrbracket = \llbracket (\lambda x . P') \rrbracket\).
   3. By the Abstraction Lemma, \(\llbracket (\lambda x . P') \rrbracket \ne \bot\).
   4. By the Bottom Uniqueness Lemma and transitivity, \(\llbracket Q \rrbracket \ne \bot\) and hence \(\mathcal{M}_{\mathrm{n}} \models Q \downarrow\).
   5. By the Adequacy Theorem, \(Q \Downarrow_{\mathrm{n}} (\lambda x . Q')\).
2. For any test argument \(L \in \Lambda(\emptyset)\):

• By definition of the denotation map, \(\llbracket L \rrbracket \mathrel{R_{\infty}} \llbracket L \rrbracket\).
• By the Congruence Axiom, \(\llbracket P \rrbracket \cdot \llbracket L \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q \rrbracket \cdot \llbracket L \rrbracket\).
• By the Big-Step Soundness Lemma, \(\llbracket P \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket (\lambda x . P') \rrbracket\).
• By the Big-Step Soundness Lemma, \(\llbracket Q \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket (\lambda x . Q') \rrbracket\).
• By the Semantic Abstraction Axiom, \(\llbracket (\lambda x . P') \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket P' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Semantic Abstraction Axiom, \(\llbracket (\lambda x . Q') \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Congruence Axiom, \(\llbracket P \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket P' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Congruence Axiom, \(\llbracket Q \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Substitution Lemma, \(\llbracket P'[L/x] \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket P' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\).
• By the Substitution Lemma, \(\llbracket Q'[L/x] \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\).
• By transitivity, \(\llbracket P'[L/x] \rrbracket_{\rho} \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q'[L/x] \rrbracket_{\rho}\).
• Since \(\rho\) was arbitrary, \(\llbracket P'[L/x] \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q'[L/x] \rrbracket\).
• It follows that \(P'[L/x] \mathrel{\mathcal{S}} Q'[L/x]\).

3. Thus, \(\mathcal{S}\) is an applicative bisimulation, which implies that \(\mathcal{S} \subseteq \approx\), and hence, if \(\mathcal{M}_{\mathrm{n}} \models M = N\), then \(\llbracket M \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket N \rrbracket\) and hence \(M \mathrel{\mathcal{S}} N\) and so \(M \approx_{\mathrm{n}} N\).

\(\square\)

Call-by-Value

In this section, we establish soundness for the call-by-value evaluation strategy.

Theorem (Soundness). For any closed terms \(M, N \in \Lambda(\emptyset)\),

\[\mathcal{M}_{\mathrm{v}} \models M = N \Rightarrow M \approx_{\mathrm{v}} N.\]

Proof. Define a binary relation \(\mathcal{S}\) as follows:

\[\mathcal{S} = \{(M, N) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \mid \llbracket M \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket N \rrbracket\}.\]

We will show that this relation is an applicative bisimulation.

1. Suppose \((P, Q) \in \mathcal{S}\) and \(P \Downarrow (\lambda x . P')\) for some variable \(x \in \mathcal{V}\) and term \(P' \in \Lambda(\emptyset)\).
   1. Since \((P, Q) \in \mathcal{S}\), by definition, \(\llbracket P \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q \rrbracket\).
   2. By the Big-Step Soundness Lemma \(\llbracket P \rrbracket = \llbracket (\lambda x . P') \rrbracket\).
   3. By the Abstraction Lemma, \(\llbracket (\lambda x . P') \rrbracket \ne \bot\).
   4. By the Bottom Uniqueness Lemma and transitivity, \(\llbracket Q \rrbracket \ne \bot\) and hence \(\mathcal{M}_{\mathrm{v}} \models Q \downarrow\).
   5. By the Adequacy Theorem, \(Q \Downarrow_{\mathrm{v}} (\lambda x . Q')\).
2. For any test argument \(L \in V(\emptyset)\):

• By definition of the denotation map, \(\llbracket L \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket L \rrbracket\).
• By the Congruence Axiom, \(\llbracket P \rrbracket \cdot \llbracket L \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q \rrbracket \cdot \llbracket L \rrbracket\).
• By the Big-Step Soundness Lemma, \(\llbracket P \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket (\lambda x . P') \rrbracket\).
• By the Big-Step Soundness Lemma, \(\llbracket Q \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket (\lambda x . Q') \rrbracket\).
• By the Semantic Abstraction Axiom, \(\llbracket (\lambda x . P') \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket P' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Semantic Abstraction Axiom, \(\llbracket (\lambda x . Q') \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Congruence Axiom, \(\llbracket P \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket P' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Congruence Axiom, \(\llbracket Q \rrbracket_{\rho} \cdot \llbracket L \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\) for any environment \(\rho\).
• By the Substitution Lemma, \(\llbracket P'[L/x] \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket P' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\).
• By the Substitution Lemma, \(\llbracket Q'[L/x] \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q' \rrbracket_{\rho[x \mapsto \llbracket L \rrbracket_{\rho}]}\).
• By transitivity, \(\llbracket P'[L/x] \rrbracket_{\rho} \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q'[L/x] \rrbracket_{\rho}\).
• Since \(\rho\) was arbitrary, \(\llbracket P'[L/x] \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q'[L/x] \rrbracket\).
• It follows that \(P'[L/x] \mathrel{\mathcal{S}} Q'[L/x]\).

3. Thus, \(\mathcal{S}\) is an applicative bisimulation, which implies that \(\mathcal{S} \subseteq \approx\), and hence, if \(\mathcal{M}_{\mathrm{v}} \models M = N\), then \(\llbracket M \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket N \rrbracket\) and hence \(M \mathrel{\mathcal{S}} N\) and so \(M \approx_{\mathrm{v}} N\).

\(\square\)

Completeness

Now we will demonstrate completeness.

Call-by-Name

In this section, we will establish completeness for the call-by-name evaluation strategy.

Theorem (Completeness). For any closed terms \(M, N \in \Lambda(\emptyset)\),

\[M \approx_{\mathrm{n}} N \Rightarrow \mathcal{M}_{\mathrm{n}} \models M = N.\]

Proof. We define a relation \(\mathcal{S} \subseteq D^{\mathrm{n}}_{\infty} \times D^{\mathrm{n}}_{\infty}\) as follows:

\[\mathcal{S} = \{(\llbracket M \rrbracket, \llbracket N \rrbracket) \in D^{\mathrm{n}}_{\infty} \times D^{\mathrm{n}}_{\infty} \mid \exists M', N' \in \Lambda(\emptyset) (\mathcal{M}_{\mathrm{n}} \models M = M' \land \mathcal{M}_{\mathrm{n}} \models N = N' \land M' \approx _{\mathrm{n}} N')\}.\]

We will show that this relation is a post-fixed point of the monotone map used to define \(R^{\mathrm{n}}_{\infty}\), i.e., that

\[d_1 \mathrel{\mathcal{S}} d_2\Rightarrow \begin{aligned}& d_1 \ne \bot \Rightarrow d_2 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{n}}_{\infty}(e_1 \mathrel{\mathcal{S}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)) \\ &\land \\ & d_2 \ne \bot \Rightarrow d_1 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{n}}_{\infty}(e_1 \mathrel{\mathcal{S}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)) \end{aligned}.\]

Proof. Suppose \(d_1 \mathrel{\mathcal{S}} d_2\). Then, by definition:

• \(d_1 = \llbracket M \rrbracket\) for some \(M \in \Lambda(\emptyset)\);
• \(d_2 = \llbracket N \rrbracket\) for some \(N \in \Lambda(\emptyset)\);
• \(\llbracket M \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket M' \rrbracket\) for some \(M' \in \Lambda(\emptyset)\);
• \(\llbracket N \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket N' \rrbracket\) for some \(N' \in \Lambda(\emptyset)\);
• \(M' \approx_{\mathrm{n}} N'\).

Suppose \(d_1 \ne \bot\). Then:

• since \(d_1 = \llbracket M \rrbracket\), \(\llbracket M \rrbracket \ne \bot\);
• by transitivity and the Bottom Uniqueness Lemma, it follows that \(\llbracket M' \rrbracket \ne \bot\);
• by the Adequacy Theorem, \(M' \Downarrow_{\mathrm{n}}\);
• since \(M' \approx_{\mathrm{n}} N'\), it follows that \(N' \Downarrow_{\mathrm{n}}\);
• by the Adequacy Theorem, \(\llbracket N' \rrbracket \ne \bot\);
• by transitivity and the Bottom Uniqueness Lemma, it follows that \(\llbracket N \rrbracket \ne \bot\);
• since \(d_2 = \llbracket N \rrbracket\), \(d_2 \ne \bot\), as required.

Suppose \(e_1 \mathrel{S} e_2\). Then, by definition:

• \(e_1 = \llbracket P \rrbracket\) for some \(P \in \Lambda(\emptyset)\);
• \(e_2 = \llbracket Q \rrbracket\) for some \(Q \in \Lambda(\emptyset)\);
• \(\llbracket P \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket P' \rrbracket\) for some \(M' \in \Lambda(\emptyset)\);
• \(\llbracket Q \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket Q' \rrbracket\) for some \(N' \in \Lambda(\emptyset)\);
• \(P' \approx_{\mathrm{n}} Q'\).

Then:

• \(d_1 \cdot e_1 = \llbracket M \rrbracket \cdot \llbracket P \rrbracket\);
• \(d_2 \cdot e_2 = \llbracket N \rrbracket \cdot \llbracket Q \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (MP) \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket M \rrbracket \cdot \llbracket P \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (NQ) \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket N \rrbracket \cdot \llbracket Q \rrbracket\);
• by the Congruence Axiom, \(\llbracket M \rrbracket \cdot \llbracket P \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket M' \rrbracket \cdot \llbracket P' \rrbracket\);
• by the Congruence Axiom, \(\llbracket N \rrbracket \cdot \llbracket Q \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket N' \rrbracket \cdot \llbracket Q' \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (M'P') \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket M' \rrbracket \cdot \llbracket P' \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (N'Q') \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket N' \rrbracket \cdot \llbracket Q' \rrbracket\);
• by transitivity, \(\llbracket M \rrbracket \cdot \llbracket P \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket (M'P') \rrbracket\);
• by transitivity, \(\llbracket N \rrbracket \cdot \llbracket Q \rrbracket \mathrel{R^{\mathrm{n}}_{\infty}} \llbracket (N'Q') \rrbracket\);
• by the congruence of applicative bisimilarity, since \(M' \approx_{\mathrm{n}} N'\) and \(P' \approx_{\mathrm{n}} Q'\), it follows that \((M'P') \approx_{\mathrm{n}} (N'Q')\).
• thus, it follows that \((d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)\).

A symmetric argument shows that, if \(d_2 \ne \bot\), then \(d_1 \ne \bot\), and, for all \(e_1, e_2 \in D^{\mathrm{n}}_{\infty}\), \((d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)\).

Thus, \(\mathcal{S}\) is a post-fixed point of the monotone map that characterizes \(R^{\mathrm{n}}_{\infty}\). Since \(R^{\mathrm{n}}_{\infty}\) is, by definition, the greatest post-fixed point, it follows that \(\mathcal{S} \subseteq R^{\mathrm{n}}_{\infty}\).

Thus, suppose that \(M \approx_{n} N\). Then, since \(\llbracket M \rrbracket, \llbracket N \rrbracket \in \mathrm{dom}(R^{\mathrm{n}}_{\infty})\) by construction, it follows that \(M \mathrel{S} N\) and hence \(M \mathrel{R^{\mathrm{n}}_{\infty}} N\) and so \(\mathcal{M}_{\mathrm{n}} \models M = N\). \(\square\)

Call-by-Value

In this section, we will establish completeness for the call-by-value evaluation strategy.

Theorem (Completeness). For any closed terms \(M, N \in \Lambda(\emptyset)\),

\[M \approx_{\mathrm{v}} N \Rightarrow \mathcal{M}_{\mathrm{v}} \models M = N.\]

Proof. We define a relation \(\mathcal{S} \subseteq D^{\mathrm{v}}_{\infty} \times D^{\mathrm{v}}_{\infty}\) as follows:

\[\mathcal{S} = \{(\llbracket M \rrbracket, \llbracket N \rrbracket) \in D^{\mathrm{v}}_{\infty} \times D^{\mathrm{v}}_{\infty} \mid \exists M', N' \in \Lambda(\emptyset) (\mathcal{M}_{\mathrm{v}} \models M = M' \land \mathcal{M}_{\mathrm{v}} \models N = N' \land M' \approx _{\mathrm{v}} N')\}.\]

We will show that this relation is a post-fixed point of the monotone map used to define \(R^{\mathrm{v}}_{\infty}\), i.e., that

\[d_1 \mathrel{\mathcal{S}} d_2\Rightarrow \begin{aligned}& d_1 \ne \bot \Rightarrow d_2 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{v}}_{\infty}(e_1 \ne \bot \land e_2 \ne \bot \land e_1 \mathrel{\mathcal{S}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)) \\ &\land \\ & d_2 \ne \bot \Rightarrow d_1 \ne \bot \land \forall e_1, e_2 \in D^{\mathrm{v}}_{\infty}(e_1 \ne \bot \land e_2 \ne \bot \land e_1 \mathrel{\mathcal{S}} e_2 \Rightarrow (d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)) \end{aligned}.\]

Proof. Suppose \(d_1 \mathrel{\mathcal{S}} d_2\). Then, by definition:

• \(d_1 = \llbracket M \rrbracket\) for some \(M \in \Lambda(\emptyset)\);
• \(d_2 = \llbracket N \rrbracket\) for some \(N \in \Lambda(\emptyset)\);
• \(\llbracket M \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket M' \rrbracket\) for some \(M' \in \Lambda(\emptyset)\);
• \(\llbracket N \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket N' \rrbracket\) for some \(N' \in \Lambda(\emptyset)\);
• \(M' \approx_{\mathrm{v}} N'\).

Suppose \(d_1 \ne \bot\). Then:

• since \(d_1 = \llbracket M \rrbracket\), \(\llbracket M \rrbracket \ne \bot\);
• by transitivity and the Bottom Uniqueness Lemma, it follows that \(\llbracket M' \rrbracket \ne \bot\);
• by the Adequacy Theorem, \(M' \Downarrow_{\mathrm{v}}\);
• since \(M' \approx_{\mathrm{n}} N'\), it follows that \(N' \Downarrow_{\mathrm{v}}\);
• by the Adequacy Theorem, \(\llbracket N' \rrbracket \ne \bot\);
• by transitivity and the Bottom Uniqueness Lemma, it follows that \(\llbracket N \rrbracket \ne \bot\);
• since \(d_2 = \llbracket N \rrbracket\), \(d_2 \ne \bot\), as required.

Suppose \(e_1 \mathrel{S} e_2\). Then, by definition:

• \(e_1 \ne \bot\);
• \(e_2 \ne \bot\);
• \(e_1 = \llbracket P \rrbracket\) for some \(P \in \Lambda(\emptyset)\);
• \(e_2 = \llbracket Q \rrbracket\) for some \(Q \in \Lambda(\emptyset)\);
• \(\llbracket P \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket P' \rrbracket\) for some \(M' \in \Lambda(\emptyset)\);
• \(\llbracket Q \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket Q' \rrbracket\) for some \(N' \in \Lambda(\emptyset)\);
• \(P' \approx_{\mathrm{v}} Q'\).

Then:

• \(d_1 \cdot e_1 = \llbracket M \rrbracket \cdot \llbracket P \rrbracket\);
• \(d_2 \cdot e_2 = \llbracket N \rrbracket \cdot \llbracket Q \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (MP) \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket M \rrbracket \cdot \llbracket P \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (NQ) \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket N \rrbracket \cdot \llbracket Q \rrbracket\);
• by the Congruence Axiom, \(\llbracket M \rrbracket \cdot \llbracket P \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket M' \rrbracket \cdot \llbracket P' \rrbracket\);
• by the Congruence Axiom, \(\llbracket N \rrbracket \cdot \llbracket Q \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket N' \rrbracket \cdot \llbracket Q' \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (M'P') \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket M' \rrbracket \cdot \llbracket P' \rrbracket\);
• by the Applicative Consistency Axiom, \(\llbracket (N'Q') \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket N' \rrbracket \cdot \llbracket Q' \rrbracket\);
• by transitivity, \(\llbracket M \rrbracket \cdot \llbracket P \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket (M'P') \rrbracket\);
• by transitivity, \(\llbracket N \rrbracket \cdot \llbracket Q \rrbracket \mathrel{R^{\mathrm{v}}_{\infty}} \llbracket (N'Q') \rrbracket\);
• by the congruence of applicative bisimilarity, since \(M' \approx_{\mathrm{v}} N'\) and \(P' \approx_{\mathrm{v}} Q'\), it follows that \((M'P') \approx_{\mathrm{v}} (N'Q')\).
• thus, it follows that \((d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)\).

A symmetric argument shows that, if \(d_2 \ne \bot\), then \(d_1 \ne \bot\), and, for all \(e_1, e_2 \in D^{\mathrm{v}}_{\infty}\), \((d_1 \cdot e_1) \mathrel{\mathcal{S}} (d_2 \cdot e_2)\).

Thus, \(\mathcal{S}\) is a post-fixed point of the monotone map that characterizes \(R^{\mathrm{v}}_{\infty}\). Since \(R^{\mathrm{v}}_{\infty}\) is, by definition, the greatest post-fixed point, it follows that \(\mathcal{S} \subseteq R^{\mathrm{v}}_{\infty}\).

Thus, suppose that \(M \approx_{v} N\). Then, since \(\llbracket M \rrbracket, \llbracket N \rrbracket \in \mathrm{dom}(R^{\mathrm{v}}_{\infty})\) by construction, it follows that \(M \mathrel{S} N\) and hence \(M \mathrel{R^{\mathrm{v}}_{\infty}} N\) and so \(\mathcal{M}_{\mathrm{v}} \models M = N\). \(\square\)