Jednoduchý výpočetní model, který je Turingovsky úplný. Má jen tři konstrukty:
- proměnné --
a, b, c, ... - aplikace výrazů --
(E F)(pozor, je zleva asociativní) - lambda abstrakci (vytvoření nové funkce) --
(\x. E)Dále budu označovat proměnné malými písmenky a výrazy velkými písmenky...
K tomu má jedno vyhodnocovací pravidlo ⇝:
(\x. E) F ⇝ E [ x := F ]
Slovy: pokud aplikujeme funkci s argumentem x vracející E na výraz F,
dostaneme výraz E, ve kterém všechny výskyty x nahradíme za F.
Dodejme, že funkce jsou ekvivalentní, pokud jen stačí přejmenovat proměnné, aby byly identické.
Zkusme vyhodnotit následující výraz:
(\x. x) c
pro nějakou konstantu c.
Očividně je ta funkce vlevo identita --- vrátí přímo to, co dostane.
Naše intuice nám tedy napovídá, že bychom měli dostat zpátky zase c.
Použijeme tedy vyhodnocovací pravidlo výše:
(\x. E) F
(\x. x) c
a máme dostat E [x := F], což je v našem případě x [x := c].
Tedy nám vyjde c a jsme spokojeni :)
Mějme identitu aplikovanou na identitu:
(\x. x) (\y. y)
Použijeme vyhodnocovací pravidlo výše:
(\x. E) F
(\x. x) (\y. y)
a máme dostat E [x := F], což je v našem případě x [x := (\y. y)].
Tedy nám vyjde (\y. y).
Všimněte si, že máme jen funkce s jedním argumentem. Co kdybychom chtěli argumentů víc?
Funkci dvou argumentů můžeme vyrobit následovně:
Vezmeme funkci s jedním argumentem x, která vrátí funkci s jedním argumentem y,
která teprve vrátí "tělo" funkce E: \x. (\y. E).
Často se díky této vlastnosti píše dle výrazu výše jen zkráceně jako \x y. E.
Abychom mohli psát hezky f x y s významem f(x, y),
pak dle výše uvedeného musí být aplikace nutně asociativní zleva!
Tedy nejprve se aplikuje f na x a až potom se výsledek aplikuje na y.
Zapsáno znaky: f x y == (f x) y.
Například:
% term(+LambdaKalkulovyTerm) určuje, jestli je daný lambda kalkulový term validní
term(var(X)).
term(lam(X, E)) :- term(E).
term(app(A, B)) :- term(A), term(B).Výraz (\x. x) (\y. y) pak můžeme napsat jako app(lam(x, var(x)), lam(y, var(y))) :)
Tohle je jen bonus!
Čísla můžeme reprezentovat podobně jako v Prologu / v Teorii množin.
Jako nulu prohlásíme výraz (\s. (\z. z)), ve zkrácené notaci tedy (\s z. z)
Jako jedničku výraz (\s. (\z. s z)), ve zkrácené notaci (\s z. s z).
Jako dvojku výraz (\s z. s (s z)) a tak dále...
Matematicky je číslo n funkce, která vezme funkce s a z
a aplikuje funkci s n-krát na funkci z.
Vypadá to skoro, jako kdyby z = 0 a s = (+1) (přičtení jedničky).
Také jsme si ukazovali funkci (\n. (\s z. s (n s z))), která k danému číslu přičte jedničku
(reálně je to successor funkce/funkce vracející následníka daného čísla)
a zkoušeli jsme ji zavolat na jedničku a ukázali jsme si, že to je dvojka.
Pokud tedy jako ⟦0⟧ označím nulu a jako S označím funkci následníka výše, pak:
⟦0⟧ = λ s z . z
⟦1⟧ = ⟦S0⟧
= (λ n . λ s z . s (n s z))(λ s′ z′ . z′)
⇝ λ z s . s ((λ s′ z′ . z′) s z)
⇝ λ z s . s ((λ z′ . z′) z)
⇝ λ z s . s z
⟦2⟧ = ⟦SS0⟧
= (λ n . λ s z . s (n s z))((λ n′ . λ s′ z′ . s′ (n′ s′ z′))(λ s″ z″ . z″))
⇝ (λ n . λ s z . s (n s z))(λ s′ z′ . s′ ((λ s″ z″ . z″) s′ z′))
⇝ (λ n . λ s z . s (n s z))(λ s′ z′ . s′ z′)
⇝ λ z s . s ((λ s′ z′ . s′ z′) s z)
⇝ λ z s . s (s z)
Cvičení: Naprogramujte součet dvou čísel! Rozmyslete si jak to děláte induktivně v Prologu a jen to převeďte do lambda kalkulu :) Tedy rozmyslete si, že musí platit:
m + 0 = m
m + Sn = S(m + n)
a napište funkci PLUS, která vezme dvě čísla a sečte je.
Obecně se podobně dají reprezentovat i jiné konstrukce jako if a booleany, nebo spojové seznamy,
nebo dvojice. Více detailů se dá najít na wiki: https://en.wikipedia.org/wiki/Church_encoding
Něčím podobným se ale budeme zabývat příště rovnou v Haskellu...