Что такое лямбда в математике

Добавил пользователь Владимир З.
Обновлено: 20.09.2024

Ля́мбда-исчисле́ние (λ-исчисление, лямбда-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем, для формализации и анализа понятия вычислимости.

λ-исчисление может рассматриваться как семейство прототипных языков программирования. Их основная особенность состоит в том, что они являются языками высших порядков. Тем самым обеспечивается систематический подход к исследованию операторов, аргументами которых могут быть другие операторы, а значением также может быть оператор. Языки в этом семействе являются функциональными, поскольку они основаны на представлении о функции или операторе, включая функциональную аппликацию и функциональную абстракцию.

λ-исчисление реализовано Джоном Маккарти в языке Лисп. В начале реализация идей λ-исчисления была весьма громоздкой. Но по мере развития Лисп-технологии (прошедшей этап аппаратной реализации в виде Лисп-машины) идеи получили ясную и четкую реализацию.

Содержание

Чистое λ-исчисление

Это простейший из семейства прототипных языков программирования, чистое λ-исчисление, термы которого, называемые также объектами (обами), или λ-термами, построены исключительно из переменных применением аппликации и абстракции. Изначально наличия каких-либо констант не предполагается.

Аппликация и абстракция

В основу λ-исчисления положены две фундаментальные операции: аппликация и абстракция. Аппликация означает применение или вызов функции по отношению к заданному значению. Её обычно обозначают , где f — функция, а a — значение. Это соответствует общепринятой в математике записи f(a) , которая тоже иногда используется, однако для λ-исчисления важно то, что f трактуется как алгоритм, вычисляющий результат по заданному входному значению. В этом смысле аппликация f к a может рассматриваться двояко: как результат применения f к a , или же как процесс вычисления . Последняя интерпретация аппликации связана с понятием β-редукции.

Абстракция или λ-абстракция в свою очередь строит функции по заданным выражениям. Именно, если — выражение, свободно содержащее x , тогда обозначает функцию . Таким образом, с помощью абстракции можно конструировать новые функции. Требование, чтобы x свободно входило в t , не очень существенно — достаточно предположить, что , если это не так.

β-редукция

Поскольку выражение обозначает функцию, ставящую в соответствие каждому x значение , то для вычисления выражения

$(\lambda x. 2\cdot x + 1)\ 3$

в которое входят и аппликация и абстракция, необходимо выполнить подстановку числа 3 в терм . В результате получается . Это соображение в общем виде записывается как

$(\lambda x.t)\ a = t[x:=a],$

η-преобразование

$\lambda x.\ f x$

η-преобразование выражает ту идею, что две функции являются идентичными тогда и только тогда, когда, будучи применённые к любому аргументу, дают одинаковые результаты. η-преобразование переводит друг в друга формулы и f (в обратную сторону — только если x не имеет свободных вхождений в f : иначе свободная переменная x после преобразования станет связанной внешней абстракцией).

$\lambda x. f\ x$

Надо отметить, что если рассматривать лямбда-термы не как функции, а именно как алгоритмы, то данное преобразование не всегда уместно: существуют случаи, когда вычисление завершается, а вычисление f не завершается.

Каррирование (карринг)

Семантика бестипового λ-исчисления

Тот факт, что термы λ-исчисления действуют как функции, применяемые к термам λ-исчисления (то есть, возможно, к самим себе) приводит к сложностям построения адекватной семантики λ-исчисления. Можно ли приписать λ-исчислению какой-либо смысл? Желательно иметь множество D, в которое вкладывалось бы его пространство функций D → D. В общем случае такого D не существует по соображениям ограничений на мощности этих двух множеств, D и функций из D в D: второе имеет большую мощность, чем первое.

Эту трудность преодолел Д.С. Скотт, построив понятие области D (полной решётки [1] или, более общо, полного частично упорядоченного множества со специальной топологией) и урезав D → D до непрерывных (в имеющейся топологии) функций [2] . После этого также стало понятно, как можно строить денотационную семантику языков программирования. Это произошло благодаря тому, что с помощью конструкций Скотта можно придать значение также двум важным конструкциям языков программирования — рекурсии и типам данных.

Как уже говорилось ранее, в чистом бестиповом лямбда-исчислении отсутствует всё, кроме функций. Так что даже такие элементарные вещи, как числа или булевы значения необходимо реализовывать самим. Точнее, надо создать некие активные сущности, которые будут вести себя подобно необходимым нам объектам. И, естественно, процесс кодирования будет заключаться в написании соответствующих функций.

Начнём мы с самого простого: True и False . Два терма, воплощающие поведение этих констант, выглядят следующим образом:

tru = λt.λf.t	Двухаргументная функция, всегда возвращающая первый аргумент
fls = λt.λf.f	Двухаргументная функция, всегда возвращающая второй аргумент

Оператор if под такие булевы константы будет имеет вид:
if = λb. λx. λy.b x y
Здесь b — tru или fls , x — ветка then , y — ветка else .

Посмотрим, как это будет работать:
if fls t e

Поскольку условие if ложно ( fls ), то должно возвращаться выражение из ветки else ( e в нашем случае).

(λb. λx. λy. b x y) fls t e	по определению if
(λx. λy. fls x y) t e	редукция подчёркнутого выражения из предыдущей строки
(λy. fls t y) e	редукция подчёркнутого выражения из предыдущей строки
fls t e	редукция подчёркнутого выражения из предыдущей строки
(λt.λf. f) t e	по определению fls
(λf. f) e	редукция подчёркнутого выражения из предыдущей строки
e	редукция подчёркнутого выражения из предыдущей строки

or = λx.λy. x tru y

not = λx. x fls tru

Числа Чёрча

Мы с вами будем кодировать только натуральные числа, для чего вспомним аксиомы Пеано, определяющие их множество. В основе реализации по-прежнему будут лежать функции, ведущие себя в заданном контексте подобно единице, двойке и т.д. Собственно, это одна из особенностей лямбда-исчисления: сущности, записанные в его терминах, не обладают самодостаточностью, поскольку воплощают поведение того или иного объекта.

Итак, нам нужна функция, принимающая два аргумента: фиксированное начальное значение и функцию для определения следующего элемента (функцию следования). Число будет закодировано в количестве применений функции следования к начальному значению:

0 ≡ λs.λz. z	функция s применяется к начальному значению z нуль раз
1 ≡ λs.λz. s z	функция s применяется к начальному значению z один раз
2 ≡ λs.λz. s (s z)	функция s применяется к начальному значению z два раза
.	и так далее

Легко заметить, что нуль кодируется так же, как и логическое False. Тем не менее, не стоит делать из этого какие-либо далеко идущие выводы: это всего лишь совпадение.

Задача функции следования состоит в том, чтобы прибавить к заданному числу единицу. Т.е. в качестве аргумента она будет принимать значение, которое требуется увеличить, и которое тоже является функцией двух аргументов. Таким образом, суммарно функция (+1) имеет три аргумента: предшествующее число Чёрча n , функцию, которую надо будет применить n+1 раз к начальному значению, и само начальное значение. Выглядит это так:
scc = λn. λs. λz. s (n s z)
Здесь n s z — n раз применённая к z функция s . Но нам нужно применить её n+1 раз, откуда и берётся явное s (n s z) .

Арифметические операции

Сложение

Функция, осуществляющая сложение двух чисел Чёрча, будет принимать два слагаемых: x и y , которые в свою очередь тоже имеют по два аргумента — s (функцию следования) и z (начальное значение). Сложение будет состоять в том, чтобы сначала применить s к z x раз, а потом ещё y раз.

plus = λx. λy. λs. λz. x s (y s z)

В качестве примера сложим one = λs.λz. s z и two = λs.λz. s (s z) . Ответ должен будет выглядеть так: three = λs.λz. s (s (s z)) .

plus one two s' z'	s' и z' — чтобы не путать подставляемые значения с именами переменных
(λx. λy. λs. λz. x s (y s z)) one two s' z'	по определению plus
one s' (two s' z')	после проведения редукции
(λs.λz. s z) s' (two s' z')	по определению one
s' (two s' z')	после проведения редукции
s' (( λs.λz. s (s z) s' z')	по определению two
s' (s' (s' z'))	после проведения редукции
three s' z'	по определению three

Умножение

Функцию для умножения можно определить через функцию сложения. В конце-концов, умножить x на y означает сложить x копий y .

times = λx. λy. x (plus y) z

Есть ещё один способ определения умножения на числах Чёрча, без использования plus . Его идея заключается в том, что для получения произведения x и y нужно x раз взять y раз применённую к начальному значению функцию s :

times' = λx.λy.λs.λz. x (y s) z

Для примера умножим two = λs.λz. s (s z) на three = λs.λz. s (s (s z)) . Результат должен будет иметь вид: six = λs.λz. s (s (s (s (s (s z))))) .

times' two three s' z'	s' и z' — чтобы не путать подставляемые значения с именами переменных
(λx.λy.λs.λz. x (y s) z) two three s' z'	по определению times'
two (three s') z'	после проведения редукции
(λs.λz. s (s z)) (three s') z'	по определению two
three s' ((three s') z')	после проведения редукции
(λs.λz. s (s (s z))) s' ((three s') z')	по определению three
s' (s' (s' ((three s') z')))	после проведения редукции
s' (s' (s' (((λs.λz. s (s (s z))) s') z')))	по определению three
s' (s' (s' (( (λz. s' (s' (s' z))) z' )))	после проведения редукции
s' (s' (s' (s' (s' (s' z')))))	редукция подчёркнутого выражения
six s' z'	по определению six

Определите терм для возведения числа в степень

Для x в степени y :

power = λx.λy.λs.λz . y x s z

Заключение

Как видим, технически ничего сложного в лямбда-исчислении нет: всё сводится к элементарным подстановкам и редукциям. Но столь малого набора инструментов вполне хватает, чтобы при желании реализовать активные сущности, ведущие себя подобно парам, спискам, рекурсивным функциям и т.п. Они будут достаточно громоздкими, но, как уже говорилось, λ-исчисление предназначено не для написания программ, а для исследования и спецификации языков программирования и систем типов. С чем, собственно, и прекрасно справляется.

Лямбда-исчисление — это формальная система в математической логике для выражения подсчетов на основе абстракции и применения функций с использованием привязки и подстановки переменных. Это универсальная модель, которую можно применять для проектирования любой машины Тьюринга. Впервые введена лямбда-исчисления Черчем, известным математиком, в 1930-х годах.

Система состоит из построения лямбда-членов и выполнения над ними операций сокращения.

Пояснения и приложения

Греческая буква lambda (λ) используется в лямбда-выражениях и лямбда-терминах для обозначения связывания переменной в функции.

Лямбда-исчисление может быть нетипизировано или типизировано. В первом варианте функции могут быть применены только в том случае, если они способны принимать данные этого типа. Типизированные лямбда-исчисления слабее, могут выражать меньшее значение. Но, с другой стороны, они позволяют доказывать больше вещей.

Одной из причин того, что существует много разных типов — это желание ученых сделать больше, не отказываясь от возможности доказывать сильные теоремы лямбда-исчислений.

Система находит применение во многих различных областях математики, философии, лингвистики, и компьютерных наук. В первую очередь, лямбда-исчисления — это расчет, который сыграл важную роль в развитии теории языков программирования. Именно стили функционального создания реализуют системы. Они также являются актуальной темой исследований в теории этих категорий.

Для чайников

Лямбда-исчисление была введена математиком Алонзо Черчем в 1930-х годах в рамках исследования основ науки. Первоначальная система была показана как логически несовместимая в 1935 году, когда Стивен Клин и Дж. Б. Россер разработали парадокс Клини-Россера.

В последствии, в 1936 году Черч выделил и опубликовал только ту часть, которая имеет отношение к расчетам, то, что сейчас называется нетипизированным лямбда-исчислением. В 1940 он также представил более слабую, но логически непротиворечивую теорию, известную как система простого типа. В свое работе он объясняет всю теорию простым языком, поэтому, можно сказать, что Черч опубликовал лямбду исчисления для чайников.

До 1960-х годов, когда выяснилось его отношение к языкам программирования, λ стала лишь формализмом. Благодаря применениям Ричарда Монтегю и других лингвистов в семантике естественного языка, исчисление стало занимать почетное место как в лингвистике, так и в информатике.

Происхождение символа

Введение в лямбда исчисление

Система состоит из языка терминов, которые выбираются определенным формальным синтаксисом, и набора правил преобразования, которые позволяют манипулировать ими. Последний пункт можно рассматривать как эквациональную теорию или как операционное определение.

Все функции в лямбда-исчислении являются анонимными, то есть не имеющими имен. Они принимают только одну входную переменную, при этом каррирование используется для реализации графиков с несколькими непостоянными.

Лямбда-термины

Следующие три правила дают индуктивное определение, которое можно применять для построения всех синтаксически допустимых понятий:

Переменная x сама по себе является действительным лямбда-термином:

если T это ЛТ, и x непостоянная, то (lambda xt) называется абстракцией.
если T, а также s понятия, то (TS) называется приложением.

Ничто другое не является лямбда-термином. Таким образом, понятие действительно тогда и только тогда, когда оно может быть получено повторным применением этих трех правил. Тем не менее некоторые скобки могут быть опущены в соответствии с другими критериями.

Определение

Лямбда-выражения состоят из:

переменных v 1, v 2. v n.
символов абстракции 'λ' и точки '.'
скобок ().

Множество Λ, может быть определено индуктивно:

Если x переменная, то x ∈ Λ;
x непостоянная и M ∈ Λ, то (λx.M) ∈ Λ;
M, N ∈ Λ, то (MN) ∈ Λ.

Обозначение

Чтобы сохранить нотацию лямбда-выражений в незагроможденном виде, обычно применяются следующие соглашения:

Внешние скобки опущены: MN вместо (MN).
Предполагается, что приложения остаются ассоциативными: взамен ((MN) P) можно написать MNP.
Тело абстракции простирается дальше вправо: λx.MN означает λx. (MN), а не (λx.M) N.
Сокращается последовательность абстракций: λx.λy.λz.N можно λxyz.N.

Свободные и связанные переменные

Оператор λ соединяет свою непостоянную, где бы он ни находился в теле абстракции. Переменные, попадающие в область, называются связанными. В выражении λ x. М, часть λ х часто называют связующим. Как бы намекая, что переменные становятся группой с добавлением Х х к М. Все остальные неустойчивые называются свободными.

Множество свободных переменных M обозначается как FV (M) и определяется рекурсией по структуре терминов следующим образом:

FV (x) = , где x - переменная.
FV (λx.M) = FV (M) \ .
FV (MN) = FV (M) ∪ FV (N).

Формула, которая не содержит свободных переменных, называется закрытой. Замкнутые лямбда-выражения также известны как комбинаторы и эквивалентны терминам в комбинаторной логике.

Сокращение

Значение лямбда-выражений определяется тем, как они могут быть сокращены.

Существует три вида урезания:

α-преобразование: изменение связанных переменных (альфа).
β-редукция: применение функций к своим аргументам (бета).
η-преобразование: охватывает понятие экстенсиональности.

Здесь речь также идет о полученных эквивалентностях: два выражения являются β-эквивалентными, если они могут быть β-преобразованы в одно и то же составляющее, а α / η-эквивалентность определяется аналогично.

Термин redex, сокращение от приводимого оборота, относится к подтемам, которые могут быть сокращены одним из правил. Лямбда исчисление для чайников, примеры:

(λ x.M) N является бета-редексом в выражении замены N на x в M. Составляющее, к которому сводится редекс, называется его редуктом. Редукция (λ x.M) N есть M [x: = N].

Если x не является свободной в M, λ х. М х также ет-REDEX с регулятором М.

α-преобразование

Альфа-переименования позволяют изменять имена связанных переменных. Например, λ x. х может дать λ у. у. Термины, которые отличаются только альфа-преобразованием, называются α-эквивалентными. Часто при использовании лямбда-исчисления α-эквивалентные считаются взаимными.

Точные правила для альфа-преобразования не совсем тривиальны. Во-первых, при данной абстракции переименовываются только те переменные, которые связаны с одной и той же системой. Например, альфа-преобразование λ x.λ x. x может привести к λ y.λ x. х, но это может не ввергнуть к λy.λx.y Последний имеет иной смысл, чем оригинал. Это аналогично понятию программирования затенения переменных.

Во-вторых, альфа-преобразование невозможно, если оно приведет к захвату непостоянной другой абстракцией. Например, если заменить x на y в λ x.λ y. x, то можно получить λ y.λ y. у, что совсем не то же самое.

В языках программирования со статической областью видимости альфа-преобразование можно использовать для упрощения разрешения имен. При этом следя за тем, чтобы понятие переменной не маскировало обозначение в содержащей области.

В нотации индекса Де Брюйна любые два альфа-эквивалентных термина синтаксически идентичны.

Замена

Изменения, написанные Е [V: = R], представляют собой процесс замещения всех свободных вхождений переменной V в выражении Е с оборотом R. Подстановка в терминах λ определяется лямбдой исчисления рекурсии по структуре понятий следующим образом (примечание: x и y - только переменные, а M и N - любое λ-выражение).

y [x: = N] ≡ y, если x ≠ y

(M 1 M 2) [x: = N] ≡ (M 1 [x: = N]) (M 2 [x: = N])

(λ x.M) [x: = N] ≡ λ x.M

(λ y.M) [x: = N] y λ y. (M [x: = N]), если x ≠ y, при условии, что y ∉ FV (N).

Для подстановки в лямбда-абстракцию иногда необходимо α-преобразовать выражение. Например, неверно, чтобы (λ x. Y) [y: = x] приводило к (λ x. X), потому что замещенный x должен был быть свободным, но в итоге был связанным. Правильная замена в этом случае (λ z. X) с точностью до α-эквивалентности. Стоит обратить внимание, что замещение определяется однозначно с верностью до лямбды.

β-редукция

Бета-редукция отражает идею применения функции. Бета-восстановительный определяется в терминах замещения: ((X V. E) Е ') является Е [V: = Е'].

Например, предполагая некоторое кодирование 2, 7, ×, имеется следующее β-уменьшение: ((λ n. N × 2) 7) → 7 × 2.

Бета-редукция может рассматриваться как то же самое, что и концепция локальной сводимости при естественной дедукции через изоморфизм Карри – Ховарда.

η-преобразование

Эта-конверсия выражает идею экстенсиональности, которая в этом контексте заключается в том, что две функции равны тогда, когда они дают одинаковый результат для всех аргументов. Эта конвертация обменивает между λ x. (F x) и f всякий раз, когда x не кажется свободным в f.

Данное действие может рассматриваться как то же самое, что и концепция локальной полноты в естественной дедукции через изоморфизм Карри – Ховарда.

Нормальные формы и слияние

Для нетипизированного лямбда-исчисления β-редукция как правило переписывания не является ни сильно нормализующей, ни слабо.

Тем не менее можно показать, что β-редукция сливается при работе до α-преобразования (т. е. можно считать две нормальные формы равными, если возможно α-преобразование одной в другую).

Поэтому и сильно нормализующие члены, и слабо налаживающие понятия имеют единственную нормальную форму. Для первых терминов любая стратегия сокращения гарантированно приведет к типичной конфигурации. Тогда как для слабо нормализующих условий некоторые стратегии сокращения могут не найти ее.

Дополнительные методы программирования

Существует большое количество идиом создания для лямбда-исчисления. Многие из них были первоначально разработаны в контексте использования систем в качестве основы для семантики языка программирования, эффективно применяя их в качестве создания низкого уровня. Поскольку некоторые стили включают лямбда-исчисление (или что-то очень похожее) в качестве фрагмента, эти методы также находят применение в практическом создании, но затем могут восприниматься как неясные или чужие.

Именованные константы

В лямбда-исчислении библиотека принимает форму набора ранее определенных функций, в которой термины являются просто конкретными константами. Чистое исчисление не имеет понятия именованных неизменных, поскольку все атомные лямбда-термины являются переменными. Но их также можно имитировать, выделив непостоянную в качестве имени константы, используя лямбда-абстракцию для связывания этой изменчивой в основной части, и применить эту абстракцию к намеченному определению. Таким образом, если использовать f для обозначения M в N, можно сказать,

Авторы часто вводят синтаксическое понятие, такое как let, чтобы разрешить писать все в более интуитивном порядке.

Заметным ограничением этого let является то, что имя f не определено в M, поскольку M находится вне области привязки лямбда-абстракции f. Это означает, что атрибут рекурсивной функции не может использоваться как M с let. Более продвинутая синтаксическая конструкция letrec, которая позволяет писать рекурсивные определения функций в этом стиле, вместо этого дополнительно использует комбинаторы с фиксированной точкой.

Печатные аналоги

Данный тип является типизированным формализмом, который использует символ для обозначения анонимной функции абстракция. В этом контексте типы обычно являются объектами синтаксической природы, которые присваиваются лямбда-терминам. Точная натура зависит от рассматриваемого исчисления. С определенной точки зрения, типизированные ЛИ можно рассматривать как уточнения нетипизированного ЛИ. Но с другой стороны, их также можно считать более фундаментальной теорией, а нетипизированное лямбда-исчисление — особым случаем только с одним типом.

Типизированные ЛИ являются основополагающими языками программирования и основой функциональных, таких как ML и Haskell. И, более косвенно, императивных стилей создания. Типизированные лямбда-исчисления играют важную роль в разработке систем типов для языков программирования. Здесь типизируемость обычно захватывает желательные свойства программы, например, она не вызовет нарушения доступа к памяти.

Типизированные лямбда-исчисления тесно связаны с математической логикой и теорией доказательств через изоморфизм Карри – Говарда, и их можно рассматривать как внутренний язык классов категорий, например, который просто является стилем декартовых замкнутых.

Лямбда-функция в математике представляет собой показательную функцию, у которой число x возведено в степень самого себя, возведённого в (b−1):

$\lambda(x,b) = x^<x^<b-1></p> <p>>$

Если b стремится к бесконечности, то лямбда-функция стремится к 1 при |x| < 1, и к бесконечности при x >1.

Примечания

Weisstein, Eric W.Lambda Function (англ.) на сайте Wolfram MathWorld.

Wikimedia Foundation . 2010 .

Смотреть что такое "Лямбда-функция" в других словарях:

Лямбда-выражения — Лямбда выражение (в программировании) это специальный синтаксис для объявления анонимных функторов по месту их использования. Используя лямбда выражения, можно объявлять функции в любом месте кода. Обычно лямбда выражение допускает… … Википедия

Лямбда-исчисление — (λ исчисление) формальная система, разработанная американским математиком Алонзо Чёрчем, для формализации и анализа понятия вычислимости. λ исчисление может рассматриваться как семейство прототипных языков программирования. Их основная… … Википедия

Лямбда исчисление — (λ исчисление, лямбда исчисление) формальная система, разработанная американским математиком Алонзо Чёрчем, для формализации и анализа понятия вычислимости. λ исчисление может рассматриваться как семейство прототипных языков программирования. Их… … Википедия

Лямбда-выражение — В программировании лямбда или лямбда выражения это безымянная функция, объявляемая по месту ее непосредственного использования. Обычно лямбда допускает замыкание на лексический контекст, в котором она объявлена. Смотри также Лямбда исчисление… … Википедия

Функция высшего порядка — Функция высшего порядка функция, принимающая в качестве аргументов другие функции или возвращающая другую функцию в качестве результата. Основная идея состоит в том, что функции имеют тот же статус, что и другие объекты данных.… … Википедия

Однородная функция — степени числовая функция такая, что для любого и выполняется равенство: причём называют порядком однородности. Различают также положительно однородные функции, для которых равенство … Википедия

Рекурсивная функция (теория вычислимости) — У этого термина существуют и другие значения, см. Рекурсивная функция (значения). Термин рекурсивная функция в теории вычислимости используется для обозначения трёх классов функций примитивно рекурсивные функции; общерекурсивные функции; … Википедия

Примитивно рекурсивная функция — Термин рекурсивные функции в теории вычислимости используют для обозначения трёх множеств функций примитивно рекурсивные функции; общерекурсивные функции; частично рекурсивные функции. Последние совпадают с множеством вычислимых по Тьюрингу… … Википедия

Частично рекурсивная функция — Термин рекурсивные функции в теории вычислимости используют для обозначения трёх множеств функций примитивно рекурсивные функции; общерекурсивные функции; частично рекурсивные функции. Последние совпадают с множеством вычислимых по Тьюрингу… … Википедия

Читайте также: