2.2. Meaning in L0
The context ctx records the binders currently in scope. A variable whose
name appears in the context becomes a de Bruijn index; otherwise it remains a
named free variable.
\begin{array}{rcl}
\llbracket x \rrbracket_\rho
&=& \begin{cases}
n & \rho(n) = x\\
x & x \notin \rho
\end{cases}\\
\llbracket \lambda x.\ e \rrbracket_\rho
&=& \lambda.\ \llbracket e \rrbracket_{x,\rho}\\
\llbracket e_1\ e_2 \rrbracket_\rho
&=& \llbracket e_1 \rrbracket_\rho\ \llbracket e_2 \rrbracket_\rho
\end{array}
The translation resolves a bound variable by its position in the context. Free variables are left as names, so open terms can still be represented.
namespace L1def toL0With (ctx : List String) : L1 -> L0
| .var x =>
(ctx.idxOf? x).elim (.free x) (.var)
| .lam x body =>
.lam (toL0With (x :: ctx) body)
| .app fn arg =>
.app (toL0With ctx fn) (toL0With ctx arg)def toL0 (t : L1) : L0 := toL0With [] t
Free variables are defined structurally on named terms. The theorem
fv_toL0With connects this visible definition to the free variables of the
translated L0 term.
\begin{array}{rcl}
FV(x) &=& \{x\}\\
FV(\lambda x.\ e) &=& FV(e) \setminus \{x\}\\
FV(e_1\ e_2) &=& FV(e_1) \cup FV(e_2)
\end{array}
Unlike L0, a lambda removes its bound name from the free-variable set.
The theorem following the definition says that this agrees with the translation
to L0.
def FV : L1 -> Set String
| .var x => {y | y = x}
| .lam x body => {y | y ∈ FV body ∧ y ≠ x}
| .app fn arg => {y | y ∈ FV fn ∨ y ∈ FV arg}def Closed (t : L1) : Prop :=
∀ x, x ∉ FV tTwo named terms are alpha-equivalent when they translate to the same de Bruijn term. The versions with environments are useful when the comparison happens under binders.
e =_\alpha e' \quad\text{iff}\quad
\llbracket e \rrbracket_\cdot = \llbracket e' \rrbracket_\cdot
In this development, alpha-equivalence is not another recursive relation on names. It means that the two terms have the same de Bruijn meaning.
def AlphaEqWith (ρ ρ' : List String) (s t : L1) : Prop :=
toL0With ρ s = toL0With ρ' tdef AlphaEqIn (ρ : List String) (s t : L1) : Prop :=
AlphaEqWith ρ ρ s tdef AlphaEq (s t : L1) : Prop :=
AlphaEqIn [] s tinfix:50 " =α₁ " => L1.AlphaEqabbrev BetaStep (s t : L1) : Prop := (toL0 s) →β₀ (toL0 t)infix:50 " →β₁ " => BetaStepabbrev BetaStar (s t : L1) : Prop := (toL0 s) →β₀* (toL0 t)infix:50 " →β₁* " => BetaStardef NormalForm (t : L1) : Prop := L0.NormalForm (toL0 t)
The alpha_eq tactic checks these small alpha-equivalence goals by reducing
both sides to L0.
syntax "alpha_eq" : tacticmacro_rules
| `(tactic| alpha_eq) =>
`(tactic|
simp_all [_root_.L1.AlphaEq, _root_.L1.AlphaEqIn, _root_.L1.AlphaEqWith,
_root_.L1.toL0, _root_.L1.toL0With,
List.idxOf?, List.findIdx?, List.findIdx?.go] <;> grind)