LeanLambda

• Note:

  • We assume that there is an infinite supply of variables, so that for any finite set $\mathcal{S}$ of variables, there exists a variable $x \notin \mathcal{S}$. The Lean code achieves this by allowing variable names to be arbitrary strings
  • The set of all $\lambda$ terms is denoted as $\Lambda$

• Variable Renaming: Define the renaming relation $\to^{x\to y}$ as follows

  • $x \to^{x \to y} y$
  • $z \to^{x \to y} z$, provided $z \notin {x, y}$
  • If $M \to^{x \to y} M', N \to^{x \to y} N'$, then $M \ N \to^{x \to y} M' \ N'$
  • $(\lambda x. N) \to^{x \to y} (\lambda x. N)$, provided $y \notin FV(N) \backslash {x}$ (Note that this is required: If $\lambda x. N$ is a subterm of the term $A$ we're considering, and that $N$ has free $y$, then the meaning of $A$ might change whenever a free $x$ is replaced with $y$ somewhere else in $A$)
  • If $N \to^{x \to y} N', z \notin {x, y}$, then $(\lambda z. N) \to^{x \to y} (\lambda z. N')$

  We also define the rename function $M^{x \to y}$ as follows:

  • $x^{x \to y} := y$
  • $z^{x \to y} := z$, provided $z \neq x$
  • $(M \ N)^{x \to y} := M^{x \to y} \ N^{x \to y}$
  • $(\lambda x. M)^{x \to y} := M$
  • $(\lambda z. M)^{x \to y} := \lambda z. M^{x \to y}$, provided $z \neq x$

• Binding variables: Define the binding variables function as follows:

  • $BV(x) := \emptyset$
  • $BV(M \ N) := BV(M) \cup BV(N)$
  • $BV(\lambda x. M) := BV(M) \cup {x}$

  Define the all variables function as $$AV(M) := FV(M) \cup BV(M)$$

• Properties of Variable Renaming:

  • $M \to^{x \to x} M$
  • If $M \to^{x \to y} N$ and $x \notin FV(M)$, then $N = M$
  • Given $M \to^{x \to y} N$
    • If $x \in FV(M)$, then $FV(N) = (FV(M) \backslash {x}) \cup {y}$
    • If $x \notin FV(M)$, then $FV(N) = FV(M)$
  • If $M \to^{x \to y} N_1, M \to^{x \to y} N_2$, then $N_1 = N_2$
  • If $M \to^{x \to x} N$, then $M = N$
  • Given $M, x, y$, if $y \notin AV(M) \backslash {x}$, then there exists $N$ such that $M \to^{x \to y} N$; For the opposite direction, if there exists $N$ such that $M \to^{x \to y} N$, then $y \notin FV(M) \backslash {x}$
  • If $M \to^{x \to y} N, N \to^{y \to z} P$, then $M \to^{x \to z} P$
  • If $M \to^{x \to y} N, N \to^{y \to x} P$, then $M = P$
  • If ${x, y} \cap {z, w} = \emptyset, M \to^{x \to y} N, M \to^{z \to w} M', N \to^{z \to w} N'$, then $M' \to^{z \to w} N'$

• Alpha Conversion: The production rules for $\to_\alpha$ are as follows:

  • Renaming: $\lambda x. M \to_\alpha \lambda y. N$ for all $M, N \in \Lambda$ and variables $x, y$ such that $y \notin AV(M)$ and $M \to^{x \to y} N$
  • Compatibility: If $M \to_\alpha N$, then
    • $M \ L \to_\alpha N \ L$ and $L \ M \to_\alpha L \ N$ for all $L \in \Lambda_{S\alpha}$
    • $\lambda z. M \to_\alpha \lambda z. N$ for all variables $z$

  $\twoheadrightarrow_\alpha$ is defined as the reflexive-transitive closure of $\to_\alpha$, and $\equiv$ is defined as the reflexive-transitive-symmetric closure of $\to_\alpha$

• NoUnder and NoFUnder: The NoUnder relation $noU(x,y,M)$ is true iff there is no $x$ under $\lambda y$ in $M$

  • $noU(x, y, z) := \top$, for arbitrary variable $z$
  • $noU(x, y, M \ N) := noU(x, y, M) \land noU(x, y, N)$
  • $noU(x, y, \lambda y. M) := x \notin AV(M)$
  • $noU(x, y, \lambda z. M) := noU(x, y, M)$, for $z \neq y$

  The NoFUnder relation $noFU(x, y, M)$ is true iff there is no free $x$ under $\lambda y$ in $M$

  • $noFU(x, y, z) := \top$, for arbitrary variable $z$
  • $noFU(x, y, M \ N) := noFU(x, y, M) \land noFU(x, y, N)$
  • $noFU(x, y, \lambda x. M) := \top$
  • $noFU(x, y, \lambda y. M) := x \notin AV(M)$, for $x \neq y$
  • $noFU(x, y, \lambda z. M) := noFU(x, y, M)$, for $z \neq x, z \neq y$

  Note: $noU$ and $noFU$ are introduced to facilitate better characterization of bound variable uniform renaming

• Bound Variable Uniform Renaming: The bound variable uniform renaming $M[x:=y]_B$ is defined for $M \in \Lambda$ and variables $x, y$

  • $z[x:=y]_B := z$, for all variables $z$
  • $(M \ N)[x:=y]_B := M[x:=y]_B \ N[x:=y]_B$
  • $(\lambda x. M)[x:=y]_B := (\lambda y. (M[x:=y]_B)^{x\to y})$
  • $(\lambda z. M)[x:=y]_B := (\lambda z. M[x:=y]_B)$, provided $z \notin {x, y}$

  Note: Bound variable uniform renaming is introduced to facilitate the proof of

  • Lemma for relaxing requirement of the rename step of $\to_\alpha$, and
  • Lemma for symmetry of $\twoheadrightarrow_\alpha$

• Variable Exchange: $M[x \leftrightarrow y]$ is defined as simultaneously changing all the $x$ in $M$ to $y$ and all the $y$ in $M$ to $x$

  • $z[x \leftrightarrow y] := z^{x \leftrightarrow y}$
  • $(M \ N)[x \leftrightarrow y] := (M[x \leftrightarrow y] \ N[x \leftrightarrow y])$
  • $(\lambda z. M)[x \leftrightarrow y] := \lambda z^{x \leftrightarrow y}. M[x \leftrightarrow y]$

  Note: Variable exchange is introduced to facilitate the proof of Rename preserves $\equiv$, i.e $$\forall M \ N \ M' \ N' \ x \ y, M \equiv N \to (M \to^{x \to y} M') \to (N \to^{x \to y} N') \to M' \equiv N' \ \ \ ()$$ Naturally, $()$ is proved by induction on $M \equiv N$. Note that Terms related by $\to_\alpha$ are $\equiv$ after the same rename already solves the base case of $(*)$. However, the trans case requires extra treatment. In the trans case, we have $$M \equiv P, P \equiv N, M \to^{x \to y} M', N \to^{x \to y} N'$$ $$IHMP : \forall M' \ P' \ x \ y, (M \to^{x \to y} M') \to (P \to^{x \to y} P') \to M' \equiv P'$$ $$IHPN : \forall P' \ N' \ x \ y, (P \to^{x \to y} P') \to (N \to^{x \to y} N') \to P' \equiv N'$$ and we want to show that $M \equiv N$. To do this, we would want to find a $P'$ such that $P \to^{x \to y} P'$. However, this is not always possible because it might be the case that $y \in FV(P)$. To solve this issue, we can take a variable $z \notin AV(M) \cup AV(N) \cup AV(P) \cup {x}$, which guarantees the existence of $M'', N'', P''$ such that $$M \to^{x \to z} M'', N \to^{x \to z} N'', P \to^{x \to z} P''$$ which allows us to use the induction hypotheses to derive $M'' \equiv N''$. Then, we use the properties of variable exchange to show that $M' \equiv M''[y \leftrightarrow z]$ and $N' \equiv N''[y \leftrightarrow z]$. Finally, since variable exchange preserves $\equiv$, we have $M' \equiv N'$

• Properties of $\alpha$ conversion:

  • $\twoheadrightarrow$ is compatible with the construction rules of $\lambda$ terms
  • If $M \equiv N$, then $FV(M) = FV(N)$
  • Structure-preserving:
    • If $M \ N \equiv P$, then there exists $M_1, N_1$ such that $P = M_1 \ N_1$
    • If $\lambda x. M \equiv P$, then there exists $M_1$ and $y$ such that $P = \lambda y. M_1$
  • Lemma for relaxing requirement of the rename step of $\to_\alpha$: If $M \to^{x \to y} N$ and $z \notin AV(M) \cup {y}$, then $$\lambda x. M \twoheadrightarrow_\alpha \lambda y. (M[y:=z]_B^{x\to y})[z:=y]_B$$
  • Relaxing requirement of the rename step of $\to_\alpha$: If $M \to^{x \to y} N$, then $\lambda x. M \twoheadrightarrow \lambda y. N$
  • Lemma for symmetry of $\twoheadrightarrow_\alpha$: If $noFU(y, x, M)$ and $z \notin AV(M) \cup {x, y}$, then $$\lambda y. M^{x \to y} \twoheadrightarrow_\alpha \lambda x. (M^{x \to y}[x:=z]_B)^{y \to x}[z:=x]_B$$
  • Symmetry of $\twoheadrightarrow_\alpha$: If $M \to_\alpha N$, then $N \twoheadrightarrow_\alpha M$. As a corollary, if $M \twoheadrightarrow_\alpha N$, then $N \twoheadrightarrow_\alpha M$
    Note: It follows that $\twoheadrightarrow_\alpha$ is equivalent to $\equiv$
  • Terms related by $\to_\alpha$ are $\equiv$ after the same rename: If $M \to_\alpha N, M \to^{x \to y} M', N \to^{x \to y} N'$, then $M' \equiv N'$
  • Variable exchange preserves $\equiv$: $M \equiv N$ iff $M[x \leftrightarrow y] \equiv N[x \leftrightarrow y]$
  • Rename preserves $\equiv$: If $M \equiv N, M \to^{x \to y} M', N \to^{x \to y} N'$, then $M' \equiv N'$
  • Rename reflects $\equiv$: If $M' \equiv N', M \to^{x \to y} M', N \to^{x \to y} N'$, then $M \equiv N$
  • Destruction compatible
    • If $M_1 \ N_1 \equiv M_2 \ N_2$, then $M_1 \equiv M_2$ and $N_1 \equiv N_2$
    • If $\lambda x. M \equiv \lambda y. N$, then for all $u, M_1, M_2, N_1, N_2$ such that $M \equiv M_1, M_1 \to^{x \to u} M_2, N \equiv N_1, N_1 \to^{y \to u} N_2$, we have $M_2 \equiv N_2$
      As a corollary, if $\lambda x. M \equiv \lambda x.N$, then $M \equiv N$
  • If $\lambda x. M \equiv \lambda y. N$, then for all $z \notin AV(M) \cup AV(N)$, we have $M^{x \to z} \equiv N^{x \to z}$
  • $\lambda x. M_1 \ N_1 \equiv \lambda y. M_2 \ N_2$ iff $\lambda x. M_1 \equiv \lambda y. M_2 \land \lambda x. N_1 \equiv \lambda y. N_2$
  • Given $x \neq y \land z \neq w$, we have $\lambda x \ y. M \equiv \lambda z \ w. N$ iff $\lambda y \ x. M \equiv \lambda w \ z. N$

• Definition of substitution: The substitution of $N$ for (the free occurrences of) $x$ in $M$, denoted as $M[x:=N]$, is defined as follows:

  • $x[x:=N] := N$
  • $y[x:=N] := y$, provided $y \not\equiv x$
  • $(P \ Q)[x:=N] := (P[x := N]) \ (Q[x := N])$
  • $(\lambda y. P)[x := N] := \lambda z. P'[x := N]$, provided $y \neq x$. Here $P'$ is a term and $z$ is a variable, such that $\lambda y.P \equiv \lambda z.P'$ and $z \notin FV(N) \cup {x}$. For example, $P'$ can be chosen as $P^{y\to z}$ where $z \notin AV(P) \cup FV(N) \cup {x}$
  • $(\lambda x. P)[x := N] := (\lambda x. P)$

  Note: It might be tempting to use Barendregt convention to avoid renaming in the $\lambda$ case. However, the Barendregt convention has two main drawbacks

  • It's not clear how we should formalize the Barendregt convention. This issue is particularly relevant if we want to verify properties of $\lambda$ calculus using formal verification tools
  • Even if we're using the Barendregt convention, the proof of Substitution is compatible with equivalence is still nontrivial

• Characterizing $\equiv$ using substitution: For all $\lambda$ terms $M, N$ and variables $x, y$ such that $y \notin FV(M) \backslash {x}$, we have $\lambda x. M \equiv \lambda y. N$ iff $N \equiv M[x:=y]$

• Substitution commutes with change of $\lambda$:

  • $(1)$ For all $\lambda$ terms $P_1, P_2, Q_1, Q_2$ and strings $x, y, z$, if $x \neq z, y \neq z, \lambda x. P_1 \equiv \lambda y. P_2, \lambda x. Q_1 \equiv \lambda y.Q_2$, then $\lambda x. P_1[z:=Q_1] \equiv \lambda y. P_2[z:=Q_2]$
  • $(2)$ For all $\lambda$ terms $P_1, P_2, Q_1, Q_2$ and strings $x, y$, if $\lambda x. P_1 \equiv \lambda y. P_2, \lambda x. Q_1 \equiv \lambda y.Q_2$, then $\lambda x. P_1[x:=Q_1] \equiv \lambda y. P_2[y:=Q_2]$

  Note: It's easy to see (recall the Destruction compatible in Properties of $\alpha$ conversion) that this implies Substitution is compatible with equivalence. It's worth noting that we'll be blocked by the $\lambda$ case if we try to prove Substitution is compatible with equivalence by induction. It turns out that, if we instead prove $(1)$ of Substitution commutes with change of $\lambda$ by induction, we will have some flexibility of manipulating binders in the $\lambda$ case, which allows us to complete the proof
  Corollary: Let $N, P, P'$ be terms and $x, y, z$ be variables, such that $y \not\equiv x, \lambda y. P \equiv \lambda z. P'$ and $z \notin FV(N) \cup {x}$, then $(\lambda y. P)[x := N] \equiv (\lambda z. P'[x := N])$

• Substitution is compatible with equivalence: For all $\lambda$ terms $P, N, P', N'$ and variable $x$, if $P \equiv P'$ and $N \equiv N'$, then $P[x:=N] \equiv P'[x:=N']$

• Substitution Lemma: Let $M, N, L \in \Lambda$. Suppose $x \not\equiv y$ and $x \notin FV(L)$, then $$M[x := N][y := L] \equiv M[y := L][x := N[y := L]]$$ Proof: Structural induction on $M$

  • $M$ is a variable:
    • $M = x$, then $\text{LHS} = \text{RHS} = N[y := L]$
    • $M = y$, then $\text{LHS} = \text{RHS} = L$
    • $M = z$ where $z \not\equiv x, z \not\equiv y$, then $\text{LHS} = z, \text{RHS} = z$
  • $M = P \ Q$: Trivial by induction hypothesis
  • $M = \lambda v. P$ where $v$ is a variable, then there exists a term $M' = \lambda z. Q$ such that $M' \equiv M$ and $z \notin {x, y} \cup AV(M) \cup FV(N) \cup FV(L)$. The $x = v$ case is easy. For the $x \neq z$ case, since substitution is compatible with equivalence, we only need to show that $M'[x := N][y := L] \equiv M'[y := L][x := N[y := L]]$. This can be verified through direct calculation, while making use of the corollary of Substitution commutes with change of $\lambda$

  Qed

• Substitution Rectification Lemma:

  • Inner Rectification: For all $\lambda$ terms $M, N$ and variables $x, y$, if $y \notin FV(M) \backslash {x}$, then $M[x:=N] \equiv M[x:=y][y:=N]$
  • Outer Rectification: For all $\lambda$ terms $M, N$ and variables $x, y, z$ if $z \notin (FV(M) \cup FV(N)) \backslash {y}$, then $M[x:=N] \equiv M[x:=N[y:=z]][z:=y]$

  Note:

  • The inner rectification lemma changes the name of the variable being substituted, and the outer rectification lemma changes the term that the variable is substituted to. When the premise of the substitution lemma does not hold, use substitution rectification lemma to make it possible to apply the substitution lemma.
  • For arbitrary $M[x:=N][y:=L]$, it is always possible to make the substitution lemma applicable by using the inner rectification lemma on $M[x:=N]$
  • In the Lean Code, Outer Rectification is proved first, and the proof of Inner Rectification uses Outer Rectification

• One-step $\beta$-reduction is compatible with $\alpha$ conversion: For all $\lambda$ terms $M, M', N, N'$ and variables $x, y$, if $\lambda x. M \equiv \lambda y. M'$ and $N \equiv N'$, then $M[x:=N] \equiv M[y:=N']$
  Note: This theorem is saying that, if $\lambda x. M \equiv \lambda y. M'$ and $N \equiv N'$, then the one-step leftmost $\beta$ reduction of $(\lambda x. M) N$ and $(\lambda x. M') N'$ are $\alpha$-equivalent

• Substitution Lemma's Friend: For all $\lambda$ terms $M, N, L$ and variables $x, y$, if $y \notin FV(M) \backslash {x}$, then $M[x:=N][y:=L] \equiv M[x:=N[y:=L]]$