de bruijn index
λx.x ≡ₐ λy.y => without names λx.x = λ.0 λx.λy.x y ≡ λ.λ.1 0 λx.x(λy.x y) λ.0(λ.1 0)
de bruijn expression
M ::= n n ::= 0 | 1 | 2 | ... e ≡ M
λx e₁ e₂ λx /
e₁ e₂
λx(x(λy x y)) (λz x z)
λ(0(λ 1 0)) (λ 1 0)
substitutions using de bruijn expr
λ-calculus → operational sematic → substitutions
(λx e)e' ↦ [e'|x]e (λ M) N ↦ σ(M, N) - find 0 in M - replace it with N
λλ(λ 2 1 0) (λ 0) - redex ↦ λλσ(2 1 0, λ 0) ↦ λλ1 0 λ 0
λλ (λ λ3 2 1 0) (λ 0) ——– M: λ 3 2 1 0 ↦ λλ λ2 1 (λ 0) 0
e₁: (x(λy x y)) e₂: (λz x z)
σ₀(M, N) 0->N σ₀(λM, N) = λσ₁(M, N) - find 1 in M - replace it with N
σᵢ(M,N)
σᵢ(M₁ M₂, N) = σᵢ(M₁,N) σᵢ(M₂,N) σᵢ(λM,N) = λσ_i+1(M,N) σᵢ(i, N) = N σᵢ(j, N) = j j < i σᵢ(j, N) = j - 1 j > i
σᵢ(i, N) = N closed N has free varibles σᵢ(j, N) = j j < i
de bruijin shifting
σᵢ(i,N) = N -> has free vars failed
σ₀(λλ...λi,N) = λλ...λσᵢ(i,N)
N - local var - same free variables λλ...λ σᵢ(i,N) = N - free variables in N - shift by i
λλ(λ 0)(λ 2 1 0) 21 0 ↦λλ(λ2 1 0) 21
λλ(λ(λ 1) 0)(λ 2 1 0) λλ( λ (λ 2 1 0)) (λ 2 1 0)
λλ( λ (λ 3 2 0)) (λ 2 1 0)
σᵢ(i,N) = τ₀ⁱ(N) - find free vars in N - shift by i
>= 0 => freeτ₀ⁱ(λ N) = λτ₁ⁱ(N) free var >= 0 free var >= 1 τ₁ⁱ(λ N) = λτ₂ⁱ(N)
τⱼⁱ(N) = find free vars in N free vars ≥ j shift by i
τⱼⁱ(N₁ N₂) = τⱼⁱ(N₁) τⱼⁱ(N₂) τⱼⁱ(λ N) = λτⱼ₊₁ⁱ(N) τⱼⁱ(k) = k + i k = free var k≥j τⱼⁱ(k) = k k ≠ free var k<j