====== Lambda kalkul ======
[[wp>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á!
* λ//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!
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, %%((%%λ//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
===== η-konverze =====
λ//V//.(//EV//) → //E// (//V// není volné v //E//)
===== Ekvivalence =====
* 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.