Lambda calculus

E =

• V – proměnná
• (E₁ E₂) – aplikace
• λ(V.E) – abstrakce, V je hlavička, E je tělo

• ((…((E₁ E₂) E₃)…) Eₙ) ~ E₁ E₂ E₃ … Eₙ
• (λV.(E₁ … Eₙ)) ~ λV.E₁ … Eₙ
• (λV₁.(…(λVₙ.E))) ~ λV₁ … Vₙ.E

Proměnná je vázaná, pokud se vyskutuje v (nejbližší) hlavičce lambda abstrakce. V opačném případě je proměnná volná.

λx.xy(λx.x)y
 | |   | |
 +-+   +-+

E[E′/V] (někdy také E[V := E′])

Nahrazení volných výskytů V v E za E′.

Někdy také α-přejmenování.

Přejmenovává vázané proměnné.

Aplikace funkce, ((λV.E) E′) → E[E′/V].

  +--+
  |  V
(λxy.xy)(ab) → λy.aby
  ^      |/
  |      |
  +------+

λV.(EV) → E (V není volné v E)

• Výrazy jsou identické¹⁾, když jsou zapsané stejnou posloupností symbolů.
• Výrazy jsou si rovné²⁾, pokud se dají konverzemi a redukcemi převést na identické výrazy.