Uživatelské nástroje
msz:lambda
Toto je starší verze dokumentu!
Obsah
Lambda kalkul
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.yyDošlo k navázání volných proměnných!λx.xy → λx.xzy 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 voné proměnné, lze si pomoct α-přejmenováním a substitucí.
Příklad:
- ((λn.n×2) 7) → 7×2
η-konverze
Ekvivalence
/var/www/wiki/data/attic/msz/lambda.1338281954.txt.gz · Poslední úprava: (upraveno mimo DokuWiki)
Nástroje pro stránku
Kromě míst, kde je explicitně uvedeno jinak, je obsah této wiki licencován pod následující licencí: CC Attribution-Share Alike 4.0 International
