====== 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//′.

<note important>Žádná volná proměnná v //E//′ se nesmí po substituci stát vázanou!</note>
<note>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á!
</note>
===== α-konverze =====
Někdy také α-přejmenování.

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

<note important>Nesmí dojít k navázání volných proměnných!</note>

<note>Příklad:
  * λ//x//.//xy// → λ//z//.//zy//
  * <del>λ//x//.//xy// → λ//y//.//yy//</del> Došlo k navázání volných proměnných!
  * <del>λ//x//.//xy// → λ//x//.//xz//</del> //y// není vázaná proměnná (šlo o substituci)
</note>

===== β-redukce =====
Aplikace funkce, %%((%%λ//V//.//E//) //E//′) → //E//[//E//′%%/%%//V//].

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

<note important>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í.</note>

<note>Příklad:
  * %%((%%λ//n//.//n//×2) 7) → 7×2
</note>
===== η-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.