Howe's Method

In this post, I will discuss Howe's method (due to computer scientist Douglas J. Howe), an important technique for establishing that certain notions of equivalence in higher-order languages such as the lambda calculus are congruences, a property which is both essential and difficult to prove.

A previous post introduced Howe's method in the context of the lambda calculus; this post will explore it in greater detail.

Introduction

The lambda calculus does not prescribe any particular reduction strategy. There are two major paradigms:

• one paradigm regards the lambda calculus as a term rewriting system so that lambda terms are treated as syntax trees and reduction occurs at any redex within a syntax tree, even inside abstractions, which includes the following reduction strategies:
  • normal order reduction (leftmost, outermost redex),
  • applicative order reduction (leftmost, innermost redex),
  • full beta reduction (non-deterministic beta reduction);
• another paradigm regards the lambda calculus as a prototypical functional programming language so that lambda abstractions are regarded as functions and reduction does not occur inside abstractions, which includes the following reduction strategies:
  • call-by-value (arguments are reduced prior to application - like applicative order reduction, except reduction is not performed inside abstractions),
  • call-by-name (arguments are not reduced prior to application - like normal order reduction, except reduction is not performed inside abstractions).

In this post, we adopt the functional paradigm, so we only consider the call-by-value and call-by-name reduction strategies. In this paradigm, evaluation is deterministic (each term evaluates to a unique value).

One fundamental problem is the determination of when two closed lambda terms are equivalent (we can only compute with closed terms). Since we regard lambda abstractions as functions, it makes sense to use some sort of functional equivalence.

The usual notion of extensional equality that functions qua sets inherit from set theory is not appropriate since the lambda calculus is an intensional calculus of functions, that is, lambda abstractions represent concrete procedures for mapping inputs to outputs, whereas in set theory, functions are completely determined by their input-output pairings.

As an example, consider the Church encoding of the natural numbers. In this encoding, a natural number is encoded as a (curried) function that accepts two arguments, one representing the successor operation and another representing zero, and then constructs a natural number accordingly.

• \(\mathrm{zero} = (\lambda s . (\lambda z . z))\),
• \(\mathrm{one} = (\lambda s . (\lambda z . (s z)))\),
• \(\mathrm{two} = (\lambda s . (\lambda z . (s (sz))))\),
• etc.

The successor function, i.e., the function \(n \mapsto n + 1\), can be represented as follows:

\[\mathrm{succ} = (\lambda n . (\lambda s . (\lambda z . (s ((ns) z))))).\]

One would certainly hope that one of the most elementary of all mathematical propositions, namely, \(1 + 1 = 2\), would be represented faithfully by this encoding. In other words, it ought to be the case for some notion of equivalence (denoted by the symbol \(\sim\)) that

\[(\mathrm{succ} ~ \mathrm{one}) \sim \mathrm{two}.\]

Now, if we treat equivalence as syntactic identity, then this proposition is manifestly false, since, under both the call-by-value and call-by-name reduction strategies,

\begin{align*}(\mathrm{succ} ~ \mathrm{one}) &= ((\lambda n . (\lambda s . (\lambda z . (s ((ns) z))))) (\lambda s . (\lambda z . (s z)))) \\&= (\lambda s . (\lambda z . (s (((\lambda s . (\lambda z . (s z))) s) z)))),\end{align*}

yet this is not syntactically identical to \(\mathrm{two}\).

If we treat equivalence as strict extensional equality, i.e., two abstractions are equivalent if and only if they reduce to syntactically identical terms when applied to the same argument value for all possible argument values, then, for any value \(s_v\) (where values are closed lambda abstractions for the call-by-value evaluation strategy, and closed lambda terms for the call-by-name evaluation strategy),

\[((\mathrm{succ} ~ \mathrm{one}) s_v) = (\lambda z . (s_v (((\lambda s . (\lambda z . (s z))) s_v) z)))\]

whereas

\[(\mathrm{two} ~ s_v) = (\lambda z . (s_v (s_v z))),\]

so it is not the case that these terms reduce to syntactically identical terms for all possible argument values.

However, we could consider a weak extensional equality, namely, two abstractions are equivalent if and only if they reduce to equivalent terms when applied to the same argument value for all possible argument values. Of course, this cannot serve as a definition since it is circular in nature. Nevertheless, it is a valid property of relations on terms:

\[P(R) \equiv \forall e_1, e_2 \in \Lambda(\emptyset)\Big[(e_1, e_2) \in R \Leftrightarrow \forall x \in \mathcal{V}\forall e_1' \in \Lambda\Big(e_1 \Downarrow (\lambda x. e_1') \Rightarrow \exists e_2' \in \Lambda\Big(e_2 \Downarrow (\lambda x . e_2') \land \forall v \in \mathrm{Arg}((e_1'[v/x], e_2'[v/x]) \in R)\Big)\Big)\Big].\]

Here, in the case of the call-by-value reduction strategy, \(\Downarrow\) stands for call-by-value big-step evaluation \(\Downarrow_{\mathrm{v}}\) and \(\mathrm{Arg}\) stands for the set of closed values (lambda abstractions) \(V(\emptyset)\), and, in the case of the call-by-name reduction strategy, \(\Downarrow\) stands for call-by-name big-step evaluation \(\Downarrow_{\mathrm{n}}\) and \(\mathrm{Arg}\) stands for the set of closed terms \(\Lambda(\emptyset)\). Thus, implicitly, there are two properties, \(P_{\mathrm{v}}\) for call-by-value and \(P_{\mathrm{n}}\) for call-by-name, and we display them in a single schematic formula \(P\).

We can choose the greatest relation satisfying this property as our notion of equivalence, i.e., we can specify a coinductive definition. If we define a map \(F_{\mathrm{app}} : \mathcal{P}(\Lambda(\emptyset) \times \Lambda(\emptyset)) \rightarrow \mathcal{P}(\Lambda(\emptyset) \times \Lambda(\emptyset))\) as

\[F_{\mathrm{app}}(R) = \Big\{(e_1, e_2) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \mid \forall x \in \mathcal{V}\forall e_1' \in \Lambda\Big(e_1 \Downarrow (\lambda x. e_1') \Rightarrow \exists e_2' \in \Lambda\Big(e_2 \Downarrow (\lambda x . e_2') \land \forall v \in \mathrm{Arg}((e_1'[v/x], e_2'[v/x]) \in R)\Big)\Big)\Big\},\]

then \(P(R)\) is equivalent to \(R = F_{\mathrm{app}}(R)\), i.e., \(R\) satisfies \(P\) if and only if it is a fixed point of the map \(F_{\mathrm{app}}\). Since \(F_{\mathrm{app}}\) is monotone, by the Knaster-Tarski theorem, the greatest fixed point of \(F_{\mathrm{app}}\) and hence the greatest relation \(\sim\) satisfying \(P\) is given by

\[\sim = \bigcup\{R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset) \mid R \subseteq F_{\mathrm{app}}(R)\}.\]

Note that the least relation satisfying \(P\) and hence least fixed point is simply the empty relation, and is therefore trivial.

Note also that \(F_{\mathrm{app}}\) and \(\sim\) were defined schematically, so there are variants \(F_{\mathrm{app,v}}\) and \(F_{\mathrm{app,n}}\) and \(\sim_{\mathrm{v}}\) and \(\sim_{\mathrm{n}}\).

The relation \(\sim\) so defined is called applicative bisimilarity.

Now that we've defined a candidate notion of equivalence of closed lambda terms, we need to verify that it is appropriate.

First of all, any such relation should be an equivalence relation. We can verify that applicative bisimilarity is an equivalence relation using proof by coinduction.

For instance, to prove that applicative bisimilarity is reflexive, we define the relation

\[R = \{(e, e) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \mid e \in \Lambda(\emptyset)\}.\]

To prove that \(\sim\) is reflexive, we need to show that \(R \subseteq \sim\). Since \(\sim\) was defined as the greatest post-fixed point (and hence also greatest fixed point) of \(F_{\mathrm{app}}\), if we can show that \(R \subseteq F_{\mathrm{app}}(R)\), i.e., that \(R\) is a post-fixed point of \(F_{\mathrm{app}}\), then it follows that \(R \subseteq \sim\). Such a post-fixed point is called an applicative bisimulation.

Likewise, to prove that applicative bisimilarity is symmetric, we define the relation

\[S = \{(e_1, e_2) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \mid e_2 \sim e_1\}.\]

Then, \(\sim\) is symmetric if and only if \(S \subseteq F_{\mathrm{app}}(S)\).

Again, to prove that applicative bisimilarity is transitive, we define the relation

\[T = \{(e_1, e_3) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \mid \exists e_2 \in \Lambda(\emptyset)(e_1 \sim e_2 \land e_2 \sim e_3)\}.\]

Then, \(\sim\) is transitive if and only if \(T \subseteq F_{\mathrm{app}}(T)\).

Thus, establishing that applicative bisimilarity is an equivalence relation is not difficult. However, we also require any notion of equivalence to be substitutive, i.e., to be a congruence. A congruence is a relation \(R\) such that

• \(xRx\) for all \(x \in \mathcal{V}\),
• For all \(x \in \mathcal{V}\) and \(e,e' \in \Lambda\), \((\lambda x . e) ~R~ (\lambda x . e')\) whenever \(eRe'\),
• For all \(e_1,e_1',e_2,e_2' \in \Lambda\), \((e_1e_2) ~R~ (e_1'e_2')\) whenever \(e_1Re_1'\) and \(e_2Re_2'\).

Thus, congruence relations are those relations that are stable under replacement, i.e., replacing related terms for one another in larger related expressions preserves the relationship of the larger related expressions.

In fact, congruences can be defined as pre-fixed points of certain relational liftings of the monotone map that defines the inductive syntax of lambda terms.

However, applicative bisimilarity is only defined for closed terms whereas congruences are defined for all lambda terms.

We will solve this problem in two steps: first, we will define context-indexed congruences and second, we will define a systematic method for extending relations on closed lambda terms to context-indexed relations. Then we will be in a position to state what it means for applicative bisimilarity to be a congruence, namely, it is a congruence if its context-indexed extension is a context-indexed congruence.

Context-Indexed Congruences

In this section, we will discuss context-indexed congruences.

We define a poset of context-indexed sets of lambda terms as follows:

\[\mathcal{L}_s = \prod_{\Gamma \in \mathcal{C}}\mathcal{P}(\Lambda(\Gamma)).\]

Thus, each element \(\mathcal{A} \in \mathcal{L}_s\) is a function that maps a context \(\Gamma\) to a subset \(\mathcal{A}_{\Gamma} \subseteq \Lambda(\Gamma)\) of lambda terms whose free variables are within \(\Gamma\).

We define a partial ordering as follows:

\[\mathcal{A} \le \mathcal{B} \Leftrightarrow \mathcal{A}_{\Gamma} \subseteq \mathcal{B}_{\Gamma} \text{ for all } \Gamma \in \mathcal{C}.\]

We define the meet of a subset \(\mathcal{S} \subseteq \mathcal{L}_s\) of context-indexed sets of lambda terms as

\[\left(\bigwedge_{\mathcal{A} \in \mathcal{S}}\mathcal{A}\right)_{\Gamma} = \bigcap_{\mathcal{A} \in \mathcal{S}}\left(\mathcal{A}_{\Gamma}\right).\]

Similarly, we defined the join as

\[\left(\bigvee_{\mathcal{A} \in \mathcal{S}}\mathcal{A}\right)_{\Gamma} = \bigcup_{\mathcal{A} \in \mathcal{S}}\left(\mathcal{A}_{\Gamma}\right).\]

Thus, \((\mathcal{L}_s, \le, \wedge, \vee)\) forms a complete lattice.

We then define the context-indexed syntax of the lambda calculus as follows:

\begin{align*}\left(F_{\lambda^+}(\mathcal{A})\right)_{\Gamma} &= \Gamma \\&\cup \{(\lambda x . e) \mid x \in \mathcal{V} \setminus \Gamma \land e \in \mathcal{A}_{(\Gamma \cup \{x\})}\} \\&\cup \{(e_1e_2) \mid e_1, e_2 \in \mathcal{A}_{\Gamma}\},\end{align*}

\[\Lambda(\Gamma) = \mu F_{\lambda^+}.\]

Next, we define a set of indices for these terms as

\begin{align*}I_{\Gamma} &= \{(\mathrm{var}, x) \mid x \in \Gamma\} \\&\cup \{(\mathrm{abs}, x) \mid x \in \Gamma\} \\& \cup \{\mathrm{abs}\}\end{align*}

where \(\mathrm{var}\), \(\mathrm{abs}\), and \(\mathrm{app}\) are any distinct sets that serve as labels. We define

\[\left(F_{(\mathrm{var}, x)}(\mathcal{A})\right)_{\Gamma} = \{x\},\]

\[\left(F_{(\mathrm{abs}, x)}(\mathcal{A})\right)_{\Gamma} = \{(\lambda x . e) \mid x \in \mathcal{V} \setminus \Gamma \land e \in \mathcal{A}_{(\Gamma \cup \{x\})}\},\]

\[\left(F_{\mathrm{app}}(\mathcal{A})\right)_{\Gamma} = \{(e_1e_2) \mid e_1, e_2 \in \mathcal{A}_{\Gamma}\}.\]

We then note that

\[F_{\lambda^+}(\mathcal{A})_{\Gamma} = \bigcup_{i \in I_{\Gamma}}\left(F_i(\mathcal{A})\right)\]

and, whenever \(i \ne j\),

\[(F_i)(\mathcal{A})_{\Gamma} \cap (F_j)(\mathcal{A})_{\Gamma} = \emptyset.\]

We define the set of context-indexed relations on lambda terms as

\[\mathcal{L}_r = \prod_{\Gamma \in \mathcal{C}}\mathcal{P}(\Lambda(\Gamma) \times \Lambda(\Gamma)).\]

Then, for any monotone map \(F : \mathcal{L}_s \rightarrow \mathcal{L}_s\) and context-indexed relation \(\mathcal{R} \in \mathcal{L}_r\), we define the relational lifting \(\overline{F} : \mathcal{L}_r \rightarrow \mathcal{L}_r\) as follows:

\[\left(\overline{F}(\mathcal{R})\right)_{\Gamma} = \left\{(x,y) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \middle\vert{} \forall i \in I_{\Gamma} \begin{aligned} &\forall U \subseteq \Lambda(\Gamma) \big(x \in F_i(U) \implies y \in F_i(\mathcal{R}[U]_{\Gamma})\big) \\ &\quad \land \\ &\forall V \subseteq \Lambda(\Gamma) \big(y \in F_i(V) \implies x \in F_i(\mathcal{R}^{-1}[V]_{\Gamma})\big) \end{aligned} \right\},\]

where \(\mathcal{R}[U] \in \mathcal{L}_s\) is the context-indexed set defined as

\[\mathcal{R}[U]_{\Gamma} = \{y \in \Lambda(\Gamma) \mid \exists x \in U \left((x,y) \in \mathcal{R}_{\Gamma}\right)\}\]

and \(\mathcal{R}^{-1}[V] \in \mathcal{L}_s\) is the context-indexed set defined as

\[\mathcal{R}^{-1}[V]_{\Gamma} = \{x \in \Lambda(\Gamma) \mid \exists y \in V \left((x,y) \in \mathcal{R}_{\Gamma}\right)\}.\]

We then define a context-indexed congruence as a pre-fixed point of \(\overline{F_{\lambda^+}}\), i.e., a context-indexed relation \(\mathcal{R} \in \mathcal{L}_r\) such that

\[\overline{F_{\lambda^+}}(\mathcal{R}) \le \mathcal{R}.\]

Expanding this definition explicitly, this means that

\begin{align*}\left(\overline{F_{\lambda^+}}(\mathcal{R})\right)_{\Gamma} &= \{(x,x) \mid x \in \Gamma\} \\&\cup \{((\lambda x . e), (\lambda x . e')) \mid x \in \mathcal{V} \setminus \Gamma \land (e,e') \in \mathcal{R}_{\Gamma \cup \{x\}}\} \\&\cup \{((e_1e_2), (e_1'e_2')) \mid (e_1,e_1') \in \mathcal{R}_{\Gamma} \land (e_2,e_2') \in \mathcal{R}_{\Gamma}\}.\end{align*}

Context-Indexed Extensions

Next, we will define the extension of a closed relation to a context-indexed relation.

Define the set of closed relations on lambda terms as

\[L_0 = \mathcal{P}(\Lambda(\emptyset) \times \Lambda(\emptyset)).\]

Define the set of environments as

\[\mathrm{Env}_{\mathrm{v}}(\Gamma) = \mathrm{Sub}(\Gamma, V(\emptyset))\]

for the call-by-value evaluation strategy and

\[\mathrm{Env}_{\mathrm{n}}(\Gamma) = \mathrm{Sub}(\Gamma, \Lambda(\emptyset))\]

for the call-by-name evaluation strategy, where \(\mathrm{Sub}(\Gamma, \mathrm{Arg})\) is the set of all substitution lists in context \(\Gamma\) and with substitutions in \(\mathrm{Arg}\) (this was defined inductively using a slightly different notation in a previous post).

For each evaluation strategy \(\mathrm{s} \in \{\mathrm{v}, \mathrm{n}\}\), we define the extension operator \(\mathcal{E}_{\mathrm{s}} : L_0 \rightarrow \mathcal{L}_r\) as follows for any \(R_0 \in L_0\):

\[(\mathcal{E}_{\mathrm{s}}(R_0))_{\Gamma} = \{(e_1, e_2) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid \forall \sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\left((e_1[\sigma], e_2[\sigma]) \in R_0\right))\}.\]

Now we can state what it means for applicative bisimilarity to be a congruence:

\[\overline{F_{\lambda^+}}(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})) \le \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}).\]

We will use the notation

\[\Gamma \vdash e_1 \sim_{\mathrm{s}} e_2\]

to mean \((e_1, e_2) \in (\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}))_{\Gamma}\).

We also abbreviate \(\Gamma \cup \{x\} \vdash \dots\) as \(\Gamma,x \vdash \dots\).

Then, by applying the definition of \(\overline{F_{\lambda^+}}\) and the definition of \(\mathcal{E}_{\mathrm{s}}\) and using this notation, we obtain the following characterization of congruence: for all \(\Gamma \in \mathcal{C}\),

1. \(\Gamma \vdash x \sim_{\mathrm{s}} x\) for all \(x \in \Gamma\);
2. For all \(x \in \mathcal{V} \setminus \Gamma\) and for all \(e,e' \in \Lambda(\Gamma \cup \{x\})\), \(\Gamma, x \vdash (\lambda x . e) \sim_{\mathrm{s}} (\lambda x . e')\) whenever \(\Gamma \vdash e \sim_{\mathrm{s}} e'\);
3. For all \(e_1, e_1', e_2, e_2' \in \Lambda(\Gamma)\), \(\Gamma \vdash (e_1e_2) \sim_{\mathrm{s}} (e_1'e_2')\) whenever \(\Gamma \vdash e_1 \sim_{\mathrm{s}} e_1'\) and \(\Gamma \vdash e_2 \sim_{\mathrm{s}} e_2'\).

Galois Connection

Next, we will explore various Galois connections related to context-indexed extensions.

Definition (Galois Connection). Let \((A, \le_A)\) and \((B, \le_B)\) be any two partially-ordered sets. A Galois connection consists of a pair of monotone maps \(F : A \rightarrow B\) and \(G : B \rightarrow A\) such that, for every \(a \in A\) and \(b \in B\),

\[F(a) \le_B b \Leftrightarrow a \le_A G(b).\]

Every environment \(\sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\) induces a pullback map \(\sigma^* : L_0 \rightarrow \mathcal{P}(\Lambda(\Gamma) \times \Lambda(\Gamma))\) defined as follows:

\[\sigma^*(R_0) = \{(e_1, e_2) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid (e_1[\sigma], e_2[\sigma]) \in R\}.\]

Note that

\begin{align*}\sigma^*\left(\bigwedge_{i \in I}R_i\right) &= \sigma^*\left(\bigcap_{i \in I}R_i\right) \\&= \left\{(e_1, e_2) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid (e_1[\sigma], e_2[\sigma]) \in \bigcap_{i \in I}R_i\right\} \\&= \bigcap_{i \in I}\left\{(e_1, e_2) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid (e_1[\sigma], e_2[\sigma]) \in R_i\right\} \\&= \bigwedge_{i \in I}\sigma^*(R_i)\end{align*}

and

\begin{align*}\sigma^*\left(\bigvee_{i \in I}R_i\right) &= \sigma\left(\bigcup_{i \in I}R_i\right) \\&= \left\{(e_1, e_2) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid (e_1[\sigma], e_2[\sigma]) \in \bigcup_{i \in I}R_i\right\} \\&= \bigcup_{i \in I}\left\{(e_1, e_2) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid (e_1[\sigma], e_2[\sigma]) \in R_i\right\} \\&= \bigvee_{i \in I}\sigma^*(R_i),\end{align*}

and thus \(\sigma^*\) preserves arbitrary meets and joins.

Thus, by the adjoint functor theorem for Galois connections, it follows that there exist both a left and right adjoint:

\[\exists_{\sigma} \dashv \sigma^* \dashv \forall_{\sigma}.\]

We define a sub-lattice of substitution-closed context-indexed relations \(\mathcal{L}_r^{\mathrm{sub}}\) of \(\mathcal{L}_r\) as follows:

\[\mathcal{L}_r^{\mathrm{sub}} = \{ \mathcal{R} \in \mathcal{L}_r \mid \forall \Gamma, (e_1, e_2) \in \mathcal{R}_\Gamma, \sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma) \implies (e_1[\sigma], e_2[\sigma]) \in \mathcal{R}_\emptyset \}.\]

Remark (Substitution Action / Pullback): Any substitution \(\sigma \in \mathrm{Sub}(\Gamma, \Delta)\) induces a monotone reindexing map \(\sigma^* : \mathcal{P}(\Lambda(\Gamma)^2) \to \mathcal{P}(\Lambda(\Delta)^2)\) given by \(\sigma^*(R) = \{ (e_1[\sigma], e_2[\sigma]) \mid (e_1, e_2) \in R \}\). Under this view, a context-indexed relation \(\mathcal{R} \in \mathcal{L}_r\) is substitution-closed if and only if it is monotone with respect to reindexing: \(\sigma^*(\mathcal{R}_\Gamma) \subseteq \mathcal{R}_\Delta\) for all \(\sigma \in \mathrm{Sub}(\Gamma, \Delta)\). What we stated above is a more restricted version of this property (limited only to the empty context as the codomain).

We then define a restriction operator \(\mathrm{Res}_{\mathrm{s}} : \mathcal{L}_r^{\mathrm{sub}} \rightarrow L_0\) which projects a context-indexed relation onto its fiber over the empty set restricted to the appropriate argument type:

\[\mathrm{Res}_{\mathrm{s}}(\mathcal{R}) = \mathcal{R}_{\emptyset}.\]

Then, by definition,

\begin{align*}\mathrm{Res}_{\mathrm{s}}\left(\bigvee_{i \in I}\mathcal{R}^{(i)}\right) &= \left(\bigvee_{i \in I}\mathcal{R}^{(i)}\right)_{\emptyset} \\&= \left(\bigcup_{i \in I}\mathcal{R}^{(i)}_{\emptyset}\right) \\&= \bigcup_{i \in I}\mathcal{R}^{(i)}_{\emptyset} \\&= \bigcup_{i \in I}\mathrm{Res}_{\mathrm{s}}(\mathcal{R}^{(i)}) \\&= \bigvee_{i \in I}\mathrm{Res}_{\mathrm{s}}(\mathcal{R}^{(i)}). \end{align*}

Thus, \(\mathrm{Res}\) preserves arbitrary joins, and hence, by the adjoint functor theorem, possesses a unique right adjoint \(\mathcal{E}_{\mathrm{s}}\):

\[\mathrm{Res}_{\mathrm{s}} \dashv \mathcal{E}_{\mathrm{s}}.\]

By definition of Galois connection, this means that, for any \(R_0 \in L_0\) and \(\mathcal{R} \in \mathcal{L}_r\),

\[\mathcal{R} \le \mathcal{E}_{\mathrm{s}}(R_0) \Leftrightarrow \mathrm{Res}_{\mathrm{s}}(\mathcal{R}) \le R_0.\]

Define

\[A(R_0) = \{\mathcal{R} \in \mathcal{L}_r^{\mathrm{sub}} \mid \mathrm{Res}_{\mathrm{s}}(\mathcal{R}) \subseteq R_0\}.\]

Consider any context-indexed relation \(\mathcal{R} \in A(R_0)\). By definition of \(A(R_0)\), \(\mathrm{Res}_{\mathrm{s}}(\mathcal{R}) \subseteq R_0\), and by definition of the Galois connection above, it follows that \(\mathcal{R} \le \mathcal{E}_{\mathrm{s}}(R_0)\), and hence \(\mathcal{E}_{\mathrm{s}}(R_0)\) is an upper bound of \(A(R_0)\).

Since the partial order \(\le\) is reflexive, \(\mathcal{E}_{\mathrm{s}}(R_0) \le \mathcal{E}_{\mathrm{s}}(R_0)\). Applying this fact to the Galois connection yields \(\mathrm{Res}_{\mathrm{s}}(\mathcal{E}_{\mathrm{s}}(R_0)) \le R_0\), i.e., \(\mathrm{Res}_{\mathrm{s}}(\mathcal{E}_{\mathrm{s}}(R_0)) \subseteq R_0\). Thus, \(\mathcal{E}_{\mathrm{s}}(R_0) \in A(R_0)\), so \(\mathcal{E}_{\mathrm{s}}(R_0)\) is the greatest element of \(A(R_0)\). Since the greatest element coincides with the join, it follows that

\[\mathcal{E}_{\mathrm{s}}(R_0) = \bigvee \{\mathcal{R} \in \mathcal{L}_r^{\mathrm{sub}} \mid \mathrm{Res}_{\mathrm{s}}(\mathcal{R}) \subseteq R_0\}.\]

Next, we have the following theorem.

Theorem (Substitution Consistency). For any relation \(R_0 \in L_0\),

\[\left(\mathcal{E}_{\mathrm{s}}(R_0)\right)_{\Gamma} = \{(e_1, e_2) \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid \forall \sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\left((e_1[\sigma], e_2[\sigma]) \in R_0\right)\}.\]

Proof. As previously established,

\[\mathcal{E}_{\mathrm{s}}(R_0) = \bigvee \{\mathcal{R} \in \mathcal{L}_r \mid \mathrm{Res}_{\mathrm{s}}(\mathcal{R}) \subseteq R_0\}.\]

Define

\[A = \{\mathcal{R} \in \mathcal{L}_r \mid \mathrm{Res}_{\mathrm{s}}(\mathcal{R}) \subseteq R_0\}.\]

Then,

\begin{align*}\left(\mathcal{E}_{\mathrm{s}}(R_0)\right)_{\Gamma} &= \left(\bigvee_{\mathcal{R} \in A}\mathcal{R}\right)_{\Gamma} \\&= \bigcup_{\mathcal{R} \in A}\mathcal{R}_{\Gamma}.\end{align*}

Let \(\Gamma \in \mathcal{C}\) be any context.

Direction 1 (\(\Leftarrow\)). Assume that \((e_1[\sigma], e_2[\sigma]) \in R_0\) for all \(\sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\).

Define a context-indexed relation \(\mathcal{S}\) as follows:

\[\mathcal{S}_{\Delta} = \begin{cases}\{(e_1, e_2)\} & \text{if } \Delta = \Gamma \\ \{(e_1[\sigma], e_2[\sigma]) \mid \sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\} & \text{if } \Delta = \emptyset \text{ and } \Gamma \ne \emptyset \\ \emptyset & \text{otherwise}.\end{cases}\]

If \(\Gamma = \emptyset\), then \(\mathrm{Env}_{\mathrm{s}}(\emptyset) = \{!_{\emptyset}\} = \{e_1[!_{\emptyset}], e_2[!_{\emptyset}]\} \subseteq R_0\) by hypothesis.

If \(\Gamma \ne \emptyset\), then \(\mathcal{S}_{\emptyset} = \{(e_1[\sigma], e_2[\sigma]) \mid \sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\} \subseteq R_0\) by hypothesis.

Thus, in either case, \(\mathcal{S}_{\emptyset} \subseteq R_0\), so \(\mathrm{Res}_{\mathrm{s}}(\mathcal{S}) \subseteq R_0\) and \(\mathcal{S} \in A\).

Since \(\mathcal{S} \in A\) and \((e_1, e_2) \in \mathcal{S}_{\Gamma} = \{(e_1, e_2)\}\), by definition,

\[(e_1, e_2) \in \bigcup_{\mathcal{R} \in A}\mathcal{R}_{\Gamma} = \mathcal{E}_{\mathrm{s}}(R_0).\]

Direction 2 (\(\Rightarrow\)). Suppose \((e_1, e_2) \in (\mathcal{E}_{\mathrm{s}}(\mathcal{R}))_{\Gamma}\).

By definition of set union, it follows that there exists a context-indexed relation \(\mathcal{S} \in \mathcal{L}_r^{\mathrm{sub}}\) such that \(\mathcal{S}_{\emptyset} \subseteq R_0\) and \((e_1, e_2) \in \mathcal{S}_{\Gamma}\). Since \(\mathcal{S} \in \mathcal{L}_r^{\mathrm{sub}}\), it is substitution-closed by definition. Thus, for every \(\sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\), it follows that \((e_1[\sigma], e_2[\sigma]) \in \mathcal{S}_{\emptyset} \subseteq R_0\). \(\square\)

Thus, the definition of the extension operator as the right adjoint to the restriction operator is equivalent to the original definition.

This theorem also implies that

\[\left(\mathcal{E}_{\mathrm{s}}(R_0)\right)_{\Gamma} = \bigwedge_{\sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)}\sigma^*(R_0).\]

Since \(\mathcal{E}_{\mathrm{s}}\) is a right adjoint, it automatically satisfies certain order-theoretic properties enjoyed by all right adjoints:

1. Preservation of meets: \(\mathcal{E}_{\mathrm{s}}\left(\bigwedge_{i \in I}R_i\right) = \bigwedge_{i \in I}\mathcal{E}_{\mathrm{s}}(R_i)\);
2. Monotonicity: \(R_0 \subseteq R_0' \Rightarrow \mathcal{E}_{\mathrm{s}}(R_0) \le \mathcal{E}_{\mathrm{s}}(R_0')\);
3. Co-unit identity: for \(\Gamma = \emptyset\), \((\mathcal{E}_{\mathrm{s}}(R_0))_{\emptyset} = !_{\emptyset}(R_0) = R_0\) which means that \(\mathrm{Res}_{\mathrm{s}}(\mathcal{E}_{\mathrm{s}}(R_0)) = R_0\).

Motivation

Recall that a context-indexed relation \(\mathcal{R} \in \mathcal{L}\) is a congruence if

\[\overline{F_{\lambda^+}}(\mathcal{R}) \le \mathcal{R},\]

i.e., if it is a pre-fixed point of the map \(\overline{F_{\lambda^+}} : \mathcal{L}_r \rightarrow \mathcal{L}_r\) defined as

\begin{align*}\overline{F_{\lambda^+}}(\mathcal{R})_{\Gamma} &= \{(x,x) \mid x \in \Gamma\} \\&\cup \{((\lambda x . e), (\lambda x . e')) \mid x \in \mathcal{V} \setminus \Gamma \land (e, e') \in \mathcal{R}_{\Gamma \cup \{x\}}\} \\&\cup \{((e_1 e_2), (e_1' e_2')) \mid (e_1, e_1') \in \mathcal{R}_{\Gamma} \land (e_2, e_2') \in \mathcal{R}_{\Gamma}\}.\end{align*}

Since \(\mathcal{L}_r\) is a complete lattice and \(\overline{F_{\lambda^+}}\) is a monotone map, by the Knaster-Tarski theorem, we can systematically obtain a least fixed point of \(\overline{F_{\lambda^+}}\). The appropriate notion of "meet" for some subset \(S \subseteq \mathcal{L}_r\) is "fiberwise" intersection,

\[\left(\bigwedge_{\mathcal{R} \in S}\mathcal{R}\right)_{\Gamma} = \bigcap_{\mathcal{R} \in S}\left(\mathcal{R}_{\Gamma}\right),\]

and the appropriate notion of order is

\[\mathcal{R}_1 \le \mathcal{R}_2 \Leftrightarrow \forall \Gamma \in \mathcal{C}\left((\mathcal{R}_1)_{\Gamma} \subseteq (\mathcal{R}_2)_{\Gamma}\right),\]

so we obtain

\[(\mu \overline{F_{\lambda^+}})_\Gamma = \bigcap \left\{ \mathcal{R}_\Gamma \;\middle\vert{}\; \mathcal{R} \in \mathcal{L} \land \overline{F_{\lambda^+}}(\mathcal{R}) \le \mathcal{R} \right\}.\]

Now, though this produces a congruence, we are interested in demonstrating that the open extension \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) of applicative bisimilarity \(\sim_{\mathrm{s}}\) is a (context-indexed) congruence. Our strategy is to compose the relation \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) with the map \(\overline{F_{\lambda^+}}\) to produce a new map \(\Phi_{\mathrm{s}}\) defined as

\[\Phi_{\mathrm{s}}(\mathcal{R}) = \overline{F_{\lambda^+}}(\mathcal{R}) \circ \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}).\]

Since this is a monotone map, we can apply the Knaster-Tarski theorem to obtain a fixed point again:

\[\mathcal{H}_{\mathrm{s}} = \mu \Phi_{\mathrm{s}} = \bigwedge \{ \mathcal{R} \in \mathcal{L}_r \mid \Phi_{\mathrm{s}}(\mathcal{R}) \le \mathcal{R} \},\]

or, equivalently,

\[\left(\mathcal{H}_{\mathrm{s}}\right)_\Gamma = \left(\mu \Phi_{\mathrm{s}}\right)_\Gamma = \bigcap \left\{ \mathcal{R}_\Gamma \;\middle\vert{}\; \mathcal{R} \in \mathcal{L}_r \land \Phi_{\mathrm{s}}(\mathcal{R}) \le \mathcal{R} \right\}.\]

As it turns out, \(\mathcal{H}_{\mathrm{s}} = \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\), so this is just the relation \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) in another guise. However, \(\mathcal{H}_{\mathrm{s}}\) is inductively defined and is a congruence by construction, which enables us to prove that \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) is a congruence.

Thus, extensionally, \(\mathcal{H}_{\mathrm{s}}\) and \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) are the same, i.e., they are identical as sets. However, intensionally, that is, definitionally, they are quite different: the former is inductively defined whereas the latter is coinductively defined. Howe's method is the mathematical trick that enables bridging these worlds.

This technique is known as Howe's method and is due to computer scientist Douglas J. Howe.

First, we will establish that \(\mathcal{H}_{\mathrm{s}}\) is a congruence by construction. Because \(\mathcal{H}_{\mathrm{s}}\) is a fixed point, we have

\[\mathcal{H}_{\mathrm{s}} = \overline{F_{\lambda^+}}(\mathcal{H}_{\mathrm{s}}) \circ \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}).\]

Since \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) is reflexive, \(\mathrm{id} \le \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\), where \(\mathrm{id}_{\Gamma} = \{(e, e) \mid e \in \Lambda(\Gamma)\}\) is the identity relation on terms. Since relational pre-composition is monotone, i.e., the map \(\mathcal{X} \mapsto \mathcal{R} \circ \mathcal{X}\) on \(\mathcal{L}_r\) is monotone for any \(\mathcal{R} \in \mathcal{L}_r\), it follows that

\[\overline{F_{\lambda^+}}(\mathcal{H}_{\mathrm{s}}) = \overline{F_{\lambda^+}}(\mathcal{H}_{\mathrm{s}}) \circ \mathrm{id} \le \overline{F_{\lambda^+}}(\mathcal{H}_{\mathrm{s}}) \circ \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}) = \mathcal{H}_{\mathrm{s}}\]

and hence

\[\overline{F_{\lambda^+}}(\mathcal{H}_{\mathrm{s}}) \le \mathcal{H}_{\mathrm{s}}.\]

Thus, under the assumption that \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) possesses the requisite properties (namely, reflexivity), \(\mathcal{H}_{\mathrm{s}}\) is indeed a congruence by design.

Next, we will show that \(\mathcal{H}_{\mathrm{s}} = \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\). Since \(\mathcal{H}_{\mathrm{s}}\) is reflexive,

\[\mathrm{id} \le \overline{F_{\lambda^+}}(\mathcal{H}_{\mathrm{s}}).\]

Since relational post-composition is monotone, i.e., the map \(\mathcal{X} \mapsto \mathcal{X} \circ \mathcal{R}\) on \(\mathcal{L}_r\) is monotone for any \(\mathcal{R} \in \mathcal{L}_r\), it follows that

\[\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}) = \mathrm{id} \circ \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}) \le \overline{F_{\lambda^+}}(\mathcal{H}_{\mathrm{s}}) \circ \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}) = \Phi_{\mathrm{s}}(\mathcal{H}_{\mathrm{s}})\]

and hence

\[\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}) \le \mathcal{H}_{\mathrm{s}}.\]

Finally, we show that \(\mathcal{H}_{\mathrm{s}} \le \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\). First, we must show that the relation \(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\) is a bisimulation (see a subsequent section for a proof), i.e., that

\[\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset} \subseteq \overline{F_{\mathrm{app}}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right),\]

where we write \(F_{\mathrm{app}}\) generically for either \(F_{\mathrm{app,v}}\) or \(F_{\mathrm{app,n}}\), i.e., the monotone maps that are used to define call-by-value and call-by-name applicative bisimilarity, respectively.

Then, since \(\sim_{\mathrm{s}}\) is the greatest bisimulation, it follows that

\[\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset} \subseteq \sim_{\mathrm{s}}.\]

Then, since \(\mathcal{H}_{\mathrm{s}} \le \mathcal{E}_{\mathrm{s}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right)\) (see a subsequent section for a proof) and \(\mathcal{E}_{\mathrm{s}}\) is monotone, it follows that

\[\mathcal{H}_{\mathrm{s}} \le \mathcal{E}_{\mathrm{s}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right) \le \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}).\]

Thus, since \(\mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}) \le \mathcal{H}_{\mathrm{s}}\) and \(\mathcal{H}_{\mathrm{s}} \le \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}})\) and \(\le\) is antisymmetric, it follows that

\[\mathcal{H}_{\mathrm{s}} = \mathcal{E}_{\mathrm{s}}(\sim_{\mathrm{s}}).\]

In the next few sections, we will supply various lemmas that support the proof outlined above.

Substitution Lemma

Next, we will state an important lemma called the substitution lemma.

Here, we write

\[\Gamma \vdash e \mathcal{H}_{\mathrm{s}} e'\]

to indicate \((e,e') \in \left(\mathcal{H}_{\mathrm{s}}\right)_{\Gamma}\).

Lemma (Substitution - Howe's). For any context \(\Gamma \in \mathcal{C}\), variable \(x \in \mathcal{V} \setminus \Gamma\), terms \(M,N \in \Lambda(\Gamma)\), and arguments \(A,B \in \mathrm{Arg}\), if \(\Gamma,x \vdash M ~\mathcal{H}_{\mathrm{s}}~ N\) and \(\emptyset \vdash A ~\mathcal{H}_{\mathrm{s}}~ B\), then \(\Gamma \vdash M[A/x] ~\mathcal{H}_{\mathrm{s}}~ N[B/x]\).

Proof. See this previous post which proves the lemma in detail.

Thus, we have the following schematic rule:

\[\frac{\Gamma \in \mathcal{C}, x \in \mathcal{V} \setminus \Gamma, \Gamma,x \vdash M ~\mathcal{H}_{\mathrm{s}}~ N, \emptyset \vdash A ~\mathcal{H}_{\mathrm{s}}~ B}{\Gamma \vdash M[A/x] ~\mathcal{H}_{\mathrm{s}}~ N [B/x]}.\]

Note that the substitution lemma can be extended by induction on the context length to contexts with more than one variable.

Head Step Lemma

In this section, we will state another important lemma.

Lemma (Head Step). Let \(e, e^* \in \Lambda(\emptyset)\) be any closed terms and suppose that \(\emptyset \vdash e \mathcal{H}_{\mathrm{s}} e^*\). Then:

• if \(e \Downarrow_{\mathrm{s}} (\lambda x . e_0)\) for some variable \(x \in \mathcal{V}\), then there exists an open body \(e^*_0 \in \Lambda(\{x\})\) such that \(e^* \Downarrow_{\mathrm{s}} (\lambda x . e^*_0)\) and \(e_0 \mathcal{H}_{\mathrm{s}} e^*_0\).
• if \(e^* \Downarrow_{\mathrm{v}} (\lambda x . e^*_0)\) for some variable \(x \in \mathcal{V}\), then there exists an open body \(e_0 \in \Lambda(\{x\})\) such that \(e \Downarrow_{\mathrm{s}} (\lambda x . e_0)\) and \(e_0 \mathcal{H}_{\mathrm{s}} e^*_0\).

Proof. See this previous post which proves the lemma in detail.

Extension Lemma

Next, we will show that \(\mathcal{H}_{\mathrm{s}} \le \mathcal{E}_{\mathrm{s}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right)\).

Lemma (Extension). \(\mathcal{H}_{\mathrm{s}} \le \mathcal{E}_{\mathrm{s}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right)\).

Proof. Let \(\Gamma = \{x_1, \dots, x_n\}\) be any context, and suppose \((e,e') \in \left(\mathcal{H}_{\mathrm{s}}\right)_{\Gamma}\). Let \(\sigma \in \mathrm{Env}_{\mathrm{s}}(\Gamma)\) be any closing substitution, i.e.,

\[\sigma = u_1/x_1,\dots,u_n/x_n\]

for closed values \(u_1,\dots,u_n \in \mathrm{Arg}\). Since \(\mathcal{H}_{\mathrm{s}}\) is reflexive, \((u_i, u_i) \in \left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\) for all \(u_i \in \mathrm{Arg}\). Next, we apply the (multivariate) substitution lemma to obtain:

\[(e[u_1/x_1,\dots,u_n/x_n], e'[u_1/x_1,\dots,u_n/x_n]) \in \left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}.\]

Thus, \((e[\sigma], e'[\sigma]) \in \left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\) and, since \(\sigma\) was arbitrary, \((e,e') \in \left(\mathcal{E}_{\mathrm{s}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right)\right)_{\Gamma}\). Since \(\Gamma\) and \((e, e')\) were arbitrary,

\[\mathcal{H}_{\mathrm{s}} \le \mathcal{E}_{\mathrm{s}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right).\]

\(\square\)

Bisimulation Lemma

Next, we will state another key lemma.

Lemma (Bisimulation). The relation \(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\) is an applicative bisimulation, i.e.,

\[\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset} \subseteq \overline{F_{\mathrm{app}}}\left(\left(\mathcal{H}_{\mathrm{s}}\right)_{\emptyset}\right).\]

Proof. See this previous post which proves the lemma in detail.

Contextual Equivalence

Thus, the previous sections establish that applicative bisimulation is indeed a congruence. This establishes that applicative bisimilarity possesses all of the requisite properties of a suitable notion of equivalence, namely, it is an equivalence relation and a congruence.

However, the "gold standard" for term equivalence in the lambda calculus is contextual equivalence. In this section, we will demonstrate that applicative bisimilarity coincides with contextual equivalence (i.e., they are coextensive); however, the advantage of applicative bisimilarity is that it is much more practical to apply than contextual equivalence.

Definition (Syntactic Context). A syntactic context is an element \(c \in \mathrm{Con}\) of the set

\[\mathrm{Con} = \mu F_{\mathrm{ctx}}\]

where

\[\Sigma_c = \{[,\cdot,]\} \cup \Sigma\]

and \(\Sigma\) is the alphabet of the lambda calculus and

\(F_{\mathrm{ctx}} : \mathcal{P}(\Sigma_c^*) \rightarrow \mathcal{P}(\Sigma_c^*)\) is defined as

\begin{align*}F_{\mathrm{ctx}}(C) &= \{[\cdot]\} \\&\cup \{(\lambda x . c) \mid c \in C\} \\&\cup \{(c e) \mid c \in C\} \\&\cup \{(e c) \mid c \in C\}.\end{align*}

We define a function \(\mathrm{Fill} : \mathrm{Con} \times \Lambda \rightarrow \Lambda\) by structural recursion as follows:

\[\mathrm{Fill} = \mu F_{\mathrm{fill}}\]

where the monotone map \(F_{\mathrm{fill}} : \mathcal{P}((\mathrm{Con} \times \Lambda) \times \Lambda) \rightarrow \mathcal{P}((\mathrm{Con} \times \Lambda) \times \Lambda)\) is defined as

\begin{align*}F_{\mathrm{fill}}(R) &= \{(([\cdot], e), e) \mid e \in \Lambda\} \\&\cup \{(((\lambda x . c), e), (\lambda x . c')) \mid ((c, e), c') \in R\} \\&\cup \{(((c e'), e), (c' e')) \mid ((c, e), c') \in R\} \\&\cup \{(((e' c), e), (e' c') \mid ((c, e), c') \in R\}.\end{align*}

Thus, schematically:

• \([\cdot][e] = e\),
• \((\lambda x . c)[e] = (\lambda x . c[e])\),
• \((c e')[e] = (c[e] e')\),
• \((e' c)[e] = (e' c[e])\).

A context is thus an augmented lambda term that contains a unique "hole". This hole can be filled with a lambda term to produce a complete lambda term.

We can now define contextual equivalence. It is analogous to Leibniz' principle of "identity of indiscernables".

Definition (Contextual Equivalence). Contextual equivalence is a relation \(\cong \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) defined as follows:

\[\cong ~=~ \Big\{(e_1, e_2) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \mid \forall C \in \mathrm{Con}\Big(C[e_1] \in \Lambda(\emptyset) \land C[e_2] \in \Lambda(\emptyset) \Rightarrow (C[e_1] \Downarrow ~\Leftrightarrow~ C[e_2] \Downarrow)\Big)\Big\}.\]

We have the following key theorem.

Theorem. Applicative bisimilarity coincides with contextual equivalence, i.e.,

\[\cong ~=~ \sim_{\mathrm{s}}.\]

Proof. See this previous post for a detailed proof.

Thus, in either regime (call-by-value or call-by-name), the respective notion of applicative bisimilarity coincides with contextual equivalence.

Conclusion

Howe's method is an effective method for establishing that applicative bisimulation is a congruence. It is applicable to other problems as well. Howe's method can be applied to "higher-order" languages other than the lambda calculus and to relations other than applicative bisimulation.