1302
правки
Изменения
удалил неуместный баннер
'''Лямбда-исчисление''' (''англ. lambda calculus'') {{---}} формальная система, придуманная в 1930-х годах
Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией.
дереве разбора были абстракции. Все остальные переменные называются свободными.
Например, в <tex>\lambda x\ .\ \lambda y\ .\ x</tex>, <tex>x</tex> и связана, а <tex>y</tex>{{---}} свободна. А в <tex>\lambda y\ .\ x\ (\lambda x\ .\ x)</tex>
в своём первом вхождении переменная <tex>x</tex> свободна, а во втором {{---}} связана.
{{Определение
|definition=
'''<tex>\beta</tex>-редукция''' (англ. ''<tex>\beta</tex> -reduction'') {{---}} это наименьшее соотношение на <tex>\Lambda</tex> такое что
:<tex>(\lambda x.P)Q\to _\beta P[x:=Q]</tex>
и замкнуто относительно следующих правил
}}
В <tex>\beta</tex>-редукции вполне возможна функция вида <tex>\lambda x. \lambda x.x</tex>. Во время подстановки вместо <tex>x</tex> внутренняя переменная не заменяется - действует принцип локальной переменной. Но принято считать, что таких ситуаций не возникает и все переменные называются разными именами.
===Каррирование===
Примеры выражений в этой нотации:
Переменная называется свободной, если ей соответствует число, которое больше
===+1===
Функция, прибавляющая <tex>1 </tex> к числу, должна принимать первым аргументом число.
Но число {{---}} функция двух аргументов. Значит, эта функция должна принимать три
аргумента: "число" <tex>n</tex>, которое хочется увеличить, функция, которую надо будет
===Комбинатор неподвижной точки===
Попробуем выразить в лямбда-исчислении какую-нибудь функцию, использующую рекурсию. НапрмерНапример, факториал.
<tex>\operatorname{fact} = \lambda x\ .\ \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{fact}\ (\operatorname{pred}\ x))</tex>
===Проверка на простоту===
<tex>\operatorname{isPrimeHelp}</tex> {{---}} принимает число, которое требуется проверить на простоту и то, на что его надо опытаться поделить, перебирая это от <tex>2 </tex> до <tex>p-1</tex>. Если на что-нибудь разделилось, то число {{---}} составное, иначе {{---}} простое.
<tex>\operatorname{isPrimeHelp'} =</tex><tex>\lambda f\ .\ \lambda p\ .\ \lambda i\ .\ \operatorname{if}\ (\operatorname{le}\ p\ i)\ \operatorname{true}\ (\operatorname{if}\ (\operatorname{isZero}\ (\operatorname{mod}\ p\ i))\ \operatorname{false}\ (f\ p\ (\operatorname{succ}\ i)))</tex>