403
правки
Изменения
Нет описания правки
<tex>\lambda x \to f</tex> можно заменить на <tex>\lambda y \to f[x := y]</tex>, если <tex>y</tex> не входит свободно в <tex>f</tex>,
где <tex>f[x:=y]</tex> означает замену всех свободных вхождений <tex>x</tex> в <tex>f</tex> на <tex>y</tex>.
}}
Функции, получающиеся одна из другой с помощью <tex>\alpha</tex>-конверсий, называются
|definition=
Через <tex>f \to_\beta g</tex> обозначают сведение <tex>f</tex> к <tex>g</tex> с помощью одной <tex>\beta</tex>-редукции.
А через <tex>f \to_\beta^* g</tex>~{{--- }} за ноль или более.
}}
В оригинальном определении для обозначения переменных использовались имена,
и была проблема с тем, что не были запрещены одинаковые имена в разных
От этой проблемы можно избавиться следующим образом. Вместо имени переменной
будет храниться натуральное число~{{--- }} количество абстракций в дереве разбора,
на которое нужно подняться, чтобы найти ту лямбду, с которой данная переменная
связана. В данной нотации получаются несколько более простые определения
свободных переменных и $<tex>\beta$</tex>-редукции.
Переменная называется свободной, если ей соответствует число, которое больше
количества абстракций на пути до неё в дереве разбора.
При $<tex>\beta$</tex>-редукции же нужно будет ко всем свободным переменным заменяющего
дерева при каждой замене прибавить число, равное разницы уровней раньше и сейчас.
Это будет соответствовать тому, что эта переменная продолжит <<держаться>> за
ту же лямбду, что и раньше.
Введём на основе лямбда-исчисления аналог натуральных чисел, основанный на идее,
что натуральное число~{{--- }} это или ноль, или увеличенное на единицу натуральное
число.
<tex>\begin{code}zero' bar 0 = Lam "\lambda s" $ Lam "\to \lambda z" $ Var "\to z"</tex>one' <tex>\bar 1 = Lam "\lambda s" $ Lam "\to \lambda z" $ Var "\to s" `App` Var "z"</tex>two' <tex>\bar 2 = Lam "\lambda s" $ Lam "\to \lambda z" $ Var "\to s" `App` (Var "s" `App` Var "z")</tex>three' <tex>\bar 3 = Lam "\lambda s" $ Lam "\to \lambda z" $ Var "\tp s" `App` (Var "s" `App` (Var "s" `App` Var "z"))\end{code}</tex>
Каждое число будет функцией двух аргументов: какой-то функции и начального значения.
Число $<tex>n$ </tex> будет $<tex>n$ </tex> раз применять функцию к начальному значению и возвращать результат. Если такому <<числу>> дать на вход функцию $<tex>(+1)$ </tex> и $<tex>0$ </tex> в качестве
начального значения, то на выходе как раз будет ожидаемое от функции число:
Функция, прибавляющая 1 к числу, должна принимать первым аргументом число.
Но число~{{--- }} функция двух аргументов. Значит, эта функция должна принимать триаргумента: <<число>> $<tex>n$</tex>, которое хочется увеличить, функция, которую надо будет$<tex>n+1$ </tex> раз применить, и начальное значение.
<tex>\beginoperatorname{codesucc}succ' = Lam "\lambda n" $ Lam "\to \lambda s" $ Lam "\to \lambda z" $ Var "\to s" `App` (Var "n" `App` Var "s" `App` Var "z")\end{code}</tex>
Здесь $<tex>n s z$~<tex> {{--- $}} <tex>n$ </tex> раз применённая к $<tex>z$ </tex> функция $<tex>s$</tex>. Но нужно применить $<tex>n+1$ </tex> раз. Отсюда $<tex>s (n s z)$</tex>.
\subsection{Сложение}
