Lambda kalkul [Kalábovi]

¹⁾

λV.E) E′) → E[E′/V].

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

Opět pozor na vázané a volné proměnné! Volné proměnné v E′ se nesmí stást vázanými! Lze si pomoct α-přejmenováním a substitucí.

Příklad:

((λn.n×2) 7) → 7×2 </note> ===== η-konverze ===== λV.(EV) → E (V není volné v E) ===== Ekvivalence =====
- Výrazy jsou identické((≡
²⁾
=
³⁾
Lambda kalkul

Lambda calculus

Syntaxe a konvence
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
Volné a vázané proměnné
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
 | |   | |
 +-+   +-+
```
Substituce
E[E′/V] (někdy také E[V := E′])

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

Žádná volná proměnná v E′ se nesmí po substituci stát vázanou!
Příklad:

λx.xy[vw/y] = λx.xvw

λx.xy[vw/x] nelze, protože x je vázaná proměnná!
α-konverze
Někdy také α-přejmenování.

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

Nesmí dojít k navázání volných proměnných!
Příklad:

λx.xy → λz.zy

~~λx.xy → λy.yy~~ Došlo k navázání volných proměnných!

~~λx.xy → λx.xz~~ y není vázaná proměnná (šlo o substituci)
β-redukce

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

Kalábovi