Inference rules for lambda calculus

Lambda calculus consists of λ-expressions (λ-terms)

exp := var | app | abs
var := x | y | z                "x", "ID", ...
app := exp exp                  e1 e2
abs := 'λ' x '.' exp            (λx.e)

Inference rules (evaluator)

   t₁ -> t₁'
--------------- E-App1
t₁ t₂ -> t₁' t₂


   t₂ -> t₂'
--------------- E-App2
v₁ t₂ -> v₁ t₂'


(λx.t₁₂) v₂ -> [x ⟼ v₂] t₁₂     E-AppAbs

[x ⟼ v] t means to substitute all occurrences of x with v in t. It is like a let-expression, let x = v in t, or lambda app (\x -> t) v. It is a notation of β-reducing a lambda term, when a lambda abstraction is applied to a lambda term, but in also incorporates the notion of a substitution that is mindful of name capturing.

┌─ leftmost term: lambda abstraction ──────────────────────────┐
│                                                              │
│      ┌─ scope of x ────────────────────────────────────────┐ │
│      │                                                     │ │     a
│      │       ┌─ scope of g ──────────────────────────────┐ │ │   a r
│      │       │                                           │ │ │ a r g
│      │       │         ┌─ inner term ──────────────┐     │ │ │ r g 3
│      │       │         │                           │     │ │ │ g 2 │
│      │       │         │       ┌─ scope g' ────────┤     │ │ │ 1 │ │
│      │       │         │       │                   │     │ │ │ │ │ │
(λ   . ( λ   . ( 1 2 2 2 ( λ   . ( 1 3 3 3 3 3 ) 1 3 ) 2 3 ) ) ) y f h
(λ x . ( λ g . ( g x x x ( λ g . ( g x x x x x ) g x ) g x ) ) ) y f h
   │       │     │           │     │             │     │
   │       │     │           │     │             │     │
   │       │     │           │     │             │     │
   │       │     │           │     └ application occurrence of g'
   │       │     │           │                         │
   │       │     │           └ binding occurrence of g (must be renamed to g')
   │       │     │                                     │
   │       │     └ application occurrence of g ────────┘
   │       │
   │       └ binding occurrence of g
   │
   └ binding occurrence of x

From left to right:

• The top level lambda term is an application, distinguished by two lambda terms: the long one on the left, and a short one, z, on the right.

• We first encounter the binder with the binding occurrence of the parameter g.

• which we distinguish in the meta language by subscripting it with the index 1, as g₁.

• The first formal parameter is named g, and this is the binding occurrence of the parameter (variable) g,

binds the argument z, which means replacing all its application occurrences within its scope

, i.e. g₂ and g₄.

However, on a closer inspection, we see there is another binding occurrence of g at g₃ that has the application occurrence of g at g₄in its scope. That is, g₂ is bound by g₁ and g₄ by g₃. Name capturing would be to allow the first binding occurrence g₁ to also substitute g₄for parameter z, aside from the only occurrence it is supposed to substitute, i.e. that of g₂.

Therefore, we first need to rename (α-conversion) both occurrences of g that are to be treated as distinct bindings, and only then can we perform β-reduction i.e. application of the lambda to the argument z.

(λg. g x (λg. g x)) z      β-reduction: [g ⟼ z](g x (λg. g x))
    (z x (λg. z x))        NAME CAPTURE!

We must avoid name capture by first using α-conversion on the distinct but eponymously named occurrences.

(λg. g x (λg. g x)) z
(λg. g x (λf. f x)) z      α-conversion
    (z x (λf. f x)) z      β-reduction: [g ⟼ z](g x (λf. f x))