ВУЗ:
Составители:
9 Ламбда–исчисление
Желтая река течет тысячи миль на север…
Затем поворачивает на восток и течет непрерывно,
Не важно, как она изгибается и поворачивается,
Её воды выходят из источника на горе Кунь–Лунь.
Железная флейта
9.1 Ламбда–исчисление как формальная система
9.1.1 Значение ламбда–исчисления
Ламбда–исчисление было изобретено Алонсом Чёрчем около 1930 г. Чёрч перво-
начально строил λ–исчисление как часть общей системы функций, которая должна стать
основанием математики. Но из–за найденных парадоксов эта система оказалась противо-
речивой. Книга Чёрча [12] содержит непротиворечивую подтеорию его первоначальной
системы, имеющую дело только с функциональной частью. Эта теория и есть λ–
исчисление.
Ламбда–исчисление – это безтиповая теория, рас-
сматривающая функции как правила, а не как графики. В
противоположность подходу Дирихле (вводимому функ-
ции как множество пар, состоящих из аргумента и значе-
ния) более старое понятие определяет функцию как про-
цесс перехода от аргумента к значению. С первой точки
зрения x
2
–4 и (x+2)(x–2) – разные обозначения одной и той
же функции; со второй точки зрения это разные функции.
Что значит «функция 5x
3
+2»? Если кто–то хочет
быть точным, он вводит по этому поводу функциональный
символ, например f, и говорит: «функция f: R → R, опре-
деленная соотношением f(x) = 5x
3
+2». При этом, очевидно,
что переменную x можно здесь, не меняя смысла, заменить
на другую переменную y. Ламбда–запись устраняет произ-
вольность в выборе f в качестве функционального символа.
Она предлагает вместо f выражение «λx.5x
3
+2».
Алонсо Чёрч
Кроме того, обычная запись f(x) может обозначать как имя функции f, так и вызов
функции с аргументом x. Для более строгого подхода это необходимо различать. В лам-
бда–обозначениях вызов функции с аргументом x выглядит как (λx. 5x
3
+2)x.
Функции как правила рассматриваются в полной общности. Например, мы можем
считать, что функции заданы определениями на обычном русском языке и применяются к
аргументам также описанным по–русски. Также мы можем рассматривать функции задан-
ными программами и применяемые к другим программам. В обоих случаях перед нами
безтиповая структура, где объекты изучения являются одновременно и функциями и ар-
гументами. Это отправная точка безтипового λ–исчисления. В частности, функция может
применяться к самой себе.
Ламбда–исчисление представляет класс (частичных) функций (λ–определимые
функции), который в точности характеризует неформальное понятие эффективной вычис-
лимости. Другими словами, λ–исчисления, наряду с другими подходами формализует по-
нятие алгоритма [1, с. 143–146].
Ламбда–исчисление стало объектом особенно пристального внимания в информа-
тике после того, как выяснилось, что оно представляет собой удобную теоретическую мо-
дель современного функционального программирования [8].
51
Страницы
- « первая
- ‹ предыдущая
- …
- 49
- 50
- 51
- 52
- 53
- …
- следующая ›
- последняя »
