Lambda arvutus15. Apr '14
Kõige lihtsam lambda termin tagastab oma argumendi:
\begin{equation*}
\lambda x . x
\end{equation*}
Pythoni analoog:
lambda x: x
Funktsioon mis rakendab argumenti argumendi enda peal:
\begin{equation*}
\lambda x . x\:x
\end{equation*}
Sisuliselt sama väljend Pythonis:
lambda x: x(x)
Notatsioon
The body of an abstraction extends as far right as possible: λx.M N means λx.(M N) and not (λx.M) N
Misc
Vasakassotsiatiivne:
Body of abstraction ends as far as possible
\begin{equation*}
\lambda x . E_1 E_2 \equiv \lambda x . (E_1 E_2)
\end{equation*}
\begin{equation*}
\lambda x . \lambda y E_1 E_2 \equiv \lambda x . (\lambda y. E_1 E_2)
\end{equation*}
alpha-conversion: terms differing only in bound variable names are equivalent beta-reduction: evaluate expressions, function application:
\begin{equation*}
(\lambda x . x + 1) 5 \rightarrow_{\beta} 5+1 \equiv 6
\end{equation*}
Pythoni analoogne kood:
>>> (lambda x: x + 1)(5) 6
\begin{equation*}
(\lambda x . \lambda y . x + y)(5\:6) \rightarrow_{\beta} 5 \times 6 \equiv 30
\end{equation*}
Substitution rules:
\begin{equation*}
v[v \rightarrow E] \equiv E
\end{equation*}
\begin{equation*}
x[v \rightarrow E] \equiv x
\end{equation*}
\begin{equation*}
c[v \rightarrow E] \equiv c
\end{equation*}
\begin{equation*}
(E_1 E_2) [v \rightarrow E] \equiv (E_1[v \rightarrow E] E_2[v \rightarrow E])
\end{equation*}
\begin{equation*}
(\lambda v . E_1
\end{equation*}
Näide
\begin{equation*}
(\lambda x . x\:x)(\lambda y . y)3
\end{equation*}
Pythoni analoog:
(lambda x:x(x)) (lambda y:y) (3)
Esialgse valemi võib ümber kirjutada järgnevalt:
\begin{equation*}
\big [(x\:x)(x \rightarrow \lambda y . y) \big ] 3
\end{equation*}
\begin{equation*}
\Big[ \big( x[x \rightarrow \lambda y . y])(x [x \rightarrow \lambda y . y] \big) \Big] 3
\end{equation*}
\begin{equation*}
\big [(\lambda y.y)(\lambda y.y) \big ] 3
\end{equation*}
Asendamine:
\begin{equation*}
[y(y \rightarrow \lambda y . y)] 3 \equiv (\lambda y . y)3 \equiv 3
\end{equation*}