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:
{$$ \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} $$}
{$\beta$}-reduktsioon
{$\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} $$}
Alamavaldist kujul {$(\lambda x.\, e_1)\, e_2$} nimetatakse ({$\beta$}-)reedeksiks.
NB! {$\lambda$}-termis võib olla palju reedekseid.
Ilma ({$\beta$}-)reedeksiteta {$\lambda$}-term on ({$\beta$}-)normaalkujul.
Näited: {$$ \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} $$}
Ü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