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...