Lambda-arvutus
{$\lambda$}-termide süntaks: {$$ \begin{array}{lcl@{\hspace{5em}}l} e & ::= & x & \mbox{muutuja} \\ & \mid & (e_1\ e_2) & \mbox{aplikatsioon} \\ & \mid & (\lambda x.\ e) & \mbox{abstraktsioon} \end{array} $$}
Sulgudest hoidumine: {$$ \begin{array}{lcl} e_1\ e_2\ \ldots\ e_n & \equiv & ((\ldots(e_1\ e_2)\ldots)e_n) \\ \lambda x.\ e_1\ e_2\ \ldots\ e_n & \equiv & (\lambda x.\ (e_1\ e_2\ \ldots\ e_n)) \\ \lambda x_1\ x_2\ \ldots\ x_n.\ e & \equiv & (\lambda x_1.\ (\lambda x_2.\ (\ldots(\lambda x_n.\ e)\ldots)) \end{array} $$}
Näited: {$$ \begin{array}{l@{\hspace{7em}}l} \lambda x.\ x \;\;\;& ((\lambda x.\ (\lambda f.\ f\ x))\ y)\,(\lambda z.\ z) \end{array} $$}
Pane tähele:
- Puhas {$\lambda$}-arvutus „räägib“ ainult funktsioonidest.
- Arve ja teisi andmetüüpe eraldi ei ole, kuna neid saab defineerida {$\lambda$}-termidena.
- Mugavuse pärast kasutame siiski arve ja binaarseid operaatoreid nagu nad oleksid keelde sisseehitatud.
- Samuti kasutame makro-definitsioone (peavad olema mitterekursiivsed).
Näited: {$$ \begin{array}{lcl} \mathbf{add} & \equiv & \lambda x\,y.\ x + y\\ \mathbf{dbl} & \equiv & \lambda x.\ 2 * x\\ \mathbf{I} & \equiv & \lambda x.\ x\\ \mathbf{K} & \equiv & \lambda x\, y.\ x\\ \mathbf{S} & \equiv & \lambda f\,g\,x.\ f\,x\,(g\,x) \end{array} $$}
Vabad ja seotud muutujad
Muutuja {$x$} on vaba {$\lambda$}-termis {$e$} (so. {$x \in \textsf{FV}(e)$}), kui ta ei asu sümboli {$\lambda x$} mõjupiirkonnas.
Vastasel korral on {$x$} seotud.
Vabade muutujate induktiivne definitsioon:
{$$ \begin{array}{lcl} \textsf{FV}(x) & = & \{x\} \\ \textsf{FV}(e_1\ e_2) & = & \textsf{FV}(e_1)\ \bigcup\ \textsf{FV}(e_2) \\ \textsf{FV}(\lambda x.\ e) & = & \textsf{FV}(e)\ -\ \{x\} \end{array} $$}
Ilma vabade muutujateta {$\lambda$}-termid on kinnised.
Näited: termist vabade muutujate leidmine. {$$ \begin{array}{lcl} \textsf{FV}(\lambda x\, y.\ x\ y) & = & \emptyset \\ \textsf{FV}(\lambda x.\ (\lambda y. x)\,(\lambda z. y)) & = & \{ y \} \end{array} $$}
{$\alpha$}-konversioon
- Seotud muutujate nimed ei oma tähtsust!
- {$\lambda$}-termid {$e_1$} ja {$e_2$} on {$\alpha$}-kongruentsed (tähistus {$e_1 =_\alpha e_2$}) kui nad on identsed seotud muutujate ümbernimetamise täpsuseni.
Näited: {$$ \begin{array}{lcl} \lambda x.\ x & =_{\alpha} & \lambda y.\ y \\ \lambda x.\ f\ x & =_{\alpha} & \lambda z.\ f\ z \\ \lambda x.\ (\lambda y.\ y)\ x & =_{\alpha} & \lambda y.\ (\lambda y.\ y)\ y \\ \lambda x\ y.\ x + y & \not=_{\alpha} & \lambda y\ y.\ y + y \end{array} $$}
Substitutsioon
{$\lambda$}-arvutuse alusoperatsiooniks on formaalsete parameetrite asendamine tegelike argumentidega.
Avaldise {$(\lambda x.\,e_1)\, e_2$} väärtustamiseks tuleb termis {$e_1$} asendada muutuja {$x$} kõik vabad esinemised termiga {$e_2$}.
Substitutsiooni tähistame nii: {$e_1[{x} \mapsto {e_2}]$}.
Peab vältima vabade muutujate vangistamist.
Näited: {$$ \newcommand{\subst}[2]{[{#1} \mapsto {#2}]} \begin{array}{lcl} (\lambda x.\ y\,x)\subst{y}{\lambda z.\,z} & = & \lambda x.\ (\lambda z.\,z)\,x \\ (\lambda x.\ y\,x)\subst{x}{\lambda z.\,z} & = & \lambda x.\ y\,x \\ (\lambda x.\ y\,x)\subst{y}{\lambda z.\,x} & \not= & \lambda x.\ (\lambda z.\,x)\,x \end{array} $$}
Substitutsiooni definitsioon: {$$ \newcommand{\subst}[2]{[{#1} \mapsto {#2}]} \begin{array}{lcll} y\subst{x}{e} & = & \left\{ \begin{array}{l@{\hspace{2ex}}l} e & \mbox{if}\ x = y\\ y & \mbox{otherwise} \end{array}\right.\\[3ex] (e_1\,e_2)\subst{x}{e} & = & (e_1\subst{x}{e})\ (e_2\subst{x}{e})\\[3ex] (\lambda y.\,e_1)\subst{x}{e} & = & \left\{ \begin{array}{l@{\hspace{2ex}}l} \lambda y.\,e_1 & \mbox{if}\ x = y\\ \lambda y.\,e_1\subst{x}{e} & \mbox{if}\ y \not\in \textsf{FV}(e)\\ \lambda z.\,e_1\subst{y}{z}\subst{x}{e} & \mbox{otherwise} \end{array}\right. \end{array} $$}
kus {$z$} on värske muutuja (s.t. ta ei esine antud termides vabalt) .
Reduktsioon
{$\beta$}-reduktsioon
Alamavaldist kujul {$(\lambda x.\, e_1)\, e_2$}, puus alampuud kujul 
, nimetatakse ({$\beta$}-)reedeksiks.
NB! {$\lambda$}-termis võib olla palju reedekseid.
Ilma ({$\beta$}-)reedeksiteta {$\lambda$}-term on ({$\beta$}-)normaalkujul.
Näiteid ({$\beta$}-)reedeksite leidmisest termist: {$$ \newcommand{\subst}[2]{[{#1} \mapsto {#2}]} \begin{array}{l@{\hspace{3em}}l} \lambda x.\, x\,(\lambda y.\,x) & \mbox{reedekseid ei ole (so.\ normaalkuju)}\\[1ex] \lambda x.\,\underline{(\lambda y.\,y)\,3} & \mbox{üks reedeks} \\[1ex] \lambda f.\,f\,\underline{((\lambda x.\,x)\,3)}\ \underline{((\lambda x.\,x)\,4)} & \mbox{kaks reedeksit}\\[1ex] \underline{(\lambda f.\,f\,\underline{((\lambda x.\,x)\,3)})\ (\lambda x.\,x)} & \mbox{kaks (kattuvat) reedeksit} \end{array} $$}
{$\lambda$}-termide väärtustamine toimub reduktsiooni reeglite korduva rakendamise kaudu.
{$\beta$}-reduktsiooni reegel: {$$ (\lambda x.\, e_1)\, e_2\quad\rightarrow_\beta\quad e_1\subst{x}{e_2} $$}
Ühesammuline {$\beta$}-reduktsioon:
{$$ \newcommand{\subst}[2]{[{#1} \mapsto {#2}]} \newcommand{\infer}[3]{{#2}\\ \rule{#3}{1px} \\ {#1}} \infer{(\lambda x.\,e_1)\,e_2 \rightarrow_\beta e_1\subst{x}{e_2}}{}{10em}\\[2em] \infer{e_1\,e_0 \rightarrow_\beta e_2\,e_0}{e_1 \rightarrow_\beta e_2}{6em}\\[2em] \infer{e_0\,e_1 \rightarrow_\beta e_0\,e_2}{e_1 \rightarrow_\beta e_2}{6em} \\[2em] \infer{\lambda x.e_1 \rightarrow_\beta \lambda x.e_2}{e_1 \rightarrow_\beta e_2}{7em} $$}
Mitmesammuline {$\beta$}-reduktsioon
{$$ \newcommand{\infer}[3]{{#2}\\ \rule{#3}{1px} \\ {#1}} \infer{e_1 \twoheadrightarrow_\beta e_2}{e_1 \rightarrow_\beta e_2}{4em}\\[2em] \infer{e \twoheadrightarrow_\beta e}{}{3em}\\[2em] \infer{e_1 \twoheadrightarrow_\beta e_3}{e_1 \twoheadrightarrow_\beta e_2 \quad e_2 \twoheadrightarrow_\beta e_3}{8em}\\[2em] $$}
NB! Antud definitsioon ei määra reduktsioonide järjekorda. Näide: {$$ \begin{array}{lcl} \underline{(\lambda f.\,f\,((\lambda x.\,x)\,3))\ (\lambda x.\,x)} & \rightarrow_\beta & \underline{(\lambda x.\,x)\,((\lambda x.\,x)\,3))}\\ & \rightarrow_\beta & \underline{(\lambda x.\,x)\,3}\\ & \rightarrow_\beta & 3\\[1ex] (\lambda f.\,f\,\underline{((\lambda x.\,x)\,3)})\ (\lambda x.\,x) & \rightarrow_\beta & \underline{(\lambda f.\,f\,3)\ (\lambda x.\,x)}\\ & \rightarrow_\beta & \underline{(\lambda x.\,x)\,3}\\ & \rightarrow_\beta & 3\\ \end{array} $$}
{$\beta$}-konversioon: {$$ \newcommand{\infer}[3]{{#2}\\ \rule{#3}{1px} \\ {#1}} \infer{e_1 =_\beta e_2}{e_1 \twoheadrightarrow_\beta e_2}{4em}\\[2em] \infer{e_1 =_\beta e_2}{e_2 =_\beta e_1}{4em}\\[2em] \infer{e_1 =_\beta e_3}{e_1 =_\beta e_2 \quad e_2 =_\beta e_3}{7em} $$} {$\beta$}-ekspansioon: {$$ \newcommand{\infer}[3]{{#2}\\ \rule{#3}{1px} \\ {#1}} \infer{e_1 \twoheadleftarrow_\beta e_2}{e_2 \twoheadrightarrow_\beta e_1}{4em} $$}
{$\eta$}-reduktsioon
{$\eta$}-reduktsiooni reegel:
{$$ \lambda x.\, e\, x\quad\rightarrow_\eta\quad e \qquad\qquad x \notin\textsf{FV}(e) $$}
{$\eta$}-reduktsioon vastab funktsioonide ekstensionaalsuse omadusele
Reduktsiooni järjekorrad
Normaaljärjekord: alati redutseerida vasakpoolne väline reedeks.
Aplikatiivne järjekord: alati redutseerida vasakpoolne sisemine reedeks.
Vasakpoolne välimine või vasakpoolne sisemine siin juhul tähendab, et vaadata tuleb reedeksi asukohta puus:
- "Välimine" on see, mis on juurele kõige lähemal, ja "sisemine" vastavalt juurest kõige kaugemal.
- Kui mitu reedeksit on juurest samal kaugusel, siis "vasakpoolne" tähendab, et valime puus selle, mis asub kõige vasakumal pool.
Olgu meil näiteks term: {$$(\lambda x. x x) ((\lambda x.x) (\lambda x.x))$$} mis on puu kujul vastavalt:
Siis selle termi normaaljärjekorras ja aplikatiivjärjekorras redutseerimine käib järgnevalt:
Normaaljärjekorras:
{$$ \begin{align*} \underline{(\lambda x. x x) ((\lambda x.x) (\lambda x.x))} & \rightarrow_\beta\ && {\color{Blue3} xx[x \rightarrow ((\lambda x.x) (\lambda x.x))]} \\ \underline{((\lambda x.x) (\lambda x.x))} ((\lambda x.x) (\lambda x.x)) & \rightarrow_\beta && {\color{Blue3} x[x \rightarrow (\lambda x.x)]} \\ \underline{(\lambda x.x) ((\lambda x.x) (\lambda x.x))} & \rightarrow_\beta && {\color{Blue3} x[x \rightarrow ((\lambda x.x) (\lambda x.x))]} \\ \underline{(\lambda x.x) (\lambda x.x)} & \rightarrow_\beta && {\color{Blue3} x[x \rightarrow (\lambda x.x)]} \\ (\lambda x.x) & && \\ \end{align*} $$}
NB! Redutseerimise lahenduses võib võrduste paremad pooled (substitutsiooni välja kirjutamise) ära jätta.
Aplikatiivjärjekorras:
{$$ \begin{align*} (\lambda x. x x) (\underline{(\lambda x.x) (\lambda x.x)}) & \rightarrow_\beta && {\color{Blue3} x[x \rightarrow (\lambda x.x)]} \\ \underline{(\lambda x. x x) (\lambda x.x)} & \rightarrow_\beta && {\color{Blue3} xx[x \rightarrow (\lambda x.x)]} \\ \underline{(\lambda x.x) (\lambda x.x)} & \rightarrow_\beta && {\color{Blue3} x[x \rightarrow (\lambda x.x)]} \\ (\lambda x.x) && \\ \end{align*} $$}
Kui {$\lambda$}-termil leidub normaalkuju, siis on see saavutatav normaaljärjekorraga. Seetõttu on normaaljärjekord teoreetiliselt eelistatud -- välja arvatud järgneval juhul. Kui lambda kehas on parameetrit kasutatud mitmes kohas, "paljuneb" lambda keha sisse asendatud argument. Seetõttu võib olla kasulikum enne väärtustada argument.
Aplikatiivne järjekord on optimaalne, kui kõik redutseeritavad lambdad oma argumente ka reaalselt kasutavad.
Näiteks:
Normaaljärjekorras: {$$ \underline{(\lambda x.\,y) ((\lambda x.\,x\,x) (\lambda x.\,x\,x))} \ \rightarrow_\beta\ y $$}
Applikatiivjärjekorras: {$$ \begin{array}{ll} & (\lambda x.\,y) (\underline{(\lambda x.\,x\,x) (\lambda x.\,x\,x)}) \\ \rightarrow_\beta & (\lambda x.\,y) (\underline{(\lambda x.\,x\,x) (\lambda x.\,x\,x)}) \\ \ldots \end{array} $$}