De Bruijn indices

A representation of lambda terms without variable names: each variable is the number of binders between it and the lambda that binds it. Alpha-equivalent terms become identical and substitution cannot capture a variable, at the price of shifting indices when a term moves under a binder.

λ x . λ y . x \Rightarrow λ . λ . 1 λ x . x (λ y . x y) \Rightarrow λ . 0 (λ . 10)

The same variable can have different indices at different places, as $x$ does in the second term. With names, substitution has to avoid capture:

(λ y . x) [x := y] \neq = λ y . y

The free $y$ must not be captured by the binder, so named implementations rename bound variables first. With indices the question does not arise, because a free variable is a number larger than the binders around it, and substitution adjusts it when it goes under one. Shifting adds $d$ to the free variables of $t$ , those at or above the cutoff $c$ :

↑_{c}^{d} (k) = {k k + d k < c k \geq c ↑_{c}^{d} (λ . t) = λ . ↑_{c + 1}^{d} t ↑_{c}^{d} (t_{1} t_{2}) = ↑_{c}^{d} t_{1} ↑_{c}^{d} t_{2}

Substitution moves up a level under each binder, and β-reduction removes the binder and shifts back down:

[j \mapsto s] (λ . t) = λ . [j + 1 \mapsto ↑_{0}^{1} s] t (λ . t) s \to_{β} ↑_{0}^{- 1} ([0 \mapsto ↑_{0}^{1} s] t)

Shift, substitution, and normal-order normalization.

(* Variables are numbers: the count of binders between the use and its lambda. *)
type term = Var of int | Lam of term | App of term * term
 
(* shift d c t: add d to every variable of t that is free, i.e. >= c. *)
let rec shift d c = function
  | Var k -> Var (if k >= c then k + d else k)
  | Lam t -> Lam (shift d (c + 1) t)
  | App (a, b) -> App (shift d c a, shift d c b)
 
(* subst j s t: replace variable j in t by s. Under a binder, both move up. *)
let rec subst j s = function
  | Var k -> if k = j then s else Var k
  | Lam t -> Lam (subst (j + 1) (shift 1 0 s) t)
  | App (a, b) -> App (subst j s a, subst j s b)
 
let beta body arg = shift (-1) 0 (subst 0 (shift 1 0 arg) body)
 
let rec normal = function
  | App (f, a) -> (
      match normal f with
      | Lam body -> normal (beta body a)
      | f' -> App (f', normal a))
  | Lam t -> Lam (normal t)
  | Var k -> Var k
 
let rec show = function
  | Var k -> string_of_int k
  | Lam t -> "\\." ^ show t
  | App (f, (App _ as a)) -> show f ^ " (" ^ show a ^ ")"
  | App ((Lam _ as f), a) -> "(" ^ show f ^ ") " ^ show a
  | App (f, a) -> show f ^ " " ^ show a

Running it.

K                 =  \.\.1
K applied to free 0  ->  \.1
plus 2 2          ->  \.\.1 (1 (1 (1 0)))

$K$ applied to the free variable 0 gives $λ . 1$ : under the new binder, the same free variable is one further away. $plus 22$ normalizes to the Church numeral 4.

α-equivalence becomes syntactic equality, which is why type checkers and proof assistants use indices internally, or levels counted from the outside in, and names only for display. The locally nameless style uses indices for bound variables and names for free ones, so terms compare structurally and free variables stay readable.