Изменения
Нет описания правки
связана. В данной нотации получаются несколько более простые определения
свободных переменных и <tex>\beta</tex>-редукции.
Грамматику нотации можно задать как:
:<tex>e\ ::= n\ |\ \lambda .e\ |\ e\ e</tex>
Примеры выражений в этой нотации:
:<tex>
\begin{tabular}{cc}
Standart & de Bruijn \\
$\lambda x.x$ & $\lambda .0$ \\
$\lambda z.z$ & $\lambda .0$ \\
$\lambda x. \lambda y.x$ & $\lambda . \lambda .1$\\
$\lambda x. \lambda y. \lambda s. \lambda z.x\ s\ (y\ s\ z)$ & $\lambda . \lambda . \lambda . \lambda .3\ 1(2\ 1\ 0)$\\
$(\lambda x.x\ x)(\lambda x.x\ x)$ & $(\lambda .0\ 0)(\lambda .0\ 0)$\\
$(\lambda x. \lambda x.x)(\lambda y.y)$ & $(\lambda .\lambda .0)(\lambda .0)$\\
\end{tabular}
</tex>
Переменная называется свободной, если ей соответствует число, которое больше
