The Operational Semantics of the Lambda Calculus

In this post, I will explore the operational semantics of the lambda calculus for the call-by-name and call-by-value evaluation strategies.

The big-step operational semantics describes the full evaluation of terms to values. The small-step operational semantics describes individual, atomic reduction steps. This post establishes that each of these presentations is consistent, i.e., that the iteration of small-step reductions produces the same result as the big-step evaluation.

It is also possible to give a positive characterization of divergence, i.e., one that does not formulate divergence negatively as merely the lack of convergence. We also demonstrate that the positive and negative characterizations are consistent.

Big-Step Operational Semantics

First, we describe the big-step operational semantics.

Call-by-Name

The call-by-name evaluation strategy reduces the applicand but does not reduce the argument prior to substitution.

We define a relation \(\Downarrow_{\mathrm{n}} \subseteq \Lambda(\emptyset) \times V(\emptyset)\).

Schematically, this relation is expressed as follows:

\[\frac{V \in V(\emptyset)}{V \Downarrow_{\mathrm{n}} V},\]

\[\frac{M \Downarrow_{\mathrm{n}} (\lambda x . M'), M'[N/x] \Downarrow_{\mathrm{n}} V}{(MN) \Downarrow_{\mathrm{n}} V}.\]

Explicitly, we define a monotone operator \(F_{\mathrm{big,n}}\) on the powerset lattice \((\mathcal{P}(\Lambda(\emptyset) \times V(\emptyset)), \subseteq)\) as follows:

\begin{align*}F_{\mathrm{big,n}}(R) &= \{(V, V) \mid V \in V(\emptyset)\} \\&\cup \{((MN), V) \mid M,N \in \Lambda(\emptyset) \land V \in V(\emptyset) \land \exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\})(M \mathrel{R} M' \land M'[N/x] \mathrel{R} V)\}.\end{align*}

We then define the relation \(\Downarrow_{\mathrm{n}}\) as the least fixed point of this operator:

\[\Downarrow_{\mathrm{n}} ~ = ~ \mu F_{\mathrm{big,n}}.\]

Note that since this is an inductive definition and at most one rule is applicable for any closed term, this implies that evaluation is deterministic, i.e., that a term evaluates to at most one value (note that some terms might not have any value, i.e., they might diverge, so the relation is partial).

Call-by-Value

The call-by-value evaluation strategy reduces both the applicand and argument prior to substitution.

We define a relation \(\Downarrow_{\mathrm{v}} \subseteq \Lambda(\emptyset) \times V(\emptyset)\).

Schematically, this relation is expressed as follows:

\[\frac{V \in V(\emptyset)}{V \Downarrow_{\mathrm{n}} V},\]

\[\frac{M \Downarrow_{\mathrm{v}} (\lambda x . M'), N \Downarrow_{\mathrm{v}} V_1, M'[V_1/x] \Downarrow_{\mathrm{v}} V}{(MN) \Downarrow_{\mathrm{v}} V_2}.\]

Explicitly, we define a monotone operator \(F_{\mathrm{big,v}}\) on the powerset lattice \((\mathcal{P}(\Lambda(\emptyset) \times V(\emptyset)), \subseteq)\) as follows:

\begin{align*}F_{\mathrm{big,v}}(R) &= \{(V, V) \mid V \in V(\emptyset)\} \\&\cup \{((MN), V_2) \mid M \in \Lambda(\emptyset) \land N \in V(\emptyset) \land \exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\}) \exists V_1 \in V(\emptyset)(M \mathrel{R} M' \land N \mathrel{R} V_1 \land M'[V_1/x] \mathrel{R} V_2)\}.\end{align*}

We then define the relation \(\Downarrow_{\mathrm{v}}\) as the least fixed point of this operator:

\[\Downarrow_{\mathrm{v}} ~ = ~ \mu F_{\mathrm{big,v}}.\]

Note that since this is an inductive definition and at most one rule is applicable for any closed term, this implies that evaluation is deterministic, i.e., that a term evaluates to at most one value (note that some terms might not have any value, i.e., they might diverge, so the relation is partial).

Small-Step Operational Semantics

Next, we describe the small-step operational semantics.

Call-by-Name

We define a relation \(\rightarrow_{\mathrm{n}} \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\).

Schematically, this relation is expressed as follows:

\[\frac{}{((\lambda x . M)N) \rightarrow_{\mathrm{n}} M[N/x]},\]

\[\frac{M_1 \rightarrow_{\mathrm{n}} M_2}{(M_1N) \rightarrow_{\mathrm{n}} (M_2N)}.\]

Explicitly, we define a monotone operator \(F_{\mathrm{small,n}}\) on the powerset lattice \((\mathcal{P}(\Lambda(\emptyset) \times \Lambda(\emptyset)), \subseteq)\) as follows:

\begin{align*}F_{\mathrm{small,n}}(R) &= \{(((\lambda x . M)N), M[N/x]) \mid x \in \mathcal{V} \land M \in \Lambda(\{x\}) \land N \in \Lambda(\emptyset)\} \\&\cup \{((M_1N), (M_2N)) \mid M_1 \mathrel{R} M_2 \land N \in \Lambda(\emptyset)\}.\end{align*}

We then define the relation \(\rightarrow_{\mathrm{n}} \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) as the least fixed point of this operator:

\[\rightarrow_{\mathrm{n}} ~ = ~ \mu F_{\mathrm{small,n}}.\]

Call-by-Value

We define a relation \(\rightarrow_{\mathrm{v}} \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\).

Schematically, this relation is expressed as follows:

\[\frac{N \in V(\emptyset)}{((\lambda x . M)N) \rightarrow_{\mathrm{v}} M[N/x]},\]

\[\frac{M_1 \rightarrow_{\mathrm{v}} M_2}{(M_1N) \rightarrow_{\mathrm{n}} (M_2N)},\]

\[\frac{N_1 \rightarrow_{\mathrm{v}} N_2}{(MN_1) \rightarrow_{\mathrm{v}} (MN_2)}.\]

Explicitly, we define a monotone operator \(F_{\mathrm{small,v}}\) on the powerset lattice \((\mathcal{P}(\Lambda(\emptyset) \times \Lambda(\emptyset)), \subseteq)\) as follows:

\begin{align*}F_{\mathrm{small,v}}(R) &= \{(((\lambda x . M)N), M[N/x]) \mid x \in \mathcal{V} \land M \in \Lambda(\{x\}) \land N \in \Lambda(\emptyset)\} \\&\cup \{((M_1N), (M_2N)) \mid M_1 \mathrel{R} M_2 \land N \in \Lambda(\emptyset)\} \\&\cup \{((MN_1), (MN_2)) \mid M \in \Lambda(\emptyset) \land N_1 \mathrel{R} N_2\}.\end{align*}

We then define the relation \(\rightarrow_{\mathrm{v}} \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) as the least fixed point of this operator:

\[\rightarrow_{\mathrm{v}} ~ = ~ \mu F_{\mathrm{small,v}}.\]

The Iterated Small-Step Relation

We can also define the iterated small-step relation \(\rightarrow_{\mathrm{s}}^* \subseteq \Lambda(\emptyset) \times V(\emptyset)\) for \(\mathrm{s} \in \{\mathrm{n}, \mathrm{v}\}\).

Schematically, this relation is expressed as follows:

\[\frac{V \in V(\emptyset)}{V \rightarrow_{\mathrm{s}}^* V},\]

\[\frac{M \rightarrow_{\mathrm{s}} M', M' \rightarrow_{\mathrm{s}}^* V}{M \rightarrow_{\mathrm{s}}^* V}.\]

Explicitly, we define a monotone operator \(F_{\mathrm{iter,s}}\) on the powerset lattice \((\mathcal{P}(\Lambda(\emptyset) \times V(\emptyset)), \subseteq)\) as follows:

\begin{align*}F_{\mathrm{iter,s}}(R) &= \{(V, V) \mid V \in V(\emptyset)\} \\&\cup \{(M, V) \mid \exists M' \in \Lambda(\emptyset)(M \rightarrow_{\mathrm{s}} M' \land M' \mathrel{R} V)\}.\end{align*}

We then define the relation \(\rightarrow_{\mathrm{s}}^* \subseteq \Lambda(\emptyset) \times V(\emptyset)\) as the least fixed point of this operator:

\[\rightarrow_{\mathrm{s}}^* ~ = ~ \mu F_{\mathrm{iter,s}}.\]

Divergence

A closed lambda term \(M \in \Lambda(\emptyset)\) converges to value \(V \in V(\emptyset)\) if \(M \Downarrow_{\mathrm{s}} V\).

Likewise, a closed lambda term \(M \in \Lambda(\emptyset)\) diverges (written \(M \Uparrow_{\mathrm{s}}\)) if there does not exist any value \(V \in V(\emptyset)\) such that \(M \Downarrow_{\mathrm{s}} V\):

\[M \Uparrow_{\mathrm{s}} \Leftrightarrow \neg \exists V \in V(\emptyset) (M \Downarrow_{\mathrm{s}} V).\]

This is a negative characterization of divergence. It is also possible to give a positive characterization of divergence.

Call-by-Name

Schematically, divergence for the call-by-name evaluation strategy is expressed as follows:

\[\frac{M \Uparrow_{\mathrm{n}}}{(MN) \Uparrow_{\mathrm{n}}},\]

\[\frac{M \Downarrow_{\mathrm{n}} (\lambda x . M'), M'[N/x] \Uparrow_{\mathrm{n}}}{(MN) \Uparrow_{\mathrm{n}}}.\]

Although it is not necessary to define this predicate in terms of equivalence (applicative bisimilarity), it is technically expedient to do so.

Explicitly, we define a monotone operator \(F_{\mathrm{div,n}}\) on the powerset lattice \(\mathcal{P}(\Lambda(\emptyset))\) as follows:

\begin{align*}F_{\mathrm{div,n}}(P) &= \{(MN) \mid M \in P \land N \in \Lambda(\emptyset)\} \\&\cup \{(MN) \mid \exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\})(M \Downarrow_{\mathrm{n}} (\lambda x. M') \land M'[N/x] \in P)\}.\end{align*}

We then define the predicate \(\Uparrow_{\mathrm{n}}\) as the greatest fixed point of this operator:

\[\Uparrow_{\mathrm{n}} ~ = ~ \nu F_{\mathrm{div,n}}.\]

Call-by-Value

Schematically, divergence for the call-by-value evaluation strategy is expressed as follows:

\[\frac{M \Uparrow_{\mathrm{v}}}{(MN) \Uparrow_{\mathrm{n}}},\]

\[\frac{M \Downarrow_{\mathrm{n}} (\lambda x . M'), N \Downarrow_{\mathrm{v}} V, M'[V/x] \Uparrow_{\mathrm{v}}}{(MN) \Uparrow_{\mathrm{v}}},\]

\[\frac{M \Downarrow_{\mathrm{v}} (\lambda x . M'), N \Uparrow_{\mathrm{v}}}{(MN) \Uparrow_{\mathrm{v}}}.\]

Note that the convergence of \(M\) in the last rule is necessary so that there is at most one applicable rule for every term.

Although it is not necessary to define this predicate in terms of equivalence (applicative bisimilarity), it is technically expedient to do so.

Explicitly, we define a monotone operator \(F_{\mathrm{div,v}}\) on the powerset lattice \(\mathcal{P}(\Lambda(\emptyset))\) as follows:

\begin{align*}F_{\mathrm{div,v}}(P) &= \{(MN) \mid M \in P \land N \in \Lambda(\emptyset)\} \\&\cup \{(MN)\mid \exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\})(M \Downarrow_{\mathrm{v}} (\lambda x. M') \land N \Downarrow_{\mathrm{v}} V \land M'[V/x] \in P\} \\&\cup \{(MN) \mid (\exists x \in \mathcal{V} \exists M' \in \Lambda(\{x\})(M \Downarrow_{\mathrm{v}} (\lambda x . M'))) \land N \in P\}.\end{align*}

We then define the predicate \(\Uparrow_{\mathrm{v}}\) as the greatest fixed point of this operator:

\[\Uparrow_{\mathrm{v}} ~ = ~ \nu F_{\mathrm{div,v}}.\]

Compatibility

Next, we want to demonstrate that each of the defined notions are compatible.

Call-by-Name

First, we prove a few technical lemmas.

Lemma (Application). For all closed terms \(M, N \in \Lambda(\emptyset)\), every variable \(x \in \mathcal{V}\), every open body \(M' \in \Lambda(\{x\})\), and every closed value \(V \in V(\emptyset)\), if \(M \rightarrow_{\mathrm{n}}^* (\lambda x . M')\) and \(M'[N/x] \rightarrow_{\mathrm{n}}^* V\), then \((MN) \rightarrow_{\mathrm{n}}^* V\).

Proof. We proceed by structural induction on the derivation of \(M \rightarrow_{\mathrm{n}}^* (\lambda x . M')\).

Base Case. If the base rule applies, then \(M = (\lambda x . M')\). By definition, \(((\lambda x . M')N) \rightarrow_{\mathrm{n}} M'[N/x]\), and, since \(M'[N/x] \rightarrow_{\mathrm{n}}^* V\), it follows that \(((\lambda x . M')N) \rightarrow_{\mathrm{n}}^* V\).

Induction Step. If the iteration rule applies, then \(M \rightarrow_{\mathrm{n}} M_1\) and \(M_1 \rightarrow_{\mathrm{n}}^* (\lambda x . M')\) for some closed term \(M_1 \in \Lambda(\emptyset)\). Since \(M_1 \rightarrow_{\mathrm{n}}^* (\lambda x . M')\) and \(M'[N/x] \rightarrow_{\mathrm{n}}^* V\), by the inductive hypothesis, it follows that \((M_1N) \rightarrow_{\mathrm{n}}^* V\). Since \(M \rightarrow_{\mathrm{n}} M_1\), it follows that \((MN) \rightarrow_{\mathrm{n}} (M_1N)\). Since \((MN) \rightarrow_{\mathrm{n}} (M_1N)\) and \((M_1N) \rightarrow_{\mathrm{n}}^* V\), it follows that \((MN) \rightarrow_{\mathrm{n}}^* V\).

\(\square\)

Lemma (Simulation). If \(M \rightarrow_{\mathrm{n}} M_1\) and \(M_1 \Downarrow_{\mathrm{n}} V\), then \(M \Downarrow_{\mathrm{n}} V\).

Proof. We proceed by structural induction on the derivation \(M \rightarrow_{\mathrm{n}} M_1\).

Base Case. \(M = (\lambda x . M')\), \(M_1 = M'[N/x]\), and \(M \rightarrow_{\mathrm{n}} M'[N/x]\). By the structural rules for big-step evaluation, since \(M'[N/x] \Downarrow_{\mathrm{n}} V\) and \(M \Downarrow_{\mathrm{n}} (\lambda x . M')\), it follows that \(M \Downarrow_{\mathrm{n}} V\).

Induction Step. \(M = (M_2N)\), \(M_1 = (M_2'N)\), \(M_2 \rightarrow_{\mathrm{n}} M_2'\), \((M_2N) \rightarrow_{\mathrm{n}} (M_2'N)\), \((M_2'N) \Downarrow_{\mathrm{n}} V\). Since \((M_2'N) \Downarrow_{\mathrm{n}} V\), by definition, \(M_2' \Downarrow_{\mathrm{n}} (\lambda x . M_2'')\) and \(M_2''[N/x] \Downarrow_{\mathrm{n}} V\). By inductive hypothesis, since \(M_2 \rightarrow_{\mathrm{n}} M_2'\) and \(M_2' \Downarrow_{\mathrm{n}} (\lambda x . M_2'')\), it follows that \(M_2 \Downarrow_{\mathrm{n}} (\lambda x . M_2'')\). Since \(M_2 \Downarrow_{\mathrm{n}} (\lambda x . M_2'')\) and \(M_2''[N/x] \Downarrow_{\mathrm{n}} V\), it follows that \((M_2N) \Downarrow_{\mathrm{n}} V\).

\(\square\)

Theorem (Step Soundness). If \(M \Downarrow_{\mathrm{n}} V\) then \(M \rightarrow_{\mathrm{n}}^* V\).

Proof. We proceed by structural induction on the derivation of \(M \Downarrow_{\mathrm{n}} V\).

Base Case. If the base rule applies, then the derivation is \(V \Downarrow_{\mathrm{n}} V\) and \(M = V\). By the corresponding base rule for small-step reduction, \(V \rightarrow_{\mathrm{n}}^* V\).

Induction Step. If the application rule applies, then \(M = (M_1M_2)\) and the following hold:

• \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\),
• \(M_1[M_2/x] \Downarrow_{\mathrm{n}} V\).

By the inductive hypothesis, the following hold:

• \(M_1 \rightarrow_{\mathrm{n}}^* (\lambda x . M_1')\),
• \(M_1[M_2/x] \rightarrow_{\mathrm{n}}^* V\).

By the Application Lemma, it follows that \((M_1M_2) \rightarrow_{\mathrm{n}}^* V\).

\(\square\)

Theorem (Step Completeness). If \(M \rightarrow_{\mathrm{n}}^* V\), then \(M \Downarrow_{\mathrm{n}} V\).

Proof. We proceed by structural induction on the derivation of \(M \rightarrow_{\mathrm{n}}^* V\).

Base Case. If the base rule applies, then \(M = V\), and \(V \Downarrow_{\mathrm{n}} V\) hold by the corresponding base rule for big-step evaluation.

Induction Step. If the iteration rule applies, then \(M \rightarrow_{\mathrm{n}} M'\) and \(M' \rightarrow_{\mathrm{n}}^* V\) for some closed term \(M' \in \Lambda(\emptyset)\). By the inductive hypothesis, since \(M' \rightarrow_{\mathrm{n}}^* V\), it follows that \(M' \Downarrow_{\mathrm{n}} V\). By the Simulation Lemma, it follows that \(M \Downarrow_{\mathrm{n}} V\).

\(\square\)

Theorem (Divergence Soundness). If \(M \Uparrow_{\mathrm{n}}\) then there does not exist any closed value \(V \in V(\emptyset)\) such that \(M \Downarrow_{\mathrm{n}} V\).

Proof. We proceed to prove the contrapositive by structural induction on the derivation of \(M \Downarrow_{\mathrm{n}} V\):

\[\exists V \in V(\emptyset)(M \Downarrow_{\mathrm{n}} V) \Rightarrow M \not \Uparrow_{\mathrm{n}}.\]

Base Case. If the base rule applies, then the derivation \(M \Downarrow_{\mathrm{n}} V\) has the form \(V \Downarrow_{\mathrm{n}} V\) and \(M = V\). However, every structural rule for the divergence predicate contains an application and \(V\) is an abstraction, so \(V \not \Uparrow_{\mathrm{n}}\).

Induction Step. If the application rule applies, then the derivation \(M \Downarrow_{\mathrm{n}} V\) has the form \((M_1N) \Downarrow_{\mathrm{n}} V\) and \(M = (M_1N)\), where

• \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\),
• \(M_1'[N/x] \Downarrow_{\mathrm{n}} V\).

By the inductive hypothesis, the following holds:

• \(M_1 \not \Uparrow_{\mathrm{n}}\),
• \(M_1'[N/x] \not \Uparrow_{\mathrm{n}}\).

Suppose, by way of contradiction, that \((M_1N) \Uparrow_{\mathrm{n}}\). Then, according to the structural rules of the divergence predicate, there are two possibilities.

Case 1: \(M_1 \Uparrow_{\mathrm{n}}\). This directly contradicts \(M_1 \not \Uparrow_{\mathrm{n}}\).

Case 2: \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\) and \(M_1'[N/x] \Uparrow_{\mathrm{n}}\). However, this directly contradicts \(M_1'[N/x] \not \Uparrow_{\mathrm{n}}\).

Thus, in all cases, a contradiction arises, so if \(M \Downarrow_{\mathrm{n}} V\) then \(M \not \Uparrow_{\mathrm{n}}\).

\(\square\)

Theorem (Divergence Completeness). If there does not exist any closed lambda value \(V \in V(\emptyset)\) such that \(M \Downarrow_{\mathrm{n}} V\), then \(M \Uparrow_{\mathrm{n}}\).

Proof. We proceed by coinduction. We define the following candidate set:

\[P = \{M \in \Lambda(\emptyset) \mid \neg \exists V \in V(\emptyset) (M \Downarrow_{\mathrm{n}} V)\}.\]

Our goal is to show that \(P\) is a post-fixed point of the operator \(F_{\mathrm{div,n}}\), i.e., that \(P \subseteq F_{\mathrm{div,n}}(P)\), which then implies, since \(\Uparrow_{\mathrm{n}} = \nu F_{\mathrm{div,n}}\), that \(P \subseteq \Uparrow_{\mathrm{n}}\).

Suppose \(M \in P\). Then \(M \in \Lambda(\emptyset)\) and there does not exist any closed lambda value \(V \in V(\emptyset)\) such that \(M \Downarrow_{\mathrm{n}} V\). We consider the syntactic possibilities for the closed term \(M\).

It is not possible that \(M = (\lambda x . M')\), since otherwise \(M \Downarrow_{\mathrm{n}} (\lambda x . M')\). Therefore, the only possibility is that \(M = (M_1N)\).

Suppose that \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\) and there exists some \(V\) such that \(M_1'[N/x] \Downarrow_{\mathrm{n}} V\). Then \(M = (M_1N) \Downarrow_{\mathrm{n}} V\), a contradiction. Thus, there are two possibilities:

Case 1: \(\neg \exists V' (M_1 \Downarrow_{\mathrm{n}} V')\). In this case, \((M_1N) \in F_{\mathrm{div,n}}(P)\).

Case 2: \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\) and \(\neg \exists V (M_1'[N/x] \Downarrow_{\mathrm{n}} V)\). In this case, \((M_1N) \in F_{\mathrm{div,n}}(P)\).

In all cases, if \(M \in P\) then \(M \in F_{\mathrm{div,n}}(P)\), so \(P \subseteq F_{\mathrm{div,n}}(P)\).

\(\square\)

Call-by-Value

First, we prove a few technical lemmas.

Lemma (Congruence). For all closed values \(V_0, V_1, V_2 \in V(\emptyset)\) and every closed term \(N \in \Lambda(\emptyset)\), if \((V_0V_1) \rightarrow_{\mathrm{v}}^* V_2\) and \(N \rightarrow_{\mathrm{v}}^* V_1\), then \((V_0N) \rightarrow_{\mathrm{v}}^* V_2\).

Proof. We proceed by structural induction on the derivation \(N \rightarrow_{\mathrm{v}}^* V_1\).

Base Case. If the base rule applies, then \(N = V_1\) and we already have by assumption that \((V_0V_1) \rightarrow_{\mathrm{v}}^* V_2\).

Induction Step. If the iteration rule applies, then \(N \rightarrow_{\mathrm{v}} N'\) and \(N' \rightarrow_{\mathrm{v}}^* V_1\) for some closed term \(N' \in \Lambda(\emptyset)\). Since \(N \rightarrow_{\mathrm{v}} N'\), it follows that \((V_0N) \rightarrow_{\mathrm{v}} (V_0N')\). By inductive hypothesis, since \((V_0V_1) \rightarrow_{\mathrm{v}}^* V_2\) and \(N' \rightarrow_{\mathrm{v}}^* V_1\), it follows that \((V_0N') \rightarrow_{\mathrm{v}}^* V_2\). Since \((V_0N) \rightarrow_{\mathrm{v}} (V_0N')\) and \((V_0N') \rightarrow_{\mathrm{v}}^* V_2\), it follows that \((V_0N) \rightarrow_{\mathrm{v}}^* V_2\).

\(\square\)

Lemma (Application). For all closed terms \(M, N \in \Lambda(\emptyset)\), every variable \(x \in \mathcal{V}\), every open body \(M' \in \Lambda(\{x\})\), and all closed values \(V_1, V_2 \in V(\emptyset)\), if \(M \rightarrow_{\mathrm{v}}^* (\lambda x . M')\), \(N \rightarrow_{\mathrm{v}}^* V_1\) and \(M'[V_1/x] \rightarrow_{\mathrm{v}}^* V_2\), then \((MN) \rightarrow_{\mathrm{v}}^* V_2\).

Proof. We proceed by structural induction on the derivation of \(M \rightarrow_{\mathrm{v}}^* (\lambda x . M')\).

Base Case. If the base rule applies, then \(M = (\lambda x . M')\). By definition, \(((\lambda x . M')V_1) \rightarrow_{\mathrm{v}} M'[V_1/x]\), and, since \(M'[V_1/x] \rightarrow_{\mathrm{v}}^* V\), it follows that \(((\lambda x . M')V_1) \rightarrow_{\mathrm{v}}^* V_2\). By the Congruence Lemma, since \(N \rightarrow_{\mathrm{v}}^* V_1\), it follows that \(((\lambda x . M')N) \rightarrow_{\mathrm{v}}^* V_2\).

Induction Step. If the iteration rule applies, then \(M \rightarrow_{\mathrm{v}} M_1\) and \(M_1 \rightarrow_{\mathrm{v}}^* (\lambda x . M')\) for some closed term \(M_1 \in \Lambda(\emptyset)\). Since \(M_1 \rightarrow_{\mathrm{v}}^* (\lambda x . M')\), \(N \rightarrow_{\mathrm{v}}^* V_1\), and \(M'[V_1/x] \rightarrow_{\mathrm{v}}^* V_2\), by the inductive hypothesis, it follows that \((M_1N) \rightarrow_{\mathrm{v}}^* V_2\). Since \(M \rightarrow_{\mathrm{v}} M_1\), it follows that \((MN) \rightarrow_{\mathrm{v}} (M_1N)\). Since \((MN) \rightarrow_{\mathrm{v}} (M_1N)\) and \((M_1N) \rightarrow_{\mathrm{v}}^* V_2\), it follows that \((MN) \rightarrow_{\mathrm{v}}^* V_2\).

\(\square\)

Lemma (Simulation). If \(M \rightarrow_{\mathrm{v}} M_1\) and \(M_1 \Downarrow_{\mathrm{v}} V\), then \(M \Downarrow_{\mathrm{v}} V\).

Proof. We proceed by structural induction on the derivation of \(M \rightarrow_{\mathrm{v}} M_1\).

Base Case. \(M = (\lambda x . M')\), \(M_1 = M'[N/x]\), \(N \in V(\emptyset)\), and \(M \rightarrow_{\mathrm{v}} M'[N/x]\). By the structural rules for big-step evaluation, since \(M'[N/x] \Downarrow_{\mathrm{v}} V\), \(N \Downarrow_{\mathrm{v}} N\), and \(M \Downarrow_{\mathrm{v}} (\lambda x . M')\), it follows that \(M \Downarrow_{\mathrm{v}} V\).

Induction Step 1. \(M = (M_2N)\), \(M_1 = (M_2'N)\), \(M_2 \rightarrow_{\mathrm{v}} M_2'\), \((M_2N) \rightarrow_{\mathrm{v}} (M_2'N)\), \((M_2'N) \Downarrow_{\mathrm{v}} V\). Since \((M_2'N) \Downarrow_{\mathrm{v}} V\), by definition, \(M_2' \Downarrow_{\mathrm{v}} (\lambda x . M_2'')\), \(N \Downarrow_{\mathrm{v}} V_1\), and \(M_2''[V_1/x] \Downarrow_{\mathrm{v}} V\). By inductive hypothesis, since \(M_2 \rightarrow_{\mathrm{v}} M_2'\) and \(M_2' \Downarrow_{\mathrm{v}} (\lambda x . M_2'')\), it follows that \(M_2 \Downarrow_{\mathrm{v}} (\lambda x . M_2'')\). Since \(M_2 \Downarrow_{\mathrm{v}} (\lambda x . M_2'')\), \(N \Downarrow_{\mathrm{v}} V_1\), and \(M_2''[V_1/x] \Downarrow_{\mathrm{v}} V\), it follows that \((M_2N) \Downarrow_{\mathrm{n}} V\).

Induction Step 2. \(M = (M_2N_1)\), \(M_1 = (M_2N_1')\), \(N_1 \rightarrow_{\mathrm{v}} N_1'\), \((M_2N_1') \Downarrow_{\mathrm{v}} V\). Since \((M_2N_1') \Downarrow_{\mathrm{v}} V\), it follows that \(M_2 \Downarrow_{\mathrm{v}} (\lambda x . M_2')\), \(N_1' \Downarrow_{\mathrm{v}} V_1\), and \(M_2'[V_1/x] \Downarrow_{\mathrm{v}} V\). By the inductive hypothesis, since \(N_1 \rightarrow_{\mathrm{n}} N_1'\) and \(N_1' \Downarrow_{\mathrm{v}} V_1\), it follows that \(N_1 \Downarrow_{\mathrm{v}} V_1\). Since \(M_2 \Downarrow_{\mathrm{v}} (\lambda x . M_2')\), \(N_1 \Downarrow_{\mathrm{v}} V_1\), and \(M_2'[V_1/x] \Downarrow_{\mathrm{v}} V\), it follows that \((M_2N_1) \Downarrow_{\mathrm{v}} V\).

\(\square\)

Theorem (Step Soundness). If \(M \Downarrow_{\mathrm{v}} V\) then \(M \rightarrow_{\mathrm{v}}^* V\).

Proof. We proceed by structural induction on the derivation of \(M \Downarrow_{\mathrm{v}} V\).

Base Case. If the base rule applies, then the derivation is \(V \Downarrow_{\mathrm{v}} V\) and \(M = V\). By the corresponding base rule for small-step reduction, \(V \rightarrow_{\mathrm{v}}^* V\).

Induction Step. If the application rule applies, then \(M = (M_1M_2)\) the derivation is \((M_1M_2) \Downarrow_{\mathrm{v}} V\) and the following hold:

• \(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 the inductive hypothesis, the following hold:

• \(M_1 \rightarrow_{\mathrm{v}}^* (\lambda x . M_1')\),
• \(M_2 \rightarrow_{\mathrm{v}}^* V_2\),
• \(M_1[V_2/x] \rightarrow_{\mathrm{v}}^* V\).

By the Application Lemma, it follows that \((M_1M_2) \rightarrow_{\mathrm{v}}^* V\).

\(\square\)

Theorem (Step Completeness). If \(M \rightarrow_{\mathrm{v}}^* V\), then \(M \Downarrow_{\mathrm{v}} V\).

Proof. We proceed by structural induction on the derivation of \(M \rightarrow_{\mathrm{v}}^* V\).

Base Case. If the base rule applies, then \(M = V\), and \(V \Downarrow_{\mathrm{v}} V\) hold by the corresponding base rule for big-step evaluation.

Induction Step. If the iteration rule applies, then \(M \rightarrow_{\mathrm{v}} M'\) and \(M' \rightarrow_{\mathrm{v}}^* V\) for some closed term \(M' \in \Lambda(\emptyset)\). By the inductive hypothesis, since \(M' \rightarrow_{\mathrm{v}}^* V\), it follows that \(M' \Downarrow_{\mathrm{v}} V\). By the Simulation Lemma, it follows that \(M \Downarrow_{\mathrm{v}} V\).

\(\square\)

Theorem (Divergence Soundness). If \(M \Uparrow_{\mathrm{v}}\) then there does not exist any closed value \(V \in V(\emptyset)\) such that \(M \Downarrow_{\mathrm{v}} V\).

Proof. We proceed to prove the contrapositive by structural induction on the derivation of \(M \Downarrow_{\mathrm{v}} V\):

\[\exists V \in V(\emptyset)(M \Downarrow_{\mathrm{v}} V) \Rightarrow M \not \Uparrow_{\mathrm{v}}.\]

Base Case. If the base rule applies, then the derivation \(M \Downarrow_{\mathrm{v}} V\) has the form \(V \Downarrow_{\mathrm{v}} V\) and \(M = V\). However, every structural rule for the divergence predicate contains an application and \(V\) is an abstraction, so \(V \not \Uparrow_{\mathrm{v}}\).

Induction Step. If the application rule applies, then the derivation \(M \Downarrow_{\mathrm{v}} V\) has the form \((M_1N) \Downarrow_{\mathrm{v}} V\) and \(M = (M_1N)\), where

• \(M_1 \Downarrow_{\mathrm{v}} (\lambda x . M_1')\),
• \(N \Downarrow_{\mathrm{v}} V'\)
• \(M_1'[V'/x] \Downarrow_{\mathrm{v}} V\).

By the inductive hypothesis, the following holds:

• \(M_1 \not \Uparrow_{\mathrm{v}}\),
• \(N \not \Uparrow_{\mathrm{v}}\),
• \(M_1'[V'/x] \not \Uparrow_{\mathrm{v}}\).

Suppose, by way of contradiction, that \((M_1N) \Uparrow_{\mathrm{v}}\). Then, according to the structural rules of the divergence predicate, there are three possibilities.

Case 1: \(M_1 \Uparrow_{\mathrm{v}}\). This directly contradicts \(M_1 \not \Uparrow_{\mathrm{v}}\).

Case 2: \(N \Uparrow_{\mathrm{v}}\). This directly contradicts \(N \not \Uparrow_{\mathrm{v}}\).

Case 2: \(M_1 \Downarrow_{\mathrm{v}} (\lambda x . M_1')\) and \(N \Downarrow_{\mathrm{v}} V'\) and \(M_1'[V'/x] \Uparrow_{\mathrm{v}}\). However, this directly contradicts \(M_1'[V'/x] \not \Uparrow_{\mathrm{v}}\).

Thus, in all cases, a contradiction arises, so if \(M \Downarrow_{\mathrm{v}} V\) then \(M \not \Uparrow_{\mathrm{v}}\).

\(\square\)

Theorem (Divergence Completeness). If there does not exist any closed lambda value \(V \in V(\emptyset)\) such that \(M \Downarrow_{\mathrm{v}} V\), then \(M \Uparrow_{\mathrm{v}}\).

Proof. We proceed by coinduction. We define the following candidate set:

\[P = \{M \in \Lambda(\emptyset) \mid \neg \exists V \in V(\emptyset) (M \Downarrow_{\mathrm{v}} V)\}.\]

Our goal is to show that \(P\) is a post-fixed point of the operator \(F_{\mathrm{div,v}}\), i.e., that \(P \subseteq F_{\mathrm{div,v}}(P)\), which then implies, since \(\Uparrow_{\mathrm{v}} = \nu F_{\mathrm{div,v}}\), that \(P \subseteq \Uparrow_{\mathrm{v}}\).

Suppose \(M \in P\). Then \(M \in \Lambda(\emptyset)\) and there does not exist any closed lambda value \(V \in V(\emptyset)\) such that \(M \Downarrow_{\mathrm{v}} V\). We consider the syntactic possibilities for the closed term \(M\).

It is not possible that \(M = (\lambda x . M')\), since otherwise \(M \Downarrow_{\mathrm{n}} (\lambda x . M')\). Therefore, the only possibility is that \(M = (M_1N)\).

Suppose that \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\), there exists some \(V_1\) such that \(N \Downarrow_{\mathrm{v}} V_1\), and there exists some \(V\) such that \(M_1'[V_1/x] \Downarrow_{\mathrm{v}} V\). Then \(M = (M_1N) \Downarrow_{\mathrm{v}} V\), a contradiction. Thus, there are three possibilities:

Case 1: \(\neg \exists V' (M_1 \Downarrow_{\mathrm{v}} V')\). In this case, \((M_1N) \in F_{\mathrm{div,v}}(P)\).

Case 2: \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\) and \(\neg \exists V_1 (N \Downarrow_{\mathrm{v}} V_1)\). In this case, \((M_1N) \in F_{\mathrm{div,v}}(P)\).

Case 3: \(M_1 \Downarrow_{\mathrm{n}} (\lambda x . M_1')\) and \(\exists V_1 (N \Downarrow_{\mathrm{v}} V_1)\) and \(\neg \exists V (M_1'[V_1/x] \Downarrow_{\mathrm{v}} V)\). In this case, \((M_1N) \in F_{\mathrm{div,v}}(P)\).

In all cases, if \(M \in P\) then \(M \in F_{\mathrm{div,v}}(P)\), so \(P \subseteq F_{\mathrm{div,v}}(P)\).

\(\square\)