Kalábovi

Kalábovic wikina

Uživatelské nástroje

Nástroje pro tento web


pitel:msz:lambda

Lambda kalkul

Syntaxe a konvence

E =

  • V – proměnná
  • (EE₂) – aplikace
  • λ(V.E) – abstrakce, V je hlavička, E je tělo

  • ((…((EE₂) E₃)…) Eₙ) ~ EEE₃ … 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é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.
1)
2)
=
/var/www/wiki/data/pages/pitel/msz/lambda.txt · Poslední úprava: 03. 07. 2012, 13.53:31 (upraveno mimo DokuWiki)