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