1.2. Substitution
Substitution has to pass under binders. When we cross a binder, the term being substituted must be shifted so that its free de Bruijn indices still refer to the same binders.
\begin{array}{rcl}
\uparrow_c(n) &=& \begin{cases}
n & n < c\\
n+1 & n \ge c
\end{cases}\\
\uparrow_c(x) &=& x\\
\uparrow_c(\lambda.\ e) &=& \lambda.\ \uparrow_{c+1}(e)\\
\uparrow_c(e_1\ e_2) &=& \uparrow_c(e_1)\ \uparrow_c(e_2)
\end{array}
The cutoff tells the shift operation which indices are protected by binders we have already crossed. The recursive definition below follows the displayed equations directly.
def shiftAbove (cutoff : Nat) : L0 -> L0
| .var k => .var (if k < cutoff then k else k + 1)
| .free x => .free x
| .lam body => .lam (shiftAbove (cutoff + 1) body)
| .app f a => .app (shiftAbove cutoff f) (shiftAbove cutoff a)def subst (j : Nat) (s : L0) : L0 -> L0
| .var k =>
if k = j then s
else if j < k then .var (k - 1)
else .var k
| .free x => .free x
| .lam body => .lam (subst (j + 1) (shiftAbove 0 s) body)
| .app f a => .app (subst j s f) (subst j s a)The basic substitution facts below say what substitution for the outermost variable does to variables. They are the calculation rules used by beta reduction examples.
\begin{array}{rcl}
[s/0]0 &=& s\\
[s/0](n+1) &=& n\\
[s/j]x &=& x
\end{array}
General substitution is defined above, but these three equations are the cases that show up most often when contracting a redex at the outermost binder.
theorem subst_var_zero : subst 0 s (.var 0) = s := s:L0⊢ subst 0 s (var 0) = s All goals completed! 🐙theorem subst_var_succ : subst 0 s (.var (n + 1)) = .var n := s:L0n:ℕ⊢ subst 0 s (var (n + 1)) = var n All goals completed! 🐙theorem subst_free : subst j s (.free x) = .free x := j:ℕs:L0x:String⊢ subst j s (free x) = free x All goals completed! 🐙