Applicative Bisimilarity

In this post we will explore a notion of equivalence between terms in the lambda calculus known as applicative bisimilarity.

Contents

• Syntax
  • Variables
  • Alphabet
  • Strings
  • Terms
  • Variable-Related Functions
  • Substitution
  • Stratification
  • Induction
• Operational Semantics
  • Call-by-Value
  • Call-by-Name
• Bisimilarity
  • LTS Bisimilarity
• Applicative Bisimiliarity
  • Motivation
  • LTS Definition
  • Standard Definition
  • Example
  • Equivalence of Definitions
  • Equivalence Relation
• Contexts
• Congruences
  • Stratification
  • Definition
  • Congruences in the Lambda Calculus
  • Open Congruences
• Howe's Method
  • Motivation
  • Schematic Form
  • Substitution Lemma
  • Head Step Lemma
  • Proof
• Contextual Equivalence

1: Syntax

In this section, we will define the syntax of the lambda calculus.

1a: Variables

We assume the existence of a countably infinite set \(\mathcal{V}\) of variables. It does not matter which set we use, as long as it is countably infinite. By definition, since \(\mathcal{V}\) is denumerable, there exists a function \(v : \mathbb{N} \rightarrow \mathcal{V}\) that witnesses the isomorphism \(\mathbb{N} \cong \mathcal{V}\). Thus, the variables can be written either as \(v(1), v(2), \dots, \) or as \(v_1, v_2, \dots\), etc.

Often, variables are written with metavariables (the symbols that denote particular variables) such as \(x,y,z\), etc. The variables themselves (i.e., the elements of \(\mathcal{V}\) denoted by the metavariables) are particular sets (e.g., \(\{\}\) or \(\{\{\}, \{\{\}\}\}\)).

Thus, we distinguish between variables in the meta-theory (the metavariables) and variables in the object language proper (the elements of \(\mathcal{V}\)).

1b: Alphabet

The alphabet for the lambda calculus is the set \(\Sigma\) defined as

\[\Sigma = \{\lambda, ., (, )\} \cup \mathcal{V},\]

where

• \(\lambda\)
• \(.\)
• \((\)
• \()\)

denote arbitrary sets (which we assume are distinct and not elements of \(\mathcal{V}\)).

1c: Strings

The set \(\Sigma^*\) is the set of all finite sequences of symbols from the alphabet \(\Sigma\). A finite sequence is a function \(a : \{1,\dots, n\} \rightarrow \Sigma\), often denoted \((a_i)_{i=1}^n\), so that the value at index \(i\) is written either as \(a(i)\) or as \(a_i\). Such sequences are called strings of symbols.

Such strings are typically written as string literals, e.g.,

\[(\lambda x . x),\]

etc. Thus, this particular string literal represents the sequence \((a_i)_{i=1}^6\) defined as follows:

• \(a_1 = (\),
• \(a_2 = \lambda\),
• \(a_3 = x\),
• \(a_4 = .\),
• \(a_5 = x\),
• \(a_6 = )\).

In other words, a string literal displays the symbols of a string in order from left to right.

Note that \(\Sigma^*\) includes all strings, including syntactically invalid strings such as

\[\lambda \lambda . x. \lambda (((.\]

We define the concatenation of a string \((a_i)_{i=1}^m\) and a string \((b_i)_{i=1}^n\) as the string \(((ab)_i)_{i=1}^{m+n}\) defined as follows:

\[(ab)_i = \begin{cases} a_i & \text{if } 1 \le i \le m \\ b_{i-m} & \text{if } m+1 \le i \le m+n.\end{cases}\]

The concatenation of a string literal \(s\) and a string literal \(s'\) is written as

\[ss',\]

i.e., as the juxtaposition of the string literals. Thus, for instance, if \(s=(\lambda x . x)\) and \(s' = y\), then \(ss' = (\lambda x . x)y\).

We can also define concatenations involving symbols \(s \in \Sigma\) if we treat the symbols as a singleton sequence, i.e., a sequence \((a_i)_{i=1}^1\) with \(a_1 = s\).

Since concatenation is associative, it does not matter in which order we perform multiple concatenations. Thus, for instance, if \(s=\lambda x . x\), then

\[(s) = (\lambda x.x).\]

1d: Terms

We next inductively define a subset of \(\Sigma^*\) representing the syntactically valid strings. See this post for more information about inductive definitions. We begin by defining a monotone map \(F_{\mathrm{lambda}} : \mathcal{P}(\Sigma^*) \rightarrow \mathcal{P}(\Sigma^*)\) as follows:

\begin{align*}F_{\mathrm{lambda}}(E) &= \mathcal{V} \\&\cup \{(\lambda x . e) \mid x \in \mathcal{V} \land e \in E\} \\&\cup \{(e e') \mid e, e' \in E\}.\end{align*}

We then define the set \(\Lambda\) of lambda terms as the least fixed point \(\mu F_{\mathrm{lambda}}\) of \(F_{\mathrm{lambda}}\):

\[\Lambda = \mu F_{\mathrm{lambda}} .\]

This is often displayed schematically as follows:

\[\frac{x \in \mathcal{V}}{x \in \Lambda},\]

\[\frac{x \in \mathcal{V}, e \in \Lambda}{(\lambda x . e) \in \Lambda},\]

\[\frac{e \in \Lambda, e' \in \Lambda}{(e e') \in \Lambda}.\]

Terms of the form \((\lambda x . e)\) are called abstractions and terms of the form \((ee')\) are called applications.

1e: Variable-Related Functions

Next, we define a few functions related to variables.

All Variables

Next, we define a recursive function \(\mathrm{Var} : \Lambda \rightarrow \mathcal{P}(\mathcal{V})\) that determines the variables of a lambda term as follows:

\begin{align*}F_{\mathrm{var}}(R) &= \{(x, \{x\}) \mid x \in \mathcal{V}\} \\&\cup \{((\lambda x . e), V \cup \{x\}) \mid x \in \mathcal{V} \land (e, V) \in R\} \\&\cup \{(ee', V \cup V') \mid (e, V), (e', V') \in R\},\end{align*}

\[\mathrm{Var} = \mu F_{\mathrm{var}}.\]

Thus:

• the set of variables in a term consisting solely of a single variable \(x\) is, of course, just a singleton set \(\{x\}\) containing the variable itself;
• the set of variables in an abstraction \((\lambda x . e)\) is the bound variable \(x\) together with all variables of \(e\);
• the set of variables in an application \((ee')\) is the set of variables in \(e\) together with the set of variables in \(e'\).

Free Variables

Next, we define a recursive function \(\mathrm{Free} : \Lambda \rightarrow \mathcal{P}(\mathcal{V})\) that determines the free variables of a lambda term (i.e., those variables not bound within the scope of a lambda abstraction) as follows:

\begin{align*}F_{\mathrm{free}}(R) &= \{(x, \{x\}) \mid x \in \mathcal{V}\} \\&\cup \{((\lambda x . e), V \setminus \{x\}) \mid x \in \mathcal{V} \land (e, V) \in R\} \\&\cup \{(ee', V \cup V') \mid (e, V), (e', V') \in R\},\end{align*}

\[\mathrm{Free} = \mu F_{\mathrm{free}}.\]

A lambda term \(e\) is open if \(\mathrm{Free}(e) \ne \emptyset\), and closed if \(\mathrm{Free}(e) = \emptyset\).

Thus:

• the set of free variables in a term consisting solely of a single variable \(x\) is, of course, just the singleton set \(\{x\}\) containing the variable itself;
• the set of free variables in an abstraction \((\lambda x . e)\) is the set of free variables in \(e\) excepting \(x\) since \(x\) is bound in this scope;
• the set of free variables in an application \((ee')\) is the set of free variables in \(e\) together with the set of free variables in \(e'\).

Bound Variables

We define the bound variables by the function

\[\mathrm{Bound}(e) = \mathrm{Var}(e) \setminus \mathrm{Free}(e).\]

Thus, the set of bound variables is simply every variable which is not free. This assumes a dichotomy of free and bound (thus, for instance, the variable \(x\) is considered bound in the term \(\lambda x . y\) even though it does not appear subsequently within the body of the lambda abstraction).

Fresh Variables

We define a function that selects a fresh variable (i.e., any variable not contained within some set \(V \subseteq \mathcal{V}\)) as follows:

\[\mathrm{Fresh}(V) = v\left(\min\{n \in \mathbb{N} \mid v(n) \in \mathcal{V} \setminus V\}\right)\]

where \(v : \mathbb{N} \rightarrow \mathcal{V}\) is the function that witnesses the isomorphism \(\mathcal{V} \cong \mathbb{N}\).

Thus, the function \(\mathrm{Fresh}\) selects the first variable not in the set \(V\), where the ordering is defined by \(v\).

1f: Substitution

Next, we define the substitution of a lambda term for a variable via the following recursive function:

\begin{align*} F_{\mathrm{subst1}}(R) &= \{((e, x, y), y) \mid e \in \Lambda \land x,y \in \mathcal{V} \land x \ne y\} \\ &\cup \{((e, x, x), e) \mid e \in \Lambda \land x \in \mathcal{V}\} \\ &\cup \{((e, x, (\lambda x . e')), (\lambda x . e')) \mid e, e' \in \Lambda \land x \in \mathcal{V}\} \\ &\cup \{((e, x, (\lambda y . e_y)), (\lambda y . e_y')) \mid e, e_y, e_y' \in \Lambda \land x,y \in \mathcal{V} \land x \ne y \land y \notin \mathrm{Free}(e) \land ((e, x, e_y), e_y') \in R\} \\ &\cup \{((e, x, (\lambda y . e_y)), (\lambda z . e_z')) \mid e, e_y, e_z' \in \Lambda \land x,y \in \mathcal{V} \land x \ne y \land y \in \mathrm{Free}(e) \\ &\qquad \land \exists z \in \mathcal{V} \exists e_z \in \Lambda \left( z = \mathrm{Fresh}(\{y\} \cup \mathrm{Free}(e) \cup \mathrm{Free}(e_y)) \land ((z, y, e_y), e_z) \in R \land ((e, x, e_z), e_z') \in R \right)\} \\ &\cup \{((e, x, (e_1 \, e_2)), (e_1' \, e_2')) \mid ((e, x, e_1), e_1') \in R \land ((e, x, e_2), e_2') \in R\},\end{align*}

\[\mathrm{Subst}_1 = \mu F_{\mathrm{subst1}}.\]

The literal notation \(\mathrm{Subst}_1(e, x, e') = e'[e/x]\) is used.

Thus:

• \(x[e/y] = x\) if \(x \ne y\);
• \(x[e/x] = e\);
• \((\lambda x . e')[e/x] = (\lambda x . e')\) (since \(x\) is bound and therefore not subject to substitution);
• \((\lambda y . e')[e/x] = (\lambda y . e'[e/x])\) if \(x \ne y\) and \(y \notin \mathrm{Free}(e)\) where (we can safely avoid a capturing substitution wherein a free variable inadvertently becomes bound);
• \((\lambda y . e')[e/x] = (\lambda z . e'[z/y][e/x])\) if \(x \ne y\) and \(y \in \mathrm{Free}(e)\) where \(z = \mathrm{Fresh}(\{y\} \cup \mathrm{Free}(e) \cup \mathrm{Free}(e'))\) (we must "rename" the bound variable \(y\) to a fresh variable \(z\) to ensure that it does not cause a capturing substitution wherein a free variable inadvertently becomes bound);
• \((e_1 e_2)[e/x] = (e_1[e/x]e_2[e/x])\).

Next, we define the set \(\mathcal{S}\) of substitution lists by induction as follows:

\begin{align*}F_{\mathrm{slist}}(E)(A) &= \{(\{(1, (e, x))\}, \{x\}) \mid e \in E \land x \in \mathcal{V}\} \\&\cup \{(\{(\lvert L \rvert + 1, (e, x))\} \cup L, D \cup \{x\}) \mid (L, D) \in A \land e \in E \land x \notin D\},\end{align*}

\[\mathcal{S}(E) = \mu (F_{\mathrm{slist}}(E)).\]

Thus, a substitution list is a pair \((L, D)\) whose first element \(L\) is an inductively-defined sequence of substitutions (pairs of terms and variables) and whose second element \(D\) is the domain of variables (the set of variables used in the list \(L\)). It is not necessary to define such lists inductively, but it is very useful for defining structurally recursive functions involving substitution lists.

We define the domain of a substitution list \(\sigma = (L, D) \in \mathcal{S}(E)\) as

\[\mathrm{dom}(L, D) = D.\]

We define the set

\[\mathcal{S}(E)(\Gamma) = \{L \mid (L, \Gamma) \in \mathcal{S}(E)\}.\]

We then define multiple substitution via a substitution list as follows:

\begin{align*}F_{\mathrm{subst}}(R) &= \{((\{(1, (e, x))\}, \{x\}), e', \mathrm{Subst}_1(e, x, e')) \mid e, e' \in \Lambda \land x \in \mathcal{V}\} \\ &\cup \{(\{(\lvert L \rvert + 1, (e, x))\} \cup L, D \cup \{x\}), e', \mathrm{Subst}_1(e, x, e'')) \mid ((L, D), e', e'') \in R \land e \in \Lambda \land x \in \mathcal{V}\},\end{align*}

\[\mathrm{Subst} = \mu F_{\mathrm{subst}}.\]

The literal notation

\[e/x = (\{(1, (e, x))\}, \{x\})\]

is used for a singleton substitution list and the literal notation

\[e_1/x_1, \dots, e_n/x_n = (\{(1, (e_1, x_1)), \dots, (n , (e_n, x_n))\}, \{x_1, \dots, x_n\})\]

is used for multiple-substitution lists. For a substitution list \(\sigma \in \mathcal{S}(E)\), the notation

\[e[\sigma] = \mathrm{Subst}(\sigma, e)\]

is used to indicate the corresponding substitution. Likewise, the literal notation

\[\mathrm{Subst}(e_1/x_1, \dots, e_n/x_n, e) = e[e_1/x_1, \dots, e_n/x_n]\]

is used to indicate a multiple substitution. We can summarize multiple substitution schematically as follows:

• \(e'[e/x] = \mathrm{Subst}_1(e,x, e')\),
• \(e[e_1/x_1, \dots, e_{n+1}/x_{n+1}] = (e[e_1/x_1, \dots, e_n/x_n])[e_{n+1}/x_{n+1}]\).

1g: Stratification

It will occasionally be useful to separate the various "constructors" in the lambda calculus (variable, abstraction, and application).

We stratify the syntax of the lambda calculus as follows. We define an index set \(I\) as

\begin{align*}I &= \{(\mathrm{var}, x) \mid x \in \mathcal{V}\} \\&\cup \{(\mathrm{abs}, x) \mid x \in \mathcal{V}\} \\&\cup \{\mathrm{app}\} \end{align*}

for any distinct tag values \(\mathrm{var}, \mathrm{abs}, \mathrm{app}\).

Then, we define maps

\[F_{(\mathrm{var}, x)}(U) = \{x\},\]

\[F_{(\mathrm{abs}, x)}(U) = \{(\lambda x . e) \mid e \in U\},\]

\[F_{\mathrm{app}}(U) = \{(e e') \mid e, e' \in U\}.\]

We note that

\[F_{\mathrm{lambda}} = \bigcup_{i \in I}F_i\]

and furthermore, for all \(U \subseteq \Lambda\) and \(i,j \in I\) such that \(i \ne j\),

\[F_i(U) \cap F_j(U) = \emptyset.\]

1h: Induction

We will exploit structural induction on lambda terms and structural induction on closed lambda terms.

If we want to prove that some property \(P(e)\) holds for all lambda terms \(e \in \Lambda\), then, if we show that

\[F_{\mathrm{lambda}}(A) \subseteq A\]

where

\[A = \{e \in \Lambda \mid P(e)\},\]

then, since \(\Lambda = \mu F_{\mathrm{lambda}}\), i.e. \(\Lambda\) is the least fixed point and therefore least pre-fixed point of \(F_{\mathrm{lambda}}\), it follows that

\[\Lambda \subseteq A\]

and hence, since \(A \subseteq \Lambda\) by construction, it follows that \(\Lambda = A\), i.e., \(P(e)\) holds for all \(e \in \Lambda\).

Explicitly, \(F_{\mathrm{lambda}}(A) \subseteq A\) means the following:

• \(P(x)\) for all \(x \in \mathcal{V}\),
• For all \(x \in \mathcal{V}\), \(P((\lambda x . e))\) whenever \(P(e)\),
• \(P((e_1 e_2))\) whenever \(P(e_1)\) and \(P(e_2)\).

Thus, if we establish these three clauses, then we prove that the property holds for all lambda terms.

We can also perform induction on closed terms \(\Lambda(\emptyset)\) if we define the set of closed terms inductively as follows:

\begin{align*}F_{\mathrm{closed}}(A) &= \{(\lambda x . e) \mid x \in \mathcal{V} \land e \in \Lambda(\{x\})\} \\&\cup \{(e_1 e_2) \mid e_1, e_2 \in A\},\end{align*}

\[\Lambda(\{x\}) = \{e \in \Lambda \mid \mathrm{Free}(e) = \{x\}\},\]

\[\Lambda(\emptyset) = \mu F_{\mathrm{closed}}.\]

Explicitly, if

\[A = \{e \in \Lambda \mid P(e)\},\]

then \(F_{\mathrm{closed}}(A) \subseteq A\) means the following:

• \(P((\lambda x . e))\) for all \(x \in \mathcal{V}\) and \(e \in \Lambda(\{x\})\),
• \(P((e_1 e_2))\) whenever \(P(e_1)\) and \(P(e_2)\).

Thus, if we establish these two clauses, then we prove that the property holds for all closed lambda terms.

2: Operational Semantics

Next, we will describe the (big step) operational semantics of the lambda calculus.

2a: Call-By-Value Evaluation

The call-by-value reduction strategy reduces arguments in applications prior to substitution within the applicand.

We first define the subset \(V \subseteq \Lambda\) of "values" of the lambda calculus.

\[V = \mathcal{V} \cup \{(\lambda x . e) \mid x \in \mathcal{V} \land e \in \Lambda\}.\]

These are the terms that constitute "values" (they are variables or lambda abstractions).

For any finite set of variables \(\bar{x} \in \mathcal{P}_f(\mathcal{V})\), we define the following sets:

\[\Lambda(\bar{x}) = \{e \in \Lambda \mid \mathrm{Free}(e) \subseteq \bar{x}\},\]

\[V(\bar{x}) = \{v \in V \mid \mathrm{Free}(v) \subseteq \bar{x}\}.\]

These sets represent terms or values, respectively, whose free variables belong to some set. Note that the set of closed terms is precisely \(\Lambda(\emptyset)\) and the set of closed values is precisely \(V(\emptyset)\).

We next define a relation \(\Downarrow_{\mathrm{v}} \subseteq \Lambda(\emptyset) \times V(\emptyset)\) by structural recursion as follows:

\begin{align*}F_{\mathrm{cbv}}(R) &= \{(v,v) \mid v \in V(\emptyset)\} \\&\cup \{((e_1 e_2), v') \mid \exists x \in \mathcal{V} \exists e \in \Lambda\exists v \in V(\emptyset) \left((e_1, (\lambda x . e)) \in R \land (e_2, v) \in R \land (e[v/x], v') \in R\right)\},\end{align*}

\[\Downarrow_{\mathrm{v}} = \mu F_{\mathrm{cbv}}.\]

This is often displayed schematically as follows:

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

\[\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'}.\]

The first rule indicates that evaluation is idempotent with respect to values, i.e., every value evaluates to itself. The second rule indicates that the applicand (i.e., the left-hand side \(e_1\) of an application \((e_1 e_2)\)) must be evaluated and additionally the argument (i.e., the right-hand side \(e_2\)) must be evaluated prior to performing a substitution. It is the latter property (namely, that the argument must be evaluated prior to substitution) that distinguishes the call-by-value reduction strategy.

Not all lambda terms have a value under call-by-value evaluation. For instance, consider the term

\[(\lambda x . x x)(\lambda x. x x).\]

This term reduces to itself after application, and, since it is not already value, it will never evaluate to any value.

2b: Call-By-Name Evaluation

The call-by-name evaluation strategy reduces the applicand but immediately substitutes the argument without reducing it.

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

\begin{align*}F_{\mathrm{cbn}}(R) &= \{(v, v) \mid v \in \mathcal{V}(\emptyset)\} \\&\cup \{((e_1, e_2), e_3) \mid \exists x \in \mathcal{V} \exists e \in \Lambda \left((e_1, (\lambda x . e)) \in R \land (e[e_2/x], e_3) \in R\right)\},\end{align*}

\[\Downarrow_{\mathrm{n}} = \mu F_{\mathrm{cbn}}.\]

This is often displayed schematically as follows:

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

\[\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}.\]

The first rule again expresses the idempotency of evaluation. The second rule indicates that the applicand \(e_1\) of an application \((e_1 e_2)\) must be evaluated, yet the argument \(e_2\) is substituted without being reduced.

Not all lambda terms have a value under call-by-name evaluation. For instance, consider the term

\[(\lambda x . x x)(\lambda x. x x).\]

3: Bisimilarity

In this section, we will review the definition of bisimilarity.

3a: LTS Bisimilarity

In this section, we will consider labeled transition systems and their attendant notion of bisimilarity.

Definition (Labeled Transition System - LTS). A labeled transition system (LTS) is a triple \((S, L, \rightarrow)\) consisting of a set \(S\) of states a set \(L\) of labels and a relation \(\rightarrow \subseteq S \times L \times S\) called the transition relation. We write

\[s \xrightarrow{l} s'\]

as an abbreviation for \((s, l, s') \in \rightarrow\) to indicate that state \(s\) transitions to state \(s'\) under label \(l\).

Definition (LTS Bisimulation). Let \((S, L, \rightarrow)\) be a labeled transition system. The LTS bisimulation operator is the monotone map \(F_{\mathrm{lts}} : \mathcal{P}(S \times S) \rightarrow \mathcal{P}(S \times S)\) defined as

\[F_{\mathrm{lts}}(R) = \left\{ (s_1, s_2) \in S \times S \ \middle\vert{}\ \begin{aligned} &\forall l \in L, \forall s_1', \big( s_1 \xrightarrow{l} s_1' \implies \exists s_2', \, s_2 \xrightarrow{l} s_2' \land (s_1', s_2') \in R \big) \\ &\quad \land \\ &\forall l \in L, \forall s_2', \big( s_2 \xrightarrow{l} s_2' \implies \exists s_1', \, s_1 \xrightarrow{l} s_1' \land (s_1', s_2') \in R \big) \end{aligned} \right\}\]

which acts on the complete lattice \((\mathcal{P}(S \times S), \subseteq)\). An LTS bisimulation is a post-fixed point of the LTS bisimulation operator, i.e., a relation \(R \subseteq S \times S\) such that

\[R \subseteq F_{\mathrm{lts}}(R).\]

Definition (LTS Bisimilarity). Let \((S, L, \rightarrow)\) be a labeled transition system. LTS bisimilarity is the greatest post-fixed point \(\sim = \nu F_{\mathrm{lts}}\), which, by the Tarski-Knaster theorem, is defined as

\[\nu F_{\mathrm{lts}} = \bigcup \{R \subseteq S \times S \mid R \subseteq F_{\mathrm{lts}}(R)\}.\]

4: Applicative Bisimilarity

In this section, we will introduce the notion of applicative bisimilarity.

4a: Motivation

Our object is to determine when two lambda terms are "equivalent" in some appropriate sense.

Consider the following example (note that we will omit certain parentheses when writing expressions informally, but parentheses are always part of the formal expressions):

• \(\mathrm{one} \equiv \lambda s . \lambda z . s z\),
• \(\mathrm{two} \equiv \lambda s . \lambda z . s (s z)\),
• \(\mathrm{succ} \equiv \lambda n . \lambda s . \lambda z . s ((n s) z)\).

This example represents the Church encoding of the natural numbers \(1\) and \(2\) and the successor function \(n \mapsto n + 1\). We would expect one of the most elementary of all mathematical propositions to be represented faithfully, namely:

\[1 + 1 = 2.\]

However, it is not the case when using call-by-value evaluation that

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

In the latter expression, the \(=\) indicates syntactic identity, namely, that the two terms are the very same sequence of symbols. According to call-by-value evaluation,

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

and yet this is not syntactically identical to \(\mathrm{two}\). If we reduce the inner application, namely,

\[(((\lambda s . (\lambda z . (s z))) s) z) \mapsto (sz)\]

we do indeed recover the term \(\mathrm{two}\). However, with call-by-value evaluation, the lambda abstraction is already considered a "value" and hence the evaluation stops.

With call-by-name evaluation, since the argument \(\mathrm{one}\) was already a value, the evaluation is the same as the call-by-value evaluation.

So, clearly, syntactic identity is completely unacceptable.

We might propose strict extensionality instead, namely, that two lambda terms are equivalent if they both evaluate to syntactically identical terms (or else both diverge) for all argument values. However, this would fail to equate

\[(\lambda x . (\mathrm{succ}~\mathrm{one}))\]

and

\[(\lambda x . (\mathrm{two})).\]

These represent the constant functions \(x \mapsto 1 + 1\) and \(x \mapsto 2\), respectively. Thus, no matter how we apply these abstractions, they evaluate to terms that are not syntactically identical. We don't expect a strict notion of extensionality to work for an intensional calculus like the lambda calculus.

However, we could amend our requirement such that we only require a weak extensionality, i.e., two lambda terms are equivalent if they both evaluate to equivalent terms (or else both diverge) for all argument values. This cannot serve as a definition since it is circular. However, it does represent a valid property of relations. We can escape the circularity by defining our equivalence relation as the greatest relation satisfying this property. In other words, we seek a coinductive characterization of term equivalence. This brings us to the definitions in the next section.

4b: LTS Definition

First, we will define a labeled transition system for the lambda calculus.

Definition (Call-by-Value Lambda Calculus LTS). The call-by-value lambda calculus LTS is the LTS \((\Lambda(\emptyset), V(\emptyset), \rightarrow_{\lambda})\), where

\[e_1 \xrightarrow{v}_{\lambda} e_2 \Leftrightarrow \exists e_1' \in \Lambda(\{x\})(e_1 \Downarrow_{\mathrm{v}} (\lambda x . e_1') \land e_2 = e_1'[v/x]).\]

Definition (Call-by-Name Lambda Calculus LTS). The call-by-name lambda calculus LTS is the LTS \((\Lambda(\emptyset), \Lambda(\emptyset), \rightarrow_{\lambda})\), where

\[e_1 \xrightarrow{e}_{\lambda} e_2 \Leftrightarrow \exists e_1' \in \Lambda(\{x\})(e_1 \Downarrow_{\mathrm{n}} (\lambda x . e_1') \land e_2 = e_1'[e/x]).\]

Next, we will define applicative bisimilarity.

Definition (Applicative Bisimilarity - LTS). A relation \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) is a call-by-value LTS applicative bisimulation if it is an LTS applicative bisimulation with respect to the call-by-value lambda calculus LTS, and is a call-by-name LTS applicative bisimulation if it is an LTS applicative bisimulation with respect to the call-by-name lambda calculus LTS. Explicitly:

\[R \subseteq F_{\lambda}(R),\]

where

\[F_{\lambda}(R) = \left\{ (e_1, e_2) \ \middle\vert{}\ \begin{aligned} &\forall v \in \mathrm{Arg}, \forall e_1'', \big( e_1 \xrightarrow{v}_\lambda e_1'' \implies \exists e_2'', \, e_2 \xrightarrow{v}_\lambda e_2'' \land (e_1'', e_2'') \in R \big) \\ &\quad \land \\ &\forall v \in \mathrm{Arg}, \forall e_2'', \big( e_2 \xrightarrow{v}_\lambda e_2'' \implies \exists e_1'', \, e_1 \xrightarrow{v}_\lambda e_1'' \land (e_1'', e_2'') \in R \big) \end{aligned} \right\},\]

where \(\mathrm{Arg} = V(\emptyset)\) and \(\Downarrow = \Downarrow_{\mathrm{v}}\) for call-by-value semantics, and \(\mathrm{Arg} = \Lambda(\emptyset)\) and \(\Downarrow = \Downarrow_{\mathrm{n}}\) for call-by-name semantics.

The greatest call-by-value LTS applicative bisimulation is called call-by-value LTS applicative bisimilarity and is defined as LTS bisimilarity for the call-by-value lambda calculus LTS. The greatest call-by-name LTS applicative bisimulation is called call-by-name LTS applicative bisimilarity and is defined as LTS bisimilarity for the call-by-name lambda calculus LTS.

Explicitly:

\[e_1 \sim e_2 \iff \left( \begin{aligned} &\forall v \in \mathrm{Arg}, \forall e_1'', \left( e_1 \xrightarrow{v}_\lambda e_1'' \implies \exists e_2'', \, e_2 \xrightarrow{v}_\lambda e_2'' \land e_1'' \sim e_2'' \right) \\ &\quad \land \\ &\forall v \in \mathrm{Arg}, \forall e_2'', \left( e_2 \xrightarrow{v}_\lambda e_2'' \implies \exists e_1'', \, e_1 \xrightarrow{v}_\lambda e_1'' \land e_1'' \sim e_2'' \right) \end{aligned} \right)\]

where \(\mathrm{Arg} = V(\emptyset)\) and \(\Downarrow = \Downarrow_{\mathrm{v}}\) for call-by-value semantics, and \(\mathrm{Arg} = \Lambda(\emptyset)\) and \(\Downarrow = \Downarrow_{\mathrm{n}}\) for call-by-name semantics.

4c: Standard Definition

Next, we state the standard definition of applicative bisimilarity, which does not invoke any LTS.

Definition (Applicative Bisimilarity - Standard). A relation \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) is a call-by-value applicative bisimulation if it is a post-fixed point of the map

\[F_{\mathrm{app,v}}(R) = \left\{(e_1, e_2) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \,\middle|\, \begin{aligned} &\forall x \in \mathcal{V} \forall e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{v}} (\lambda x . e_1') \Rightarrow \exists e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{v}} (\lambda x . e_2') \land \forall v \in V(\emptyset) (e_1'[v/x] ~R~ e_2'[v/x]))) \\ &\land \\ &\forall x \in \mathcal{V} \forall e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{v}} (\lambda x . e_2') \Rightarrow \exists e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{v}} (\lambda x . e_1') \land \forall v \in V(\emptyset) (e_1'[v/x] ~R~ e_2'[v/x]))) \end{aligned}\right\}.\]

Call-by-value applicative bisimilarity is the greatest post-fixed point of the map \(F_{\mathrm{app,v}}\), which, by the Tarski-Knaster theorem, is also the greatest fixed point of \(F_{\mathrm{app,v}}\) and is defined as

\[\sim_{\mathrm{v}} = \nu F_{\mathrm{app,v}} = \bigcup\{R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset) \mid R \subseteq F_{\mathrm{app,v}}(R)\}.\]

Thus, \(e_1 \sim_{\mathrm{v}} e_2\) if and only if there exists a call-by-value applicative bisimulation \(R\) such that \(e_1 R e_2\). Additionally,

\[e_1 \sim_{\mathrm{v}} e_2 \Leftrightarrow \begin{aligned} &\forall x \in \mathcal{V} \forall e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{v}} (\lambda x . e_1') \Rightarrow \exists e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{v}} (\lambda x . e_2') \land \forall v \in V(\emptyset) (e_1'[v/x] \sim_{\mathrm{v}} e_2'[v/x]))) \\ &\land \\ &\forall x \in \mathcal{V} \forall e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{v}} (\lambda x . e_2') \Rightarrow \exists e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{v}} (\lambda x . e_1') \land \forall v \in V(\emptyset) (e_1'[v/x] \sim_{\mathrm{v}} e_2'[v/x]))) \end{aligned}.\]

Likewise, a relation \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) is a call-by-name applicative bisimulation if it is a post-fixed point of the map

\[F_{\mathrm{app,n}}(R) = \left\{(e_1, e_2) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \,\middle|\, \begin{aligned} &\forall x \in \mathcal{V} \forall e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{n}} (\lambda x . e_1') \Rightarrow \exists e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{n}} (\lambda x . e_2') \land \forall e \in \Lambda(\emptyset) (e_1'[e/x] ~R~ e_2'[e/x]))) \\ &\land \\ &\forall x \in \mathcal{V} \forall e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{n}} (\lambda x . e_2') \Rightarrow \exists e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{n}} (\lambda x . e_1') \land \forall e \in \Lambda(\emptyset) (e_1'[e/x] ~R~ e_2'[e/x]))) \end{aligned}\right\}.\]

Call-by-name applicative bisimilarity is the greatest post-fixed point of the map \(F_{\mathrm{app,n}}\), which, by the Tarski-Knaster theorem, is also the greatest fixed point of \(F_{\mathrm{app,n}}\) and is defined as

\[\sim_{\mathrm{n}} = \nu F_{\mathrm{app,n}} = \bigcup\{R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset) \mid R \subseteq F_{\mathrm{app,n}}(R)\}.\]

Thus, \(e_1 \sim_{\mathrm{n}} e_2\) if and only if there exists a call-by-name applicative bisimulation \(R\) such that \(e_1 R e_2\). Additionally,

\[e_1 \sim_{\mathrm{n}} e_2 \Leftrightarrow \begin{aligned} &\forall x \in \mathcal{V} \forall e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{n}} (\lambda x . e_1') \Rightarrow \exists e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{n}} (\lambda x . e_2') \land \forall e \in \Lambda(\emptyset) (e_1'[e/x] \sim_{\mathrm{n}} e_2'[e/x]))) \\ &\land \\ &\forall x \in \mathcal{V} \forall e_2' \in \Lambda (e_2 \Downarrow_{\mathrm{n}} (\lambda x . e_2') \Rightarrow \exists e_1' \in \Lambda (e_1 \Downarrow_{\mathrm{n}} (\lambda x . e_1') \land \forall e \in \Lambda(\emptyset) (e_1'[e/x] \sim_{\mathrm{n}} e_2'[e/x]))) \end{aligned}.\]

Note that the difference between the various definitions for the call-by-value and call-by-name evaluation strategies is that the former use values \(V(\emptyset)\) for substitutions whereas the latter uses arbitrary closed terms \(\Lambda(\emptyset)\) and, of course, the former uses \(\Downarrow_{\mathrm{v}}\) whereas the latter uses \(\Downarrow_{\mathrm{n}}\).

4d: Example

Next, we will give a simple example of applicative bisimilarity. We want to show that

\[(\mathrm{succ}~\mathrm{one}) \sim_{\mathrm{v}} \mathrm{two},\]

i.e., that

\[((\lambda n . (\lambda s . (\lambda z . (s ((n s) z))))) (\lambda s . (\lambda z . (s z)))) \sim (\lambda s . (\lambda z . (s z))).\]

To show this, we must exhibit a call-by-value applicative bisimulation \(R\) such that

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

Consider the following relation:

\[R = \{(\mathrm{succ}~\mathrm{one}, \mathrm{two})\} \cup \{(e, e) \mid e \in \Lambda(\emptyset)\}.\]

We make the following definitions:

• \(e_1 = ((\lambda n . (\lambda s . (\lambda z . (s ((n s) z))))) (\lambda s . (\lambda z . (s z))))\),
• \(e_2 = (\lambda s . (\lambda z . (s z)))\),
• \(e_1' = (\lambda s . (\lambda z . (s (((\lambda s . (\lambda z . (s z))) s) z))))\),
• \(e_2' = (\lambda z . (s (s z)))\),
• \(e_1 \Downarrow_{\mathrm{v}} (\lambda s . e_1')\),
• \(e_2 \Downarrow_{\mathrm{v}} (\lambda s . e_2')\).

We thus need to show that, for every \(v_s \in V(\emptyset)\),

\[e_1'[v_s/s] ~R~ e_2'[v_s/s].\]

We make the following definitions:

• \(e_3 = e_1'[v_s/s] = (\lambda z . (v_s (((\lambda s . (\lambda z . (s z))) v_s) z)))\),
• \(e_4 = e_2'[v_s/s] = (\lambda z . (v_s (v_s z)))\),
• \(e_3' = (v_s (((\lambda s . (\lambda z . (s z))) v_s) z))\),
• \(e_4' = (v_s (v_s z))\),
• \(e_3 \Downarrow_{\mathrm{v}} (\lambda z . e_3')\),
• \(e_4 \Downarrow_{\mathrm{v}} (\lambda z . e_4')\).

We thus need to show that, for every \(v_z \in V(\emptyset)\),

\[e_3'[v_z/z] ~R~ e_4'[v_z/z].\]

We make the following definitions:

• \(e_5 = e_3'[v_z/z] = (v_s (((\lambda s . (\lambda z . (s z))) v_s) v_z))\),
• \(e_6 = e_4'[v_z/z] = (v_s (v_s v_z))\).

Now, suppose that \(e_5 \Downarrow_{\mathrm{v}} (\lambda x . e)\).

By the definition of \(\Downarrow_{v}\), it follows that \(e_5 \Downarrow_{\mathrm{v}} (\lambda x . e)\) if and only if \((v_s (v_s v_z)) \Downarrow_{\mathrm{v}} (\lambda x . e)\) since \((v_s (v_s v_z))\) is an intermediate reduction of \(e_5\). Thus, \(e_6 \Downarrow_{\mathrm{v}} (\lambda x . e)\). Then, for any value \(v \in V(\emptyset)\),

\[e[v/x] ~R~ e[v/x]\]

by construction of \(R\). Thus, we have shown that

\[((\mathrm{succ}~ \mathrm{one}), \mathrm{two}) \in F_{\mathrm{app,v}}(R).\]

It is trivially the case that \((e, e) \in F_{\mathrm{app,v}}(R)\) for all pairs \((e, e) \in R\) where \(e \in \Lambda(\emptyset)\). Thus,

\[R \subseteq F_{\mathrm{app,v}}(R),\]

i.e., \(R\) is an applicative bisimulation.

4e: Equivalence of Definitions

In this section, we will prove that LTS applicative bisimilarity and standard applicative bisimilarity are equivalent. We do so by proving that the monotone maps that define them are equal, which then implies that the notions of bisimulation and bisimilarity defined by them coincide.

Theorem. \(F_{\lambda} = F_{\mathrm{app}}\).

Proof. Let \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\).

(\(\subseteq\)). Suppose \((e_1, e_2) \in F_{\lambda}(R)\). Suppose \(e_1 \Downarrow (\lambda x . e_1')\). For any \(v \in \mathrm{Arg}\), \(e_1 \xrightarrow{v}_{\lambda} e_1'[v/x]\). By definition of \(F_{\lambda}\), there exists some \(e_2''\) such that \(e_2 \xrightarrow{v}_{\lambda} e_2''\) and \((e_1'[v/x], e_2'') \in R\). By definition of \(\rightarrow_{\lambda}\), \(e_2 \Downarrow (\lambda x . e_2')\) and \(e_2'' = e_2'[v/x]\) (note that we can always arrange for the bound variable to be \(x\) by alpha conversion). Thus, \((e_1'[v/x], e_2'[v/x]) \in R\). A symmetric argument shows that if \(e_2 \Downarrow (\lambda x . e_2')\), then \((e_1'[v/x], e_2'[v/x]) \in R\). Thus, \((e_1, e_2) \in F_{\mathrm{app}}(R)\).

(\(\supseteq\)). Suppose \((e_1, e_2) \in F_{\mathrm{app}}(R)\). Let \(v \in \mathrm{Arg}\) and \(e_1'' \in \Lambda(\emptyset)\) and suppose \(e_1 \xrightarrow{v}_{\lambda} e_1''\). Then, by definition of \(\rightarrow_{\lambda}\), there exists a variable \(x \in \mathcal{V}\) and a term \(e_1' \in \Lambda\) such that \(e_1 \Downarrow (\lambda x . e_1')\) and \(e_1'' = e_1'[v/x]\). By definition of \(F_{\mathrm{app}}\), there exists an \(e_2' \in \Lambda\) such that \(e_2 \Downarrow (\lambda x .e_2')\) and \((e_1'[v/x], e_2'[v/x]) \in R\) for all \(v \in \mathrm{Arg}\). Thus, \((e_1'', e_2'') \in R\), and, by definition of \(\rightarrow_{\lambda}\), this means that \(e_2 \xrightarrow{v}_{\lambda} e_2''\). A symmetric argument shows that \(e_2 \xrightarrow{v}_{\lambda} e_2''\) implies that \((e_1'', e_2'') \in R\) and \(e_1 \xrightarrow{v}_{\lambda} e_1''\). Thus, \((e_1, e_2) \in F_{\lambda}(R)\).

\(\square\)

4f: Equivalence Relation

In this section, we will prove that applicative bisimilarity is an equivalence relation.

Reflexivity

We proceed by coinduction. We will show that the set

\[\mathrm{id} = \{(e, e) \mid e \in \Lambda(\emptyset)\}\]

is an applicative bisimulation. Since applicative bisimilarity is the greatest applicative bisimulation, this implies that \(\mathrm{id} \subseteq \sim\), i.e., that \(\sim\) is reflexive.

Suppose that \((e_1, e_2) \in \mathrm{id}\). Then, by definition, \(e_1 = e_2\). Let \(x \in \mathcal{V}\) and \(e_1' \in \Lambda\) and suppose that \(e_1 \Downarrow (\lambda x . e_1')\). Then, since \(e_1 = e_2\), \(e_2 \Downarrow (\lambda x . e_2')\) where \(e_1' = e_2'\). Suppose \(v \in \mathrm{Arg}\). Then, since \(e_1'[v/x] = e_2'[v/x]\), it follows that \((e_1'[v/x], e_2'[v/x]) \in \mathrm{id}\). A symmetric argument shows that, if \(e_2 \Downarrow (\lambda x . e_2')\), then \(e_1 \Downarrow (\lambda x . e_1')\) and \((e_1'[v/x], e_2'[v/x]) \in \mathrm{id}\). Thus, \((e_1, e_2) \in F_{\mathrm{app}}(\mathrm{id})\) and so \(\mathrm{id} \subseteq F_{\mathrm{app}}(\mathrm{id})\) and \(\mathrm{id}\) is an applicative bisimulation. Since \(\sim\) is the greatest such bisimulation, \(\mathrm{id} \subseteq \sim\) and \(\sim\) is reflexive.

Symmetry

We proceed by coinduction. We will show that the set

\[S = \{(e_1, e_2) \mid e_2 \sim e_1\}\]

is an applicative bisimulation.

Suppose that \((e_1, e_2) \in S\). Then, by definition, \(e_2 \sim e_1\). Let \(x \in \mathcal{V}\) and \(e_1' \in \Lambda\) and suppose that \(e_1 \Downarrow (\lambda x . e_1')\). Since \(e_2 \sim e_1\), by definition, there exists an \(e_2' \in \Lambda\) such that \(e_2 \Downarrow (\lambda x . e_2')\) and \(e_2'[v/x] \sim e_1'[v/x]\) for all \(v \in \mathrm{Arg}\). By definition of \(S\), it follows that \((e_1'[v/x], e_2'[v/x]) \in S\). A symmetric argument shows that if \(e_2 \Downarrow (\lambda x . e_2')\), then there exists an \(e_1'\) such that \(e_1 \Downarrow (\lambda x . e_1')\) and \((e_1'[v/x], e_2'[v/x]) \in S\) for all \(v \in \mathrm{Arg}\). Thus, \((e_1, e_2) \in F_{\mathrm{app}}(S)\) and \(S \subseteq F_{\mathrm{app}}(S)\) and \(\mathrm{S}\) is an applicative bisimulation. Since \(\sim\) is the greatest such bisimulation, \(\mathrm{S} \subseteq \sim\) and hence \(\sim\) is symmetric.

Transitivity

We proceed by coinduction. We will show that the set

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

is an applicative bisimulation.

Suppose that \((e_1, e_3) \in T\). Then, by definition, there exists an \(e_2 \in \Lambda(\emptyset)\) such that \(e_1 \sim e_2\) and \(e_2 \sim e_3\). Let \(x \in \mathcal{V}\) and \(e_1' \in \Lambda\) and suppose that \(e_1 \Downarrow (\lambda x . e_1')\). Since \(e_1 \sim e_2\), by definition, there exists an \(e_2' \in \Lambda\) such that \(e_2 \Downarrow (\lambda x . e_2')\) and \((e_1'[v/x] \sim e_2'[v/x]\) for all \(v \in \mathrm{Arg}\). Similiarly, since \(e_2 \sim e_3\), by definition, there exists an \(e_3' \in \Lambda\) such that \(e_2 \Downarrow (\lambda x . e_3')\) and \(e_2'[v/x] \sim e_3'[v/x]\) for all \(v \in \mathrm{Arg}\). Since \(e_1'[v/x] \sim e_2'[v/x]\) and \(e_2'[v/x] \sim e_3'[v/x]\), by definition of \(T\), it follows that \((e_1'[v/x], e_3'[v/x]) \in T\). A symmetric argument shows that if \(e_3 \Downarrow (\lambda x . e_3')\), then there exists an \(e_1' \in \Lambda\) such that \(e_1 \Downarrow (\lambda x . e_1')\) and \((e_1'[v/x] \sim e_3'[v/x])\) for all \(v \in \mathrm{Arg}\). Hence \((e_1, e_3) \in F_{\mathrm{app}}(T)\) and \(T \subseteq F_{\mathrm{app}}(T)\) so \(T\) is an applicative bisimulation. Since \(\sim\) is the greatest bisimulation, \(T \subseteq \sim\) and hence \(\sim\) is transitive.

5: Contexts

We define a context as a finite set \(\Gamma\) of variables, i.e.,

\[\Gamma \in \mathcal{P}_f(\mathcal{V}).\]

The set of all contexts is denoted \(\mathcal{C}\) and defined as

\[\mathcal{C} = \mathcal{P}_f(\mathcal{V}).\]

We then define a context-indexed relation lattice of lambda terms as follows:

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

An element \(\mathcal{R} \in \mathcal{L}\) is a function \(\mathcal{R} : \mathcal{C} \rightarrow \mathcal{P}(\Lambda(\Gamma) \times \Lambda(\Gamma))\) and we often write \(\mathcal{R}_{\Gamma}\) for \(\mathcal{R}(\Gamma)\).

The appropriate notion of order in the lattice \(\mathcal{L}\) is the "fiberwise" subset relation defined as

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

We then define the call-by-value extension of a relation \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) on closed lambda terms as \(\mathcal{E}_{\mathrm{v}}(R)\), where the call-by-value extension operator \(\mathcal{E}_{\mathrm{v}} : \mathcal{P}(\Lambda(\emptyset) \times \Lambda(\emptyset)) \rightarrow \mathcal{L}\) is defined as

\[\mathcal{E}_{\mathrm{v}}(R) = \{(e, e') \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid \forall \sigma \in \mathcal{S}(V(\emptyset), \Gamma) . e[\sigma] ~R~ e'[\sigma]\}.\]

Likewise, we define the call-by-name extension of a relation \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) on closed lambda terms as \(\mathcal{E}_{\mathrm{n}}(R)\), where the call-by-name extension operator \(\mathcal{E}_{\mathrm{n}} : \mathcal{P}(\Lambda(\emptyset) \times \Lambda(\emptyset)) \rightarrow \mathcal{L}\) is defined as

\[\mathcal{E}_{\mathrm{n}}(R)_{\Gamma} = \{(e, e') \in \Lambda(\Gamma) \times \Lambda(\Gamma) \mid \forall \sigma \in \mathcal{S}(\Lambda(\emptyset), \Gamma) . e[\sigma] ~R~ e'[\sigma]\}.\]

The only difference is that the former uses closed values whereas the latter uses closed terms.

Note that, since applicative bisimulation is an equivalence relation, its open extension \(\mathcal{E}(\sim)\) is likewise an equivalence relation.

6: Congruences

Next, we will establish that applicative bisimilarity is a congruence, i.e., that bisimilar terms can be substituted for one another in expressions while preserving bisimilarity.

6a: Stratification

Here we make a few preliminary definitions.

Definition (Stratifiable Map). A monotone map \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) for a set \(X\) is stratifiable if it can be partitioned into disjoint sub-maps \(\{F_i\}_{i \in I}\) for some tag set \(I\) such that

\[F = \bigcup_{i \in I}F_i\]

and for all \(U \subseteq X\) and \(V \subseteq Y\)

\[F_i(U) \cap F_j(U) = \emptyset \text{ when } i \ne j.\]

Definition (Stratified Relational Lifting). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be a stratifiable map. Let \(R \subseteq X \times X\) be any relation. The stratified relational lifting of \(R\) with respect to \(F\) is the map \(\overline{F} : \mathcal{P}(X \times X) \rightarrow \mathcal{P}(X \times X)\) defined as follows:

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

This stratification along \(F_i\) ensures that the relation cannot "mix" terms that arise from distinct "rules" (e.g., a lambda abstraction and an application). This is often essential in proofs (where we exploit this property to ensure that terms of the left-hand side of a relation are of the same structure as terms on the right-hand side of the relation).

6b: Definition

This brings us to the following definition.

Definition (Congruence). Let \(X\) be any set and \(F : \mathcal{P}(X) \rightarrow \mathcal{P}(X)\) be any stratified map. A relation \(R \subseteq X \times X\) is a congruence (or congruence relation) if it is a pre-fixed point of the relational lifting \(\overline{F}\), i.e.,

\[\overline{F}(R) \subseteq R.\]

In fact, if we dualize this definition (i.e., if we take a post-fixed point), we obtain a notion of (stratified) bisimulation. Thus, congruences and bisimulations are dual concepts.

6c: Congruences in the Lambda Calculus

Next, we will determine the form of congruences in the lambda calculus. We make use of the stratification of the lambda calculus.

We have the following theorem.

Theorem. For any relation \(R \subseteq \Lambda \times \Lambda\), \(R\) is a congruence relation, i.e., \(\underline{F_{\mathrm{lambda}}}(R) \subseteq R\), if and only if \(R\) is closed under the following conditions:

1. \(x R x\) for all \(x \in \mathcal{V}\),
2. \((\lambda x . e) ~R~ (\lambda x . e')\) whenever \(eRe'\) for all \(x \in \mathcal{V}\) and \(e,e' \in \Lambda\),
3. \((e_1 e_2) ~ R ~ (e_1'e_2')\) whenever \(e_1Re_1'\) and \(e_2Re_2'\) for all \(e_1, e_1', e_2, e_2' \in \Lambda\).

Proof. (If). Suppose that \(R\) is closed under these conditions. Suppose that \((M,N) \in \overline{F_{\mathrm{lambda}}}(R)\). By canonicity, there are three possibilities for \(M\).

Case 1: \(M = x\) for \(x \in \mathcal{V}\). We choose \(U = \emptyset\). Since \(F_{(\mathrm{var}, x)}(U) = \{x\}\), it follows that \(M \in F_{(\mathrm{var}, x)}(U)\) and hence \(N \in F_{(\mathrm{var}, x)}(R[U]) = \{x\}\) so \(N = x\). A symmetric argument for \(V = \emptyset\) also shows that \(M = x\) whenever \(N = x\). By condition 1, \(xRx\).

Case 2: \(M = (\lambda x . e)\) for \(x \in \mathcal{V}\) and \(e \in \Lambda\). We choose \(U = \{e\}\). Since \(\{(\lambda x . e)\} = F_{(\mathrm{abs},x)}(U)\), it follows that \(M \in F_{(\mathrm{abs}, x)}(U)\), so \(N \in F_{(\mathrm{abs}, x)}(R[U])\), which means that there exists an \(e' \in \Lambda\) such that \(eRe'\) and \(N = (\lambda x . e')\). By condition 2, \((\lambda x . e) ~R~ (\lambda x . e')\). A symmetric argument for \(V = \{e'\}\) also shows that \(M = (\lambda x . e)\) and \(eRe'\) whenever \(N = (\lambda x . e')\) and hence \((\lambda x . e) ~R~ (\lambda x . e')\).

Case 3: \(M = (e_1 e_2)\) for \(e_1, e_2 \in \Lambda\). We choose \(U = \{e_1, e_2\}\). Since \(\{(e_1 e_2)\} \subseteq F_{\mathrm{app}}(U)\), it follows that \(M \in F_{\mathrm{app}}(U)\), so \(N \in F_{\mathrm{app}}(R[U])\), which means that there exists \(e_1', e_2' \in \Lambda\) such that \(e_1 R e_1'\) and \(e_2 R e_2'\) and \(N = (e_1' e_2')\). By condition 3, \((e_1 e_2) ~ R ~ (e_1'e_2')\). A symmetric argument for \(V = \{e_1' e_2'\}\) also shows that \(M = (e_1 e_2)\), \((e_1 R e_1')\), and \(e_2 R e_2'\) whenever \(N = (e_1' e_2')\) and hence \((e_1 e_2) ~ R ~ (e_1'e_2')\).

In all cases, \((M,N) \in R\). Since \(M\) and \(N\) were arbitrary,

\[\overline{F_{\mathrm{lambda}}}(R) \subseteq R.\]

(Only If). Suppose that \(R\) is a congruence, i.e., that

\[\overline{F_{\mathrm{lambda}}}(R) \subseteq R.\]

Suppose \(x \in \mathcal{V}\). Let \(U \subseteq \Lambda\) be any set and suppose that \(M \in F_{(\mathrm{var}, x)}(U)\). Then, since \(F_{(\mathrm{var}, x)}(U) = \{x\}\), it follows that \(M = x\). Futhermore, since \(F_{(\mathrm{var}, x)}(R[U]) = \{x\}\), \(x \in F_{(\mathrm{var}, x)}(R[U])\). A symmetric argument shows for any \(V \subseteq \Lambda\) that whenever \(N \in F_{(\mathrm{var}, x)}(V) = \{x\}\), \(x \in F_{(\mathrm{var}, x)}(R^{-1}[V])\). Thus, \((x,x) \in \overline{F_{\mathrm{lambda}}}(R) \subseteq R\) and hence \(xRx\) and condition 1 is satisfied.

Suppose \(eRe'\) for any \(e,e' \in \Lambda\) and suppose \(x \in \mathcal{V}\). Let \(U \subseteq \Lambda\) be any set and suppose that \((\lambda x . e) \in F_{(\mathrm{abs}, x)}(U)\). Then, it follows that \(e \in U\), and, since \(eRe'\), it follows that \((\lambda x . e') \in F_{(\mathrm{abs}, x)}(R[U])\). A symmetric argument shows that, for any set \(V \subseteq \Lambda\), if \((\lambda x . e') \in F_{(\mathrm{abs}, x)}(V)\), then \((\lambda x . e) \in F_{(\mathrm{abs}, x)}(R^{-1}[V])\). Thus, \(((\lambda x . e), (\lambda x . e')) \in \overline{F_{\mathrm{lambda}}}(R) \subseteq R\) and so \((\lambda x . e) ~R~ (\lambda x . e')\) and condition 2 is satisfied.

Suppose \(e_1 R e_1'\) and \(e_2 R e_2'\) for any \(e_1,e_1',e_2,e_2' \in \Lambda\). Let \(U \subseteq \Lambda\) be any set and suppose that \((e_1 e_2) \in F_{\mathrm{app}}(U)\). Then, it follows that \(e_1,e_2 \in U\), and, since \(e_1 R e_1'\) and \(e_2 R e_2'\), it follows that \((e_1' e_2') \in F_{\mathrm{app}}(R[U])\). A symmetric argument shows that, for any set \(V \subseteq \Lambda\), if \((e_1' e_2') \in F_{\mathrm{app}}(V)\), then \((e_1 e_2) \in F_{\mathrm{app}}(R^{-1}[V])\). Thus, \(((e_1 e_2), (e_1' e_2')) \in \overline{F_{\mathrm{lambda}}}(R) \subseteq R\) and so \((e_1 e_2) ~R~ (e_1' e_2')\) and condition 3 is satisfied. \(\square\)

Thus, we can summarize the relational lifting for the lambda calculus as follows:

\begin{align*}\overline{F_{\mathrm{lambda}}}(R) &= \{(x,x) \mid x \in \mathcal{V}\} \\&\cup \{((\lambda x . e), (\lambda x . e')) \mid e,e' \in \Lambda \land eRe'\} \\&\cup \{((e_1e_2), (e_1'e_2')) \mid e_1,e_1',e_2,e_2' \in \Lambda \land e_1 R e_1' \land e_2 R e_2'\}.\end{align*}

6d: Open Congruences

Our goal is to indicate that applicative bisimilarity is a congruence in some appropriate sense. However, applicative bisimilarity is a relation on closed terms whereas congruences are defined for all lambda terms, including open terms. We need some way to extend the notion of congruence to account for open terms.

We extend the relational lifting for the lambda calculus so that it operates on elements \(\mathcal{R} \in \mathcal{L}\) as follows:

\begin{align*}\Psi(\mathcal{R})_{\Gamma} &= \{(x,x) \mid x \in \Gamma\} \\&\cup \{((\lambda x . e), (\lambda x . e')) \mid (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*}

Thus, we say that a relation \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) is a call-by-value open congruence if

\[\Psi(\mathcal{E}_{\mathrm{v}}(R)) \le \mathcal{E}_{\mathrm{v}}(R).\]

Likewise, we say that a relation \(R \subseteq \Lambda(\emptyset) \times \Lambda(\emptyset)\) is a call-by-name open congruence if

\[\Psi(\mathcal{E}_{\mathrm{n}}(R)) \le \mathcal{E}_{\mathrm{n}}(R).\]

In particular, applicative bisimilarity is a call-by-value open congruence if

\[\Psi(\mathcal{E}_{\mathrm{v}}(\sim_{\mathrm{v}})) \le \mathcal{E}_{\mathrm{v}}(\sim_{\mathrm{v}})\]

and applicative bisimilarity is a call-by-name open congruence if

\[\Psi(\mathcal{E}_{\mathrm{n}}(\sim_{\mathrm{n}})) \le \mathcal{E}_{\mathrm{n}}(\sim_{\mathrm{n}}).\]

Using the notation

\[\Gamma \vdash_{\mathrm{v}} eRe'\]

for \((e,e') \in \mathcal{E}_{\mathrm{v}}(R)\) and the notation

\[\Gamma \vdash_{\mathrm{n}} eRe'\]

for \((e,e') \in \mathcal{E}_{\mathrm{n}}(R)\), a call-by-value open congruence satisfies the conditions

1. \(\Gamma \vdash_{\mathrm{v}} x R x\) for all \(x \in \Gamma\),
2. \((\Gamma \cup \{x\}) \vdash_{\mathrm{v}} (\lambda x . M) ~R~ (\lambda x . M')\) whenever \(\Gamma \vdash_{\mathrm{v}} M ~R~ M'\),
3. \(\Gamma \vdash_{\mathrm{v}} (MN) ~R~ (M'N')\) whenever \(\Gamma \vdash_{\mathrm{v}} M ~R~ M'\) and \(\Gamma \vdash_{\mathrm{v}} N ~R~ N'\),

and a call-by-name open congruence satisfies the conditions

1. \(\Gamma \vdash_{\mathrm{n}} x R x\) for all \(x \in \Gamma\),
2. \((\Gamma \cup \{x\}) \vdash_{\mathrm{n}} (\lambda x . M) ~R~ (\lambda x . M')\) whenever \(\Gamma \vdash_{\mathrm{n}} M ~R~ M'\),
3. \(\Gamma \vdash_{\mathrm{n}} (MN) ~R~ (M'N')\) whenever \(\Gamma \vdash_{\mathrm{n}} M~R~ M'\) and \(\Gamma \vdash_{\mathrm{n}} N ~R~ N'\).

7: Howe's Method

Next, we will prove that applicative bisimulation is a congruence.

7a: Motivation

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

\[\Psi(\mathcal{R}) \le \mathcal{R},\]

i.e., if it is a pre-fixed point of the map \(\Psi : \mathcal{L} \rightarrow \mathcal{L}\) defined as

\begin{align*}\Psi(\mathcal{R})_{\Gamma} &= \{(x,x) \mid x \in \Gamma\} \\&\cup \{((\lambda x . e), (\lambda x . e')) \mid (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}\) is a complete lattice and \(\Psi\) is a monotone map, by the Tarski-Knaster theorem, we can systematically obtain a least fixed point of \(\Psi\). The appropriate notion of "meet" for some subset \(S \subseteq \mathcal{L}\) 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 \Psi)_\Gamma = \bigcap \left\{ \mathcal{R}_\Gamma \;\middle\vert{}\; \mathcal{R} \in \mathcal{L} \land \Psi(\mathcal{R}) \le \mathcal{R} \right\}.\]

Now, though this produces a congruence, we are interested in demonstrating that the open extension \(\mathcal{E}(\sim)\) of applicative bisimilarity \(\sim\) is a (context-indexed) congruence (where we write \(\sim\) to stand generically either for the call-by-value or call-by-name variant). Our strategy is to compose the relation \(\mathcal{E}(\sim)\) with the map \(\Psi\) to produce a new map \(\Phi\) defined as

\[\Phi(\mathcal{R}) = \Psi(\mathcal{R}) \circ \mathcal{E}(\sim).\]

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

\[\mathcal{H} = \mu \Phi = \bigwedge \{ \mathcal{R} \in \mathcal{L} \mid \Phi(\mathcal{R}) \le \mathcal{R} \},\]

or, equivalently,

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

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

Thus, extensionally, \(\mathcal{H}\) and \(\mathcal{E}(\sim)\) 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}\) is a congruence by construction. Because \(\mathcal{H}\) is a fixed point, we have

\[\mathcal{H} = \Psi(\mathcal{H}) \circ \mathcal{E}(\sim).\]

Since \(\mathcal{E}(\sim)\) is reflexive, \(\mathrm{id} \le \mathcal{E}(\sim)\), 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}\) is monotone for any \(\mathcal{R} \in \mathcal{L}\), it follows that

\[\Psi(\mathcal{H}) = \Psi(\mathcal{H}) \circ \mathrm{id} \le \Psi(\mathcal{H}) \circ \mathcal{E}(\sim) = \mathcal{H}\]

and hence

\[\Psi(\mathcal{H}) \le \mathcal{H}.\]

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

Next, we will show that \(\mathcal{H} = \mathcal{E}(\sim)\). Since \(\mathcal{H}\) is reflexive,

\[\mathrm{id} \le \Psi(\mathcal{H}).\]

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

\[\mathcal{E}(\sim) = \mathrm{id} \circ \mathcal{E}(\sim) \le \Psi(\mathcal{H}) \circ \mathcal{E}(\sim) = \Phi(\mathcal{H})\]

and hence

\[\mathcal{E}(\sim) \le \mathcal{H}.\]

Finally, we show that \(\mathcal{H} \le \mathcal{E}(\sim)\). First, we must show that the relation \(\mathcal{H}_{\emptyset}\) is a bisimulation, i.e., that

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

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\) is the greatest bisimulation, it follows that

\[\mathcal{H}_{\emptyset} \subseteq \sim.\]

Then, since \(\mathcal{H} \le \mathcal{E}(\mathcal{H}_{\emptyset})\) and \(\mathcal{E}\) is monotone, it follows that

\[\mathcal{H} \le \mathcal{E}(\mathcal{H}_{\emptyset}) \le \mathcal{E}(\sim).\]

Thus, since \(\mathcal{E}(\sim) \le \mathcal{H}\) and \(\mathcal{H} \le \mathcal{E}(\sim)\) and \(\le\) is antisymmetric, it follows that

\[\mathcal{H} = \mathcal{E}(\sim).\]

7b: Schematic Form

Next, we will derive the schematic form of Howe's method.

We will write

\[\Gamma \vdash e_1 \mathcal{H} e_2\]

to indicate that \((e_1, e_2) \in \mathcal{H}_{\Gamma}\).

By definition,

\[\mathcal{H} = \mu\Phi = \Psi(\mathcal{H}) \circ \mathcal{E}(\sim).\]

Thus, for any context \(\Gamma\),

\[(M,N) \in \mathcal{H}_{\Gamma} \Leftrightarrow (M,N) \in (\Psi(\mathcal{H}) \circ \mathcal{E}(\sim))_{\Gamma},\]

which means that

\[(M,N) \in \mathcal{H}_{\Gamma} \Leftrightarrow \exists L \in \Lambda(\Gamma) ((M,L) \in \Psi(\mathcal{H})_{\Gamma} \land (L, N) \in \mathcal{E}(\sim)_{\Gamma}).\]

Variables

Next, we will specialize

\[(M,N) \in \mathcal{H}_{\Gamma} \Leftrightarrow \exists L \in \Lambda(\Gamma) ((M,L) \in \Psi(\mathcal{H})_{\Gamma} \land (L, N) \in \mathcal{E}(\sim)_{\Gamma})\]

for variables.

When \(M=x\) for some variable \(x \in \mathcal{V}\), then, if \((M, L) \in \Psi(\mathcal{H})_{\Gamma}\), the only possibility is \(L=x\). The condition \((M,L) = (x,x) \in \Psi(\mathcal{H})_{\Gamma}\) is unconditionally satisfied and becomes superfluous. Thus, we are left with \((L, N) \in \mathcal{E}(\sim)_{\Gamma}\) which means that \((x, N) \in \mathcal{E}(\sim)_{\Gamma}\), so the rule for variables becomes

\[\frac{\Gamma \vdash x \sim N}{\Gamma \vdash x \mathcal{H} N}.\]

Abstraction

Next, we will specialize

\[(M,N) \in \mathcal{H}_{\Gamma} \Leftrightarrow \exists L \in \Lambda(\Gamma) ((M,L) \in \Psi(\mathcal{H})_{\Gamma} \land (L, N) \in \mathcal{E}(\sim)_{\Gamma})\]

for abstractions.

When \(M = (\lambda x . M')\), then, if \((M, L) \in \Psi(\mathcal{H})_{\Gamma}\), it follows that \(L = (\lambda x . L')\) and \((M', L') \in \mathcal{H}_{\Gamma \cup \{x\}}\). If \((L, N) \in \mathcal{E}(\sim)_{\Gamma}\), then \(((\lambda x . L'), N) \in \mathcal{E}(\sim)_{\Gamma}\). This yields

\[\frac{\Gamma,x \vdash M' ~\mathcal{H}~ L', \Gamma \vdash (\lambda x . L') \sim N}{\Gamma \vdash (\lambda x . M') ~\mathcal{H}~ N}.\]

Application

Next, we will specialize

\[(M,N) \in \mathcal{H}_{\Gamma} \Leftrightarrow \exists L \in \Lambda(\Gamma) ((M,L) \in \Psi(\mathcal{H})_{\Gamma} \land (L, N) \in \mathcal{E}(\sim)_{\Gamma})\]

for applications.

When \(M = (M_1 M_2)\), then, if \((M,L) \in \Psi(\mathcal{H})_{\Gamma}\), it follows that \(L = (L_1 L_2)\) and \((M_1, L_1) \in \mathcal{H}_{\Gamma}\) and \((M_2, L_2) \in \mathcal{H}_{\Gamma}\). If \((L, N) \in \mathcal{E}(\sim)_{\Gamma}\), then \(((L_1 L_2), N) \in \mathcal{E}(\sim)_{\Gamma}\). This yields

\[\frac{\Gamma \vdash M_1 ~\mathcal{H}~ L_1, \Gamma \vdash M_2 ~\mathcal{H}~ L_2, \Gamma \vdash (L_1 L_2) \sim N}{\Gamma \vdash (M_1 M_2) ~\mathcal{H}~ N}.\]

7c: Substitution Lemma

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

Lemma (Substitution - Howe's). If \(\Gamma,x \vdash M ~\mathcal{H}~ N\) and \(\emptyset \vdash A ~\mathcal{H}~ B\) where \(A,B \in E\) and \(E\) is either \(\Lambda(\emptyset)\) or \(V(\emptyset)\), then \(\Gamma \vdash M[A/x] ~\mathcal{H}~ N[B/x]\).

Proof. We proceed by structural induction on the term \(M\) in the premise \(\Gamma,x \vdash M \mathcal{H} N\).

Note that, if \((M,N) \in \mathcal{H}_{\Gamma \cup \{x\}}\), then, since

\[\mathcal{H}_{\Gamma \cup \{x\}} = \Psi(\mathcal{H})_{\Gamma \cup \{x\}} \circ \mathcal{E}(\sim)_{\Gamma \cup \{x\}},\]

this implies that there is some \(K \in \Lambda(\Gamma \cup \{x\})\) such that

\[(M,K) \in \Psi(\mathcal{H})_{\Gamma \cup \{x\}} \text{ and } (K, N) \in \mathcal{E}(\sim)_{\Gamma \cup \{x\}}.\]

Case 1: \(M = y\) for some variable \(y\). Then \((M,K) \in \Psi(\mathcal{H})_{\Gamma \cup \{x\}}\) implies that \(K=y\).

Case 1a: Suppose \(y=x\). Then \(M[A/x] = x[A/x] = A\). The premise \(\Gamma,x \vdash K \sim N\) then becomes \(\Gamma,x \vdash x \sim N\). Let \(\sigma \in \mathcal{S}(E, \Gamma)\) be any closing substitution list. Then, by definition of open extension, it follows that \(x[B/x][\sigma] \sim N[B/x][\sigma]\), i.e., \(B[\sigma] \sim N[B/x][\sigma]\). Since \(\sigma\) was arbitrary, \(\Gamma \vdash B \sim N[B/x]\). Since \(A\) and \(B\) are closed and \(\emptyset \vdash A \mathcal{H} B\), it follows that \(\Gamma \vdash A \mathcal{H} B\). Since \(\Gamma \vdash A \mathcal{H} B\) and \(\Gamma \vdash B \sim N[B/x]\), it follows that \(\Gamma \vdash A \mathcal{H} N[B/x]\), and since \(M[A/x] = A\), it follows that \(\Gamma \vdash M[A/x] \mathcal{H} N[B/x]\).

Case 1b: Suppose \(y \ne x\). Then \(M[A/x] = y[A/x] = y\). The premise \(\Gamma,x \vdash K \sim N\) then becomes \(\Gamma,x \vdash y \sim N\). Then, in particular, for any closing substitution \(\sigma \in \mathcal{S}(E, \Gamma)\), it follows that \(y[B/x][\sigma] \sim N[B/x][\sigma]\) which, since \(y \ne x\), means \(y[\sigma] \sim N[B/x][\sigma]\) and hence \(\Gamma \vdash y \sim N[B/x]\). Then, since \(\Gamma \vdash y \mathcal{H} y\), it follows that \(\Gamma \vdash y \mathcal{H} N[B/x]\) and since \(M[A/x] = y\), it follows that \(\Gamma \vdash M[A/x] \mathcal{H} N[B/x]\).

Case 2: \(M = (\lambda y . M_1)\). Then, it follows that \(N = (\lambda y . N_1)\) and \(K = (\lambda y . K_1)\) where \(\Gamma,x,y \vdash M_1 \mathcal{H} K_1\) and \(\Gamma,x \vdash (\lambda y . K_1) \sim N\). We then apply the inductive hypothesis to the pair \((M_1, K_1)\) to obtain \(\Gamma,y \vdash M_1[A/x] \mathcal{H} K_1[B/x]\). By definition of \(\Psi\), this means that \(\Gamma \vdash (\lambda y . M_1[A/x]) \mathcal{H} (\lambda y . K_1[B/x])\). Since \(\Gamma,x \vdash (\lambda y . K_1) \sim N\), for any substitution list \(\sigma \in \mathcal{S}(E, \Gamma)\), it follows that \((\lambda y . K_1)[B/x][\sigma] \sim N[B/x][\sigma]\). Without loss of generality, we assume \(y \ne x\) and \(y \notin \mathrm{Free}(B)\), so that \((\lambda y . K_1)[B/x][\sigma] = (\lambda y . K_1[B/x][\sigma])\). Since \(y \notin \mathrm{dom}(\sigma)\), it follows that \((\lambda y . K_1[B/x][\sigma]) = (\lambda y . K_1[B/x])[\sigma]\). We thus obtain \((\lambda y . K_1[B/x])[\sigma] \sim N[B/x][\sigma]\). We conclude that \(\Gamma \vdash (\lambda y . K_1[B/x]) \sim N[B/x]\). From \(\Gamma \vdash (\lambda y . M_1[A/x]) \mathcal{H} (\lambda y . K_1[B/x])\) and \(\Gamma \vdash (\lambda y . K_1)[B/x] \sim N[B/x]\), we conclude \(\Gamma \vdash (\lambda y . M_1[A/x]) \mathcal{H} N[B/x]\), and, since \(M[A/x] = (\lambda y . M_1)[A/x] = (\lambda y . M_1[A/x])\), we conclude that \(\Gamma \vdash M[A/x] \mathcal{H} N[B/x]\).

Case 3: \(M = (M_1 M_2)\). Then, it follows that \(N = (N_1 N_2)\) and \(K = K_1 K_2\) where \(\Gamma,x \vdash M_1 \mathcal{H} K_1\), \(\Gamma,x \vdash M_2 \mathcal{H} K_2\), and \(\Gamma,x \vdash (K_1 K_2) \sim N\). We then apply the inductive hypothesis to subterms to obtain \(\Gamma \vdash M_1[A/x] \mathcal{H} K_1[B/x]\) and \(\Gamma \vdash M_2[A/x] \mathcal{H} K_2[B/x]\). By definition of \(\Psi(\mathcal{H})\), it follows that \(\Gamma \vdash (M_1[A/x]M_2[A/x]) \mathcal{H} (K_1[B/x]K_2[B/x])\). Since \(\Gamma,x \vdash (K_1 K_2) \sim N\), then, for any substitution \(\sigma \in \mathcal{S}(E, \Gamma)\), \((K_1 K_2)[B/x][\sigma] \sim N[B/x][\sigma]\) and thus \((K_1[B/x] K_2[B/x])[\sigma] \sim N[B/x][\sigma]\). Since \(\sigma\) was arbitrary, \(\Gamma \vdash (K_1[B/x] K_2[B/x]) \sim N[B/x]\). Since \(\Gamma \vdash (M_1[A/x]M_2[A/x]) \mathcal{H} (K_1[B/x]K_2[B/x])\) and \(\Gamma \vdash (K_1[B/x] K_2[B/x]) \sim N[B/x]\), it follows that \(\Gamma \vdash (M_1[A/x]M_2[A/x]) \mathcal{H} N[B/x]\) and hence \(\Gamma \vdash (M_1 M_2)[A/x] \mathcal{H} N[B/x]\).

\(\square\)

We have thus indicated that there is one additional structural rule enjoyed by \(\mathcal{H}\):

\[\frac{\Gamma,x \vdash M \mathcal{H} N, \emptyset \vdash A \mathcal{H} B}{\Gamma \vdash M[A/x] \mathcal{H} N [B/x]}.\]

7d: Head Step Lemma

Next, we will establish one final lemma.

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

1. Call-by-value: 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{v}} (\lambda x . e^*_0)\) and \(e_0 \mathcal{H} e^*_0\).
2. Call-by-name: if \(e \Downarrow_{\mathrm{n}} (\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{n}} (\lambda x . e^*_0)\) and \(e_0 \mathcal{H} e^*_0\).

Proof. We proceed by induction on closed terms. Since \(\emptyset \vdash e \mathcal{H} e^*\), it follows that \(\emptyset \vdash e \mathcal{H} K\) and \(\emptyset \vdash K \sim e^*\) (where \(\sim\) denotes either \(\sim_{\mathrm{v}}\) or \(\sim_{\mathrm{n}}\)).

Since \(e\) is closed, it is either an abstraction or an application.

Case 1 (base): \(e = (\lambda x . e_0)\). Then \(e \Downarrow (\lambda x . e_0)\) for both CBV and CBN semantics. Since \(\emptyset \vdash e \mathcal{H} K\), it follows that \(K = (\lambda x . K_0)\) and \(x \vdash e_0 \mathcal{H} K_0\). Since \(K\) is a already a value, \(K \Downarrow (\lambda x . K_0)\) (for both CBV and CBN semantics). Since \(\emptyset \vdash K \sim e^*\) and \(K \Downarrow (\lambda x . K_0)\), it follows that \(e^* \Downarrow (\lambda x . e^*_0)\) and, for all \(a \in \mathrm{Input}\) (where \(\mathrm{Input}\) is \(V(\emptyset)\) for CBV and \(\Lambda(\emptyset)\) for CBN), \(K_0[a/x] \sim e^*_0[a/x]\). Thus, it follows that \(x \vdash K_0 \sim e^*_0\). Since \(x \vdash e_0 \mathcal{H} K_0\) and \(x \vdash K_0 \sim e^*_0\), it follows that \(x \vdash e_0 \mathcal{H} e^*_0\).

Case 2 (induction): \(e = (e_1 e_2)\) and \(e \Downarrow (\lambda x . e_0)\). Then, since \(\emptyset \vdash (e_1e_2) \mathcal{H} K\), it follows that \(K = K_1 K_2\), \(\emptyset \vdash e_1 \mathcal{H} K_1\), and \(\emptyset \vdash e_2 \mathcal{H} K_2\).

Case 2a: (call-by-value). Suppose \((e_1 e_2) \Downarrow_{\mathrm{v}} (\lambda x . e_0)\). In CBV, we have

\[\frac{e_1 \Downarrow_{\mathrm{v}} (\lambda y . e_1'), e_2 \Downarrow_{\mathrm{v}} v_2, e_1'[v_2/y] \Downarrow_{\mathrm{v}} (\lambda x . e_0)}{(e_1 e_2) \Downarrow_{\mathrm{v}} (\lambda x . e_0)}.\]

By the inductive hypothesis on \(e_1 \Downarrow_{\mathrm{v}} (\lambda y . e_1')\), we have \(K_1 \Downarrow_{\mathrm{v}} (\lambda y . K_1')\) and \(y \vdash e_1' \mathcal{H} K_1'\). Since \(v_2 = (\lambda y . v_2')\) is an abstraction, by inductive hypothesis on \(e_2 \Downarrow_{\mathrm{v}} v_2\), \(K_2 \Downarrow_{\mathrm{v}} v_{K_2}\) and \(\emptyset \vdash v_2 \mathcal{H} K_2\). We then apply the substitution lemma:

\[\frac{y \vdash e_1' \mathcal{H} K_1', \emptyset \vdash v_2 \mathcal{H} v_{K_2}}{\emptyset \vdash e_1'[v_2/y] \mathcal{H} K_1'[v_{K_2}/y]}.\]

Applying the inductive hypothesis to \(e_1'[v_2/y] \Downarrow_{\mathrm{v}} (\lambda x . e_0)\) yields \(K_1'[v_{K_2}/y] \Downarrow_{\mathrm{v}} (\lambda x . e^*_0)\) with \(x \vdash e_0 \mathcal{H} e^*_0\). Then, according to CBV semantics,

\[\frac{K_1 \Downarrow_{\mathrm{v}} (\lambda y . K_1'), K_2 \Downarrow_{\mathrm{v}} v_{K_2}, K_1'[v_{K_2}/y] \Downarrow_{\mathrm{v}} (\lambda x . e^*_0)}{(K_1 K_2) \Downarrow_{\mathrm{v}} (\lambda x . e^*_0)}.\]

Now, since \(K \sim_{\mathrm{v}} e^*\), it follows that \(e^* \Downarrow_{\mathrm{v}} (\lambda x . e^{**}_0)\) and \(e^*_0[v/x] \sim_{\mathrm{v}} e^{**}_0[v/x]\) for all \(v \in V(\emptyset)\). It then follows that \(x \vdash e^*_0 \sim_{\mathrm{v}} e^{**}_0\). Since we already established that \(x \vdash e_0 \mathcal{H} e^*_0\) and \(x \vdash e^*_0 \sim_{\mathrm{v}} e^{**}_0\), by definition, \(x \vdash e_0 \mathcal{H} e^{**}_0\).

Case 2b: (call-by-name). Suppose \((e_1 e_2) \Downarrow_{\mathrm{n}} (\lambda x . e_0)\). In CBN, we have

\[\frac{e_1 \Downarrow_{\mathrm{n}} (\lambda y . e_1'), e_1'[e_2/y] \Downarrow_{\mathrm{n}} (\lambda x . e_0)}{(e_1e_2) \Downarrow_{\mathrm{n}} (\lambda x . e_0)}.\]

Since \(\emptyset \vdash e_1 \mathcal{H} K_1\) and \(e_1 \Downarrow_{\mathrm{n}} (\lambda y . e_1')\), by inductive hypothesis, there exists a term \(K_1'\) such that \(K_1 \Downarrow_{\mathrm{n}} (\lambda y . K_1')\) and \(y \vdash e_1' \mathcal{H} K_1'\). We then apply the substitution lemma:

\[\frac{y \vdash e_1' \mathcal{H} K_1', \emptyset \vdash e_2 \mathcal{H} K_2}{\emptyset \vdash e_1'[e_2/y] \mathcal{H} K_1'[K_2/y]}.\]

Since \(e_1'[e_2/y] \mathcal{H} K_1'[K_2/y]\) and \(e_1'[e_2/y] \Downarrow_{\mathrm{n}} (\lambda x . e_0)\), by inductive hypothesis, there exists a term \(e^*_0\) such that \(K_1'[K_2/y] \Downarrow_{\mathrm{n}} (\lambda x . e^*_0)\) and \(x \vdash e_0 \mathcal{H} e^*_0\). Then, according to CBN semantics,

\[\frac{K_1 \Downarrow_{\mathrm{n}} (\lambda y . K_1'), K_1'[K_2/y] \Downarrow_{\mathrm{n}} (\lambda x . e^*_0)}{(K_1 K_2) \Downarrow_{\mathrm{n}} (\lambda x . e^*_0)}.\]

Now, since \(K \sim_{\mathrm{n}} e^*\), it follows that \(e^* \Downarrow_{\mathrm{n}} (\lambda x . e^{**}_0)\) and \(e^*_0[a/x] \sim_{\mathrm{n}} e^{**}_0[a/x]\) for all \(a \in \Lambda(\emptyset)\). It then follows that \(x \vdash e^*_0 \sim_{\mathrm{n}} e^{**}_0\). Since we already established that \(x \vdash e_0 \mathcal{H} e^*_0\) and \(x \vdash e^*_0 \sim_{\mathrm{n}} e^{**}_0\), by definition, \(x \vdash e_0 \mathcal{H} e^{**}_0\).

\(\square\)

We can also state a symmetric version of the head step lemma.

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

• Call-by-value: 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{v}} (\lambda x . e_0)\) and \(e_0 \mathcal{H} e^*_0\).
• Call-by-name: if \(e^* \Downarrow_{\mathrm{n}} (\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{n}} (\lambda x . e_0)\) and \(e_0 \mathcal{H} e^*_0\).

Proof. We proceed by induction on closed terms. Since \(\emptyset \vdash e \mathcal{H} e^*\), it follows that \(\emptyset \vdash e \mathcal{H} K\) and \(\emptyset \vdash K \sim e^*\) (where \(\sim\) denotes either \(\sim_{\mathrm{v}}\) or \(\sim_{\mathrm{n}}\)).

Since \(e^* \Downarrow (\lambda x . e^*_0)\) and \(\emptyset \vdash K \sim e^*\), by symmetry and the definition of applicative bisimilarity, it follows that \(K \Downarrow (\lambda x . K_0)\) for some \(K_0\) such that \(x \vdash K_0 \sim e^*_0\).

Since \(K\) evaluates to an abstraction, \(K\) is either an abstraction or an application. Since \(\emptyset \vdash e \mathcal{H} K\), \(e\) must match the constructor structure of \(K\).

Case 1 (base): \(K = (\lambda x . K_0)\). Then \(K \Downarrow (\lambda x . K_0)\) for both CBV and CBN semantics. Since \(\emptyset \vdash e \mathcal{H} K\), it follows that \(e = (\lambda x . e_0)\) and \(x \vdash e_0 \mathcal{H} K_0\). Since \(e\) is already a value, \(e \Downarrow (\lambda x . e_0)\) (for both CBV and CBN semantics). Since \(x \vdash e_0 \mathcal{H} K_0\) and \(x \vdash K_0 \sim e^*_0\), by definition of \(\mathcal{H} = \Psi(\mathcal{H}) \circ \mathcal{E}(\sim)\), it follows that \(x \vdash e_0 \mathcal{H} e^*_0\).

Case 2 (induction): \(K = (K_1 K_2)\) and \(K \Downarrow (\lambda x . K_0)\). Then, since \(\emptyset \vdash e \mathcal{H} (K_1 K_2)\), it follows that \(e = (e_1 e_2)\), \(\emptyset \vdash e_1 \mathcal{H} K_1\), and \(\emptyset \vdash e_2 \mathcal{H} K_2\).

Case 2a: (call-by-value). Suppose \((K_1 K_2) \Downarrow_{\mathrm{v}} (\lambda x . K_0)\). In CBV, we have

\[\frac{K_1 \Downarrow_{\mathrm{v}} (\lambda y . K_1'), K_2 \Downarrow_{\mathrm{v}} v_{K_2}, K_1'[v_{K_2}/y] \Downarrow_{\mathrm{v}} (\lambda x . K_0)}{(K_1 K_2) \Downarrow_{\mathrm{v}} (\lambda x . K_0)}.\]

By the inductive hypothesis on \(K_1 \Downarrow_{\mathrm{v}} (\lambda y . K_1')\), we have \(e_1 \Downarrow_{\mathrm{v}} (\lambda y . e_1')\) and \(y \vdash e_1' \mathcal{H} K_1'\). Since \(v_{K_2}\) is an abstraction, by inductive hypothesis on \(K_2 \Downarrow_{\mathrm{v}} v_{K_2}\), \(e_2 \Downarrow_{\mathrm{v}} v_2\) and \(\emptyset \vdash v_2 \mathcal{H} v_{K_2}\). We then apply the substitution lemma:

\[\frac{y \vdash e_1' \mathcal{H} K_1', \emptyset \vdash v_2 \mathcal{H} v_{K_2}}{\emptyset \vdash e_1'[v_2/y] \mathcal{H} K_1'[v_{K_2}/y]}.\]

Applying the inductive hypothesis to \(K_1'[v_{K_2}/y] \Downarrow_{\mathrm{v}} (\lambda x . K_0)\) yields \(e_1'[v_2/y] \Downarrow_{\mathrm{v}} (\lambda x . e_0)\) with \(x \vdash e_0 \mathcal{H} K_0\). Then, according to CBV semantics,

\[\frac{e_1 \Downarrow_{\mathrm{v}} (\lambda y . e_1'), e_2 \Downarrow_{\mathrm{v}} v_2, e_1'[v_2/y] \Downarrow_{\mathrm{v}} (\lambda x . e_0)}{(e_1 e_2) \Downarrow_{\mathrm{v}} (\lambda x . e_0)}.\]

Since we established that \(x \vdash e_0 \mathcal{H} K_0\) and \(x \vdash K_0 \sim_{\mathrm{v}} e^*_0\), by definition, \(x \vdash e_0 \mathcal{H} e^*_0\).

Case 2b: (call-by-name). Suppose \((K_1 K_2) \Downarrow_{\mathrm{n}} (\lambda x . K_0)\). In CBN, we have

\[\frac{K_1 \Downarrow_{\mathrm{n}} (\lambda y . K_1'), K_1'[K_2/y] \Downarrow_{\mathrm{n}} (\lambda x . K_0)}{(K_1 K_2) \Downarrow_{\mathrm{n}} (\lambda x . K_0)}.\]

Since \(\emptyset \vdash e_1 \mathcal{H} K_1\) and \(K_1 \Downarrow_{\mathrm{n}} (\lambda y . K_1')\), by inductive hypothesis, there exists a term \(e_1'\) such that \(e_1 \Downarrow_{\mathrm{n}} (\lambda y . e_1')\) and \(y \vdash e_1' \mathcal{H} K_1'\). We then apply the substitution lemma:

\[\frac{y \vdash e_1' \mathcal{H} K_1', \emptyset \vdash e_2 \mathcal{H} K_2}{\emptyset \vdash e_1'[e_2/y] \mathcal{H} K_1'[K_2/y]}.\]

Since \(e_1'[e_2/y] \mathcal{H} K_1'[K_2/y]\) and \(K_1'[K_2/y] \Downarrow_{\mathrm{n}} (\lambda x . K_0)\), by inductive hypothesis, there exists a term \(e_0\) such that \(e_1'[e_2/y] \Downarrow_{\mathrm{n}} (\lambda x . e_0)\) and \(x \vdash e_0 \mathcal{H} K_0\). Then, according to CBN semantics,

\[\frac{e_1 \Downarrow_{\mathrm{n}} (\lambda y . e_1'), e_1'[e_2/y] \Downarrow_{\mathrm{n}} (\lambda x . e_0)}{(e_1 e_2) \Downarrow_{\mathrm{n}} (\lambda x . e_0)}.\]

Since we established that \(x \vdash e_0 \mathcal{H} K_0\) and \(x \vdash K_0 \sim_{\mathrm{n}} e^*_0\), by definition, \(x \vdash e_0 \mathcal{H} e^*_0\).

\(\square\)

7e: Proof

Next, we will establish that \(\mathcal{H}_{\emptyset}\) is an applicative bisimulation, which is the missing part of the proof that \(\mathcal{H} = \mathcal{E}(\sim)\).

The proof is nearly identical for the CBV and CBN cases. Our goal is to prove the following, where \(\mathrm{Arg} = V(\emptyset)\) for CBV and \(\mathrm{Arg} = \Lambda(\emptyset)\) for CBN and \(\Downarrow = \Downarrow_{\mathrm{v}}\) for CBV and \(\Downarrow = \Downarrow_{\mathrm{n}}\) for CBN:

\[\mathcal{H}_{\emptyset} \subseteq F_{\mathrm{app}}(\mathcal{H}_{\emptyset})\]

where

\[F_{\mathrm{app}}(R) = \left\{(e_1, e_2) \in \Lambda(\emptyset) \times \Lambda(\emptyset) \middle| \begin{aligned} &\forall x \in \mathcal{V} \forall e_1' \in \Lambda (e_1 \Downarrow (\lambda x . e_1') \Rightarrow \exists e_2' \in \Lambda (e_2 \Downarrow (\lambda x . e_2') \land \forall v \in \mathrm{Arg} (e_1'[v/x] ~R~ e_2'[v/x]))) \\ &\land \\&\forall x \in \mathcal{V} \forall e_2' \in \Lambda (e_2 \Downarrow (\lambda x . e_2') \Rightarrow \exists e_1' \in \Lambda (e_1 \Downarrow (\lambda x . e_1') \land \forall v \in \mathrm{Arg} (e_1'[v/x] ~R~ e_2'[v/x]))) \end{aligned}\right\}.\]

Thus, we assume that \((e_1, e_2) \in \mathcal{H}_{\emptyset}\) and our goal is to show that \((e_1, e_2) \in F_{\mathrm{app}}(\mathcal{H}_{\emptyset})\). Since \(\emptyset \vdash e_1 \mathcal{H} e_2\), by definition, there exists a term \(e'\) such that

\[\emptyset \vdash e_1 \mathcal{H} e' \text{ and } e' \sim e_2.\]

Forward Direction (\(\forall x \in \mathcal{V} \forall e_1' \in \Lambda (e_1 \Downarrow (\lambda x . e_1') \Rightarrow \exists e_2' \in \Lambda (e_2 \Downarrow (\lambda x . e_2') \land \forall v \in \mathrm{Arg} (\emptyset \vdash e_1'[v/x] ~\mathcal{H}~ e_2'[v/x])))\)).

Suppose \(e_1 \Downarrow (\lambda x . e_1')\).

We apply the head step lemma to premises \(\emptyset \vdash e_1 \mathcal{H} e'\) and \(e_1 \Downarrow (\lambda x . e_1')\) to obtain \(e' \Downarrow (\lambda x . e'')\) and \(x \vdash e_1' \mathcal{H} e''\).

Since \(e' \Downarrow (\lambda x . e'')\) and \(e' \sim e_2\), by definition of \(\sim\), this implies that there exists an \(e_2'\) such that \(e_2 \Downarrow (\lambda x . e_2')\) and for all \(a \in \mathrm{Arg}\), \(e''[a/x] \sim e_2'[a/x]\).

For any \(a \in \mathrm{Arg}\), since \(x \vdash e_1' \mathcal{H} e''\) and \(\emptyset \vdash a \mathcal{H} a\) (by reflexivity), by the substitution lemma, we get \(\emptyset \vdash e_1'[a/x] \mathcal{H} e''[a/x]\). By transitivity, since \(\emptyset \vdash e_1'[a/x] \mathcal{H} e''[a/x]\) and \(\emptyset \vdash e''[a/x], e_2'[a/x]\), it follows that \(\emptyset \vdash e_1'[a/x] \mathcal{H} e_2'[a/x]\).

Backward Direction (\(\forall x \in \mathcal{V} \forall e_2' \in \Lambda (e_2 \Downarrow (\lambda x . e_2') \Rightarrow \exists e_1' \in \Lambda (e_1 \Downarrow (\lambda x . e_1') \land \forall v \in \mathrm{Arg} (\emptyset \vdash e_1'[v/x] ~\mathcal{H} ~ e_2'[v/x])))\)).

Suppose \(e_2' \Downarrow (\lambda x . e_2')\).

Since \(\sim\) is symmetric and \(e' \sim e_2\), it follows that \(e_2 \sim e'\). Then, by definition of \(\sim\), it follows that there exists a term \(e''\) such that \(e' \Downarrow (\lambda x . e'')\) and \(e''[a/x] \sim e_2'[a/x]\) for all \(a \in \mathrm{Arg}\).

Since \(\emptyset \vdash e_1 \mathcal{H} e'\) and \(e' \Downarrow (\lambda x . e'')\), by the converse head step lemma, there exists a term \(e_1'\) such that \(e_1 \Downarrow (\lambda x . e_1')\) and \(x \vdash e_1' \mathcal{H} e''\).

Since \(x \vdash e_1' \mathcal{H} e''\) and \(\emptyset \vdash a \mathcal{H} a\) (by reflexivity) for all \(a \in \mathrm{Arg}\), by the substitution lemma, \(\emptyset \vdash e_1'[a/x] \mathcal{H} e''[a/x]\).

By transitivity, we then conclude that \(\emptyset \vdash e_1'[a/x] \mathcal{H} e_2'[a/x]\).

\(\square\)

Thus, by coinduction, \(\mathcal{H}_{\emptyset} \subseteq \sim\), and, by construction, \(\sim \subseteq \mathcal{H}_{\emptyset}\), so \(\mathcal{H}_{\emptyset} = \sim\).

Combined with the previous reasoning, we conclude that applicative bisimilarity is a congruence.

8: Contextual Equivalence

In this section, we will introduce the standard notion of equivalence in the lambda calculus (called contextual equivalence) and prove that it is equivalent to applicative bisimilarity.

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

\(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\}.\]

Now we will establish that applicative bisimilarity is coextensive with contextual equivalence.

First, observe that if \(e_1 \sim e_2\) then \(C[e_1] \sim C[e_2]\) since \(\sim\) is a congruence. This can be established via induction on syntactic contexts: first, \([\cdot][e_1] = e_1 \sim e_2 = [\cdot][e_2]\). Then, if \(C[e_1] \sim C[e_2]\), then, by definition of congruence for lambda terms, \((\lambda x . C[e_1]) \sim (\lambda x . C[e_2])\). Likewise, if \(C[e_1] \sim C[e_2]\), then \((C[e_1] e) \sim (C[e_2] e)\) and \((e C[e_1]) \sim (e C[e_2])\) for any \(e \in \Lambda\) since \(e \sim e\) (by reflexivity).

We use the following technical lemma.

Lemma. Let \(x \in \mathcal{V}\), \(e' \in \Lambda\), \(v \in \mathrm{Arg}\). Then

\[((\lambda x . e') v) \sim e'[v/x].\]

Proof. By definition of \(\Downarrow\), \(((\lambda x . e') v) \Downarrow w \Leftrightarrow e'[v/x] \Downarrow w\). Thus, since \(sim\) is reflexive, it is trivially the case that \(w[u/y] \sim w[u/y]\) for any variable \(y\) and argument \(u\). Thus, \(((\lambda x . e') v) \sim e'[v/x]\) as required. \(\square\)

Theorem. Applicative bisimilarity coincides with contextual equivalence, i.e., \(\sim = \cong\).

Proof. (Soundness - \(\sim \subseteq \cong\)). Suppose \(e_1 \sim e_2\). Let \(C \in \mathrm{Con}\) be any syntactic context such that \(C[e_1], C[e_2] \in \Lambda(\emptyset)\). Then, since \(\sim\) is a congruence, it follows that \(C[e_1] \sim C[e_2]\). Suppose \(C[e_1] \Downarrow\). By definition, there exists a variable \(x \in \mathcal{V}\) and term \(e_1 \in \Lambda\) such that \(C[e_1] \Downarrow (\lambda x . e_1')\). Since \(C[e_1] \sim C[e_2]\), by definition of \(\sim\), it follows that there exists a term \(e_2' \in \Lambda\) such that \(C[e_2] \Downarrow (\lambda x . e_2')\) and hence \(C[e_2] \Downarrow\). By a symmetric argument, \(C[e_1] \Downarrow\) whenever \(C[e_2] \Downarrow\). Thus, \(e_1 \cong e_2\).

(Completeness - \(\cong \subseteq \sim\)). We proceed by coinduction. We will demonstrate that \(\cong\) is an applicative bisimulation, i.e.,

\[\cong \subseteq F_{\mathrm{app}}(\cong).\]

Since \(\sim\) is the greatest such bisimulation, it will follow that \(\cong \subseteq \sim\).

Suppose \(e_1 \cong e_2\).

Suppose \(x \in \mathcal{V}\), \(e_1' \in \Lambda\), and \(e_1 \Downarrow (\lambda x .e_1')\). Consider the identity context \(C_{\mathrm{id}}\) defined as \(C_{\mathrm{id}}[e] = e\) for all \(e \in \Lambda\). Since \(e_1 \cong e_2\), by definition, since \(C[e_1] \Downarrow\), it follows that \(C[e_2] \Downarrow\), and thus, by definition, there exists a term \(e_2' \in \Lambda\) such that \(e_2 \Downarrow (\lambda x . e_2')\) (where we may ensure that the bound variable is \(x\) by alpha conversion if necessary).

Suppose \(v \in \mathrm{Arg}\). We must demonstrate that \(e_1'[v/x] \cong e_2'[v/x]\). Let \(C\) be any context such that \(C[e_1'[v/x]]\) and \(C[e_2'[v/x]]\) are both closed. Define a context \(C_v\) as

\[C_v[e] = C[(ev)].\]

1. Since \(e_1 \Downarrow (\lambda x . e_1')\), it follows that \(e_1 \sim (\lambda x . e_1')\). Since \(\sim \subseteq \cong\), it follows that \(e_1 \cong (\lambda x . e_1')\), which, by definition, implies that \(C_v[e_1] \Downarrow \Leftrightarrow C_v[(\lambda x . e_1')] \Downarrow\) and hence \(C[(e_1 v)] \Downarrow \Leftrightarrow C[((\lambda x . e_1') v)] \Downarrow\).
2. By the lemma, \(((\lambda x . e_1') v) \sim e_1'[v/x]\). Since \(\sim \subseteq \cong\), it follows that \(((\lambda x . e_1') v) \cong e_1'[v/x]\), which, by definition, implies that \(C[((\lambda x . e_1') v)] \Downarrow \Leftrightarrow C[e_1'[v/x]] \Downarrow\).
3. Since \(e_1 \cong e_2\), it follows by definition that \(C[e_1] \Downarrow \Leftrightarrow C[e_2] \Downarrow\).
4. Since \(e_2 \Downarrow (\lambda x . e_2')\), it follows that \(e_2 \sim (\lambda x . e_2')\). Since \(\sim \subseteq \cong\), it follows that \(e_2 \cong (\lambda x . e_2')\), which, by definition, implies that \(C_v[e_2] \Downarrow \Leftrightarrow C_v[(\lambda x . e_2')] \Downarrow\) and hence \(C[(e_2 v)] \Downarrow \Leftrightarrow C[((\lambda x . e_2') v)] \Downarrow\).
5. By the lemma, \(((\lambda x . e_2') v) \sim e_2'[v/x]\). Since \(\sim \subseteq \cong\), it follows that \(((\lambda x . e_2') v) \cong e_2'[v/x]\), which, by definition, implies that \(C[((\lambda x . e_2') v)] \Downarrow \Leftrightarrow C[e_2'[v/x]] \Downarrow\).

Chaining these equivalences, we obtain:

\begin{align*}C[e_1'[v/x]] \Downarrow & \Leftrightarrow C[((\lambda x . e_1') v)] \Downarrow \\&\Leftrightarrow C[(e_1 v)] \Downarrow \\&\Leftrightarrow C[(e_2 v)] \Downarrow \\&\Leftrightarrow C[((\lambda x .e_2') v)] \Downarrow \\&\Leftrightarrow C[e_2'[v/x]] \Downarrow.\end{align*}

Thus, we conclude that contextual equivalence is an applicative bisimulation. \(\square\)