Lambda kalkul
Syntaxe a konvence
E =
((…((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á!
λx.xy[x/y] 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!
β-redukce
Aplikace funkce, ((λ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í.
η-konverze
λV.(EV) → E (V není volné v E)
Ekvivalence
Výrazy jsou
identické1), když jsou zapsané stejnou posloupností symbolů.
Výrazy jsou si
rovné2), pokud se dají konverzemi a redukcemi převést na identické výrazy.