Что такое лямбда исчисление

Лямбда-исчисление

В этой главе мы узнаем о лямбда-исчислении. Лямбда-исчисление описывает понятие алгоритма. Ещё до появления компьютеров в 30-е годы двадцатого века математиков интересовал вопрос о возможности создания алгоритма, который мог бы на основе заданных аксиом дать ответ о том верно или нет некоторое логическое высказывание. Например у нас есть базовые утверждения и логические связки такие как “и”, “или”, “для любого из”, “существует один из”, с помощью которых мы можем строить из базовых высказываний составные. Некоторые из них окажутся ложными, а другие истинными. Нам интересно узнать какие. Но для решения этой задачи прежде всего необходимо было понять а что же такое алгоритм?

Ответ на этот вопрос дали Алонсо Чёрч (Alonso Church) и Алан Тьюринг (Alan Turing). Чёрч разработал лямбда-исчисление, а Тьюринг теорию машин Тьюринга. Оказалось, что задача автоматического определения истинности формул в общем случае не имеет решения.

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

В рамках теории машин Тьюринга алгоритм описывается по-другому. Машина Тьюринга имеет внутреннее состояние, Состояние содержит некоторое значение, которое изменяется по ходу работы машины. Машина живёт не сама по себе, она читает ленту символов. Лента символов – это большая цепочка букв. На каждую букву машина реагирует серией действий. Она может изменить значение состояния, обновить букву в ленте или перейти к следующему или предыдущему символу. Есть состояния, которые обозначают конец работы, они называются терминальными. Как только машина дойдёт до терминального состояния мы считаем, что вычисление алгоритма закончилось. После этого мы можем считать результат из состояний машины.

Функциональные языки программирования основаны на лямбда-исчислении. Поэтому мы будем говорить именно об этом описании алгоритма.

Лямбда исчисление без типов

Составление термов

Можно считать, что лямбда исчисление это такой маленький язык программирования. В нём есть множество символов, которые считаются переменными, они что-то обозначают и неделимы. В лямбда-исчислении программный код называется термом. Для написания программного кода у нас есть всего три правила:

$$(((Fun\ Arg1)\ Arg2)\ Arg3)$$

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

Источник

Бестиповое лямбда-исчисление, комбинаторы, Unlambda и числа Фибоначчи

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

Для знатоков: статья скорее имеет целью объяснить, как это работает, нежели дать строгое формальное описание.

λ-исчисление было изобретено Алонзо Чёрчем для формализации понятия алгоритма и вычислимости. Функции в λ-исчислении следует понимать именно так — как некий алгоритм, обрабатывающий входные данные.

Бестиповое λ-исчисление

Предположим, что у нас есть функции от одного аргумента. Причем и их аргумент, и возвращаемое значение — тоже функции от одного аргумента.

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

Тогда λx.f x = f, так как эта функция принимает аргумент x и возвращает значение f x, что и делает сама функция f. Это называется η-преобразованием.

Несложно набросать тождественную функцию, просто возвращающую свой аргумент: λx.x
Функция-константа тоже не вызывает осложнений: λx.c, где c не зависит от x. Действительно, при любом аргументе функция возвратит c.
Казалось бы, вот и все. Мы ведь даже не умеем строить функции от нескольких аргументов! Да нет, умеем, просто мы пока об этом не знаем.

Рассмотрим такой пример: λx.λy.x+y. Для большей наглядности, расставим скобки: λx.(λy.(x+y)) — это функция, возвращающая другую функцию, возвращающую сумму. Как это работает? Давайте применим ее к некоторому аргументу: (λx.(λy.(x+y))) a = λy.(a+y). Получившуюся функцию применим к другому аргументу: (λy.(a+y)) b = a+b. Такой прием называется карринг, или каррирование (в честь Хаскелла Карри), и работает для любого числа аргументов. Договоримся, что если функция имеет вид λx.(λy.(λz.(F))), то мы будем записывать её как λxyz.F. Ещё договоримся, что (f a b c) обозначает
(((f a) b) c). Теперь функции многих аргументов записываются очень просто: λxy.x+y, а их применение — (f a b).

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

Управляющие конструкции

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

Теперь попробуем решить классическую задачу на циклы и рекурсию — вычисление факториала. Пусть у нас уже реализованы числа, арифметические операции (которые мы теперь будем записывать в префиксной нотации, в стиле λ-исчисления), функция dec, уменьшающая свой аргумент на 1, а также функция zero, с помощью которой мы можем проверить число на равенство нулю.
g = λrn.(zero n) 1 (* n (r r (dec n)))
Посмотрим внимательно: функция проверяет n на равенство нулю, возвращает 1 в случае успеха, иначе возвращает (* n (r r (dec n))) — произведение n и значения некой функции r от самой себя и n-1. Что такое функция r? Это своего рода хак, чтобы сделать рекурсию — в качестве r мы будем передавать саму функцию g, а значит написанное выражение действительно вычисляет факториал: g(n) = n * g(n-1). Так как неудобно каждый раз передавать функции саму себя, сделаем такую окончательную реализацию факториала:
f = g g
Таким образом, g «запомнит» свой первый аргумент, и останется только передать ей нужное число для вычислений.

Комбинатор неподвижной точки

Оказывается, в лямбда-исчислении для любой функции f существует такой аргумент x, что f x = x. Более того, этот x всегда можно найти! Эту работу выполняет так называемый комбинатор неподвижной точки. Один из его вариантов, придуманный нашим любимым Хаскеллом Карри:
Y = λf.(λx.f (x x)) (λx.f (x x))
Посмотрим, как это работает:
Y f = (λx.f (x x)) (λx.f (x x)) = f ((λx.f (x x)) (λx.f (x x))) = f (Y f)
Таким образом, Y f — действительно неподвижная точка функции f, так как f (Y f) = Y f.

Числа и арифметика

Как Вы уже могли догадаться, все приведённые выше реализации необходимых объектов и структур не единственны — прелесть λ-исчисления в том, что Вы сами решаете, как реализовать базовые необходимые Вам вещи. Но если в отношении циклов и условий вроде как выявлены самые простые реализации, то с числами дела обстоят по-другому — практичных реализаций чисел необозримо много, для каждой задачи можно придумай свой, специфичный вариант. Тем не менее, существует общепринятая реализация чисел — «числительные Чёрча», придуманные тем самым Алонзо Чёрчем.

Функция inc:
inc = λnfx.f (n f x)
n раз применили функцию, и применим еще разок, чтобы получить n+1.

Как сложить m и n? Нужно применить f к x сначала m, а затем n раз:

add = λmnfx.m f (n f x)

Умножение делается проще, нужно m раз применять (n f) к x:

Возведение в степень — и того проще:
pow = λmn.n m

Напишем функцию, проверяющую, ноль ли наш аргумент:
λn.n (λx.false) true
Если аргумент — ноль, то он (как Вы помните из определения) просто возвратит второй аргумент, т.е. true, иначе он будет много (ну, как минимум, один) раз применять функцию λx.false к чему-то там. Вот и пригодились те самые константы, о которых мы говорили — возвращаемое значение будет false.

Теперь кое-что потруднее — вычитание. Для начала сделаем функцию, возвращающую число на 1 меньше (или что-нибудь, если аргумент — 0). Вот она:
dec = λnfx.n (λgh.h (g f)) (λu.x) (λu.u)
Думаю, теперь даже у самых стойких сдают нервы в связи с вопросом «как это, черт возьми, работает?». Попробуем понять.

Итак, мы видим, что после n применений, наше выражение имеет вид:
dec n = λfx.(λh.h ((n-1) f x)) ((λu.u)) = λfx.(λu.u) ((n-1) f x) = λfx.(n-1) f x = (n-1)
Профит!
Но что функция вернет в случае нуля?
dec 0 = λfx.(λu.x) (λu.u) = λfx.x = 0

Замечу, что 0 и false в наших определениях совпадают.

Теперь несложно написать и вычитание:
sub = λmn.(n dec) m

Комбинаторы

И еще один интересный факт: возможно выбрать конечный набор комбинаторов, через которые можно выразить любую другую λ-функцию! Такими наборами являются, например, SKI и BCKW.

Unlambda

Unlambda — чистый функциональный язык программирования, использующий комбинаторную логику. А именно, для создания функций в нем используется набор SKI. Применение функции F к функции G записывается как `FG, что избавляет нас от ненужных скобок. Применение нескольких аргументов подряд: «`fxyz. Помимо встроенных функций s, k, i в языке имеется возможность вывода на экран (.x обозначает функцию, аналогичную i, но в качестве побочного эффекта выводящую символ x на экран), а также механизмы для ввода и отложенных вычислений, но о них здесь речи идти не будет.

Давным-давно, в далекой-далекой галактике, я нашел некий туториал по unlambda, который заканчивался примерно такими словами:

Сейчас я хотел объяснить, как в этом языке можно написать цикл, вычисляющий числа Фибоначчи, но уже тут я бессилен:
«`s«s«sii`ki
`k.*«s«s`ks
«s`k`s`ks«s«s`ks«s`k`s`kr«s`k`sikk
`k«s`ksk

Что ж, давайте попробуем.
К слову, программа выводит число Фибоначчи в виде соответствующего числа звездочек на экране.

Пока всё будем записывать в стиле (уже) привычного нам λ-исчисления.

Вывести N звездочек: N print i — N раз применим print к тождественной функции, заодно выведем N звездочек. В итоге мы получим тождественную функцию. Давайте её к чему-нибудь применим! ((N print i) newline) (cycle (+ N M) N), где M — предыдущее число Фибоначчи. Итак, получилась такая функция одного прохода цикла:
cycle = λcnm.((n print i) newline) (c (+ n m) n)
передадим циклу самого себя в качестве параметра, и инициализируем его единичкой и нулем:
fib = cycle cycle 1 0

Осталось, как я и обещал, перевести это на unlambda. Ох.

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

Всё более-менее очевидно, кроме последнего. Посмотрим на определение комбинатора S:
S = λxyz.(x z) (y z)
Применим его к F, потом к G:
S F G = (λyz.(F z) (y z)) G = λz.(F z) (G z)
Действительно, это то, что нам нужно.

Теперь переведем на unlambda необходимые нам «кирпичики»:
0 = `ki
1 = i
add:

И готовая программа:

Да, да, мне самому очень страшно. К слову, в сборнике программ на unlambda аналогичный код занимает не намного меньше места. Видимо, автор языка владеет секретными древними техниками чрезвычайно компактного и оптимизированного перевода из λ-исчисления в unlambda. Тем не менее, обещание я сдержал. Спасибо тем, кто дочитал до конца.

Источник

Лямбда-исчисление на JavaScript

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

Итак, основная идея: всё есть функция. Поэтому мы ограничим себя очень узким кругом возможностей языка: любое выражение будет либо анонимной функцией с одним аргументом ( x => expr ), либо вызовом функции ( f (x) ). То есть весь код будет выглядеть похожим образом:

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

Базовые вещи

Начнём, как это принято, с условного ветвления. Введём две константы:

Это функции «двух аргументов», True возвращает первый аргумент, False возвращает второй аргумент. То есть, справедливы следующие утверждения:

Данные константы представляют логические истину и ложь, и позволяют написать функцию If :

Следующим делом введём первую «структуру данных» — пару. Определение выглядит следующим образом:

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

Вообще говоря, с подобным арсеналом мы уже могли бы определить Byte как кортеж из 8 логических значений, Int как кортеж из 4 Byte и реализовать на них машинную арифметику, но дело это рутинное и удовольствия никакого не принесёт. Есть более красивый способ описать натуральные числа — арифметика Чёрча.

Арифметика

Арифметика Чёрча описывает множество натуральных чисел с нулём как функции от двух аргументов:

Первый аргумент — это функция, второй аргумент — это что-то, к чему функция применяется n раз. Для их построения, по сути, нужны только ноль и функция +1 :

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

Тут стоит ещё описать способ преобразования чисел Чёрча во всем нам знакомый int — это в точности применение функции x => x + 1 к нулю n раз:

Аналогично определяются операции сложения, умножения и т.д.:

Таки образом можно продолжать реализовывать стрелочную нотацию, но смысла в этом нет: к этому моменту принцип работы с числами должен быть понятен.

Следующий шаг — вычитание. Следуя только что появившейся традиции, его реализация будет вот такой:

но остаётся проблемой реализация функции Pred. К счастью, Клини придумал её за нас.

Для полноты картины приведу реализации операций сравнения:

Списки

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

Если вы знакомы с функциональными операциями на списках, то, вероятно, уже заметили, что эта структура описывает правую свёртку. Поэтому и реализуется она тривиально:

Теперь реализуем стандартные операции для персистентных списков — добавление в начало, получение «головы» и «хвоста» списка.

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

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

Как пример использования, приведу реализацию функции map и ещё некоторых других:

Map заменяет каждый элемент списка результатом вызова функции f на нём.
Length и IsEmpty говорят сами за себя. toList и toIntList будут полезны для тестирования и для вывода списков в консоль.

Рекурсия

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

Видите ошибку? Если f не останавливается на пустом списке, то и OnNonEmpty не остановится, хотя должна. Дело в том, что JavaScript предоставляет нам аппликативный порядок вычислений, то есть все аргументы функции вычисляются до её вызова, никакой ленивости. А оператор If должен вычислять лишь одну ветку в зависимости от условия. Поэтому функцию нужно переписать, и красивее она от этого не станет.

Вторая проблема — рекурсия. Внутри функции мы можем обращаться только к её формальным аргументам. Это значит, что функция не может ссылаться сама на себя по имени.

«Главное свойство» комбинатора даёт прекрасный «побочный эффект»: возможность реализации рекурсии. Например, запись:

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

Последовательности

Последняя структура данных, которой я коснусь, это «бесконечные списки», или последовательности. Функциональное программирование славится возможностью работать с подобными объектами, и я просто не могу обойти их стороной.

Объявляются последовательности следующим образом:

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

Для возможности тестирования напишем функцию получения первых n элементов:

Если хотите поупражняться — реализуйте SeqTake без рекурсии. Это возможно, я гарантирую.

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

Осталось совсем немного, последние 2 функции, и они самые громоздкие из тех, что есть в данном тексте. Первая — функция фильтрации последовательности. Она находит в передаваемой последовательности все элементы, удовлетворяющие переданному предикату:

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

Вторая — последовательность простых чисел. Очередной вариант Решета Эратосфена в моём исполнении:

Эту функцию можно назвать кульминацией статьи. Принцип её работы проще будет понять на псевдокоде:

Не знаю, как вас, а меня всё ещё удивляет, что подобные вещи возможно написать с помощью лишь чистых функций!

Заключение

В итоге у меня получилось такое вот странное введение в LISP на примере языка JavaScript. Надеюсь я смог показать, что абстрактные математические идеи на самом деле очень близки к реальности программирования. И после подобного взгляда лямбда-исчисление перестанет выглядеть чем-то чересчур академичным.

Ну и, конечно, вот ссылка на Github со всем кодом из статьи.

Источник

Лямбда-исчисление

Лямбда-исчисление (англ. lambda calculus) — формальная система, придуманная в 1930-х годах Алонзо Чёрчем. Лямбда-функция является, по сути, анонимной функцией. Эта концепция показала себя удобной и сейчас активно используется во многих языках программирования.

Содержание

Лямбда-исчисление [ править ]

Пробел во втором правиле является терминалом грамматики. Иногда его обозначают как @, чтобы он не сливался с другими символами в выражении.

В первом случае функция является просто переменной. Во втором происходит аппликация (применение) одной функции к другой. Это аналогично вычислению функции-левого операнда на аргументе-правом операнде. В третьем — абстракция по переменной. В данном случае происходит создание функции одного аргумента с заданными именем аргумента и телом функции.

[math] x\\ (x\ z)\\ (\lambda x.(x\ z))\\ (\lambda z.(\lambda w.((\lambda y.((\lambda x.(x\ z))\ y))\ w)))\\ [/math]

Приоритет операций [ править ]

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

Связанными переменными называются все переменные, по которым выше в дереве разбора были абстракции. Все остальные переменные называются свободными.

Связанные переменные — это аргументы функции. То есть для функции они являются локальными.

α-эквивалетность [ править ]

и замкнуто относительно следующих правил:

[math] P=_\alpha P’ \Rightarrow \forall x \in V: \lambda x.P=_\alpha \lambda x.P’\\ P=_\alpha P’ \Rightarrow \forall Z \in \Lambda : P Z =_\alpha P’Z\\ P=_\alpha P’ \Rightarrow \forall Z \in \Lambda : Z P =_\alpha Z P’\\ P=_\alpha P’ \Rightarrow P’=_\alpha P\\ P=_\alpha P’ \ \& \ P’=_\alpha P» \Rightarrow P=_\alpha P»\\[/math]

β-редукция [ править ]

и замкнуто относительно следующих правил

[math]P\to _\beta P’ \Rightarrow \forall x\in V:\lambda x.P\to _\beta \lambda x.P’\\ P\to _\beta P’ \Rightarrow \forall Z\in \Lambda : P\ Z\to _\beta P’\ Z\\ P\to _\beta P’ \Rightarrow \forall Z\in \Lambda : Z\ P\to _\beta Z\ P'[/math]

Каррирование [ править ]

Нотация Де Брауна [ править ]

Грамматику нотации можно задать как:

Примеры выражений в этой нотации:

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

Определение [ править ]

Введём на основе лямбда-исчисления аналог натуральных чисел, основанный на идее, что натуральное число — это или ноль, или увеличенное на единицу натуральное число.

+1 [ править ]

Сложение [ править ]

Сложение двух чисел похоже на прибавление единицы. Но только надо прибавить не единицу, а второе число.

[math]n[/math] раз применить [math]s[/math] к применённому [math]m[/math] раз [math]s[/math] к [math]z[/math]

[math](\operatorname\ \bar 3\ \bar 3)\ (+1)\ 0 \equiv 6[/math]

[math](\operatorname\ ((\operatorname\ 2\ 5)(+1)\ 0)\ 4)(+1)0 \equiv 11[/math]

Умножение [ править ]

[math](\operatorname \bar 3\ \bar 3)\ (+1)\ 0 \equiv 9[/math]

Возведение в степень [ править ]

It’s a kind of magic

[math](\operatorname\ \bar 3\ (\operatorname\ \bar 3))\ (+1)\ 0 \equiv 81[/math]

Логические значения [ править ]

Стандартные функции булевой логики:

Ещё одной важной функцией является функция проверки, является ли число нулём:

Пара [ править ]

Вычитание [ править ]

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

Если вы ничего не поняли, не огорчайтесь. Вычитание придумал Клини, когда ему вырывали зуб мудрости. А сейчас наркоз уже не тот.

Сравнение [ править ]

Комбинатор неподвижной точки [ править ]

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

Лямбда исчисление обладаем замечательным свойством: у каждой функции есть неподвижная точка!

Рассмотрим следующую функцию.

[math]\operatorname = \operatorname\ \operatorname[/math]

[math]Y\ = \ \lambda f.(\lambda x.f(x\ x))\ (\lambda x.f(x\ x))[/math]

Деление [ править ]

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

[math]\operatorname