Pull to refresh

λ-исчисление. Часть первая: история и теория

Reading time 6 min
Views 154K
Идею, короткий план и ссылки на основные источники для этой статьи мне подал хабраюзер z6Dabrata, за что ему огромнейшее спасибо.

UPD: в текст внесены некоторые изменения с целью сделать его более понятным. Смысловая составляющая осталась прежней.

Вступление


Возможно, у этой системы найдутся приложения не только
в роли логического исчисления. (Алонзо Чёрч, 1932)


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


Начнём мы с традиционного (но краткого) экскурса в историю. В 30-х годах прошлого века перед математиками встала так называемая проблема разрешения (Entscheidungsproblem), сформулированная Давидом Гильбертом. Суть её в том, что вот есть у нас некий формальный язык, на котором можно написать какое-либо утверждение. Существует ли алгоритм, за конечное число шагов определяющий его истинность или ложность? Ответ был найден двумя великими учёными того времени Алонзо Чёрчем и Аланом Тьюрингом. Они показали (первый — с помощью изобретённого им λ-исчисления, а второй — теории машины Тьюринга), что для арифметики такого алгоритма не существует в принципе, т.е. Entscheidungsproblem в общем случае неразрешима.

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

λ-исчисление: основные понятия


Синтаксис

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

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

Термы:
переменная: x
лямбда-абстракция (анонимная функция): λx.t, где x — аргумент функции, t — её тело.
применение функции (аппликация): f x, где f — функция, x — подставляемое в неё значение аргумента


Соглашения о приоритете операций:
  • Применение функции левоассоциативно. Т.е. s t u — это тоже самое, что (s t) u
  • Аппликация (применение или вызов функции по отношению к заданному значению) забирает себе всё, до чего дотянется. Т.е. λx. λy. x y x означает то же самое, что λx. (λy. ((x y) x))
  • Скобки явно указывают группировку действий.


Может показаться, будто нам нужны какие-то специальные механизмы для функций с несколькими аргументами, но на самом деле это не так. Действительно, в мире чистого лямбда-исчисления возвращаемое функцией значение тоже может быть функцией. Следовательно, мы можем применить первоначальную функцию только к одному её аргументу, «заморозив» прочие. В результате получим новую функцию от «хвоста» аргументов, к которой применим предыдущее рассуждение. Такая операция называется каррированием (в честь того самого Хаскелла Карри). Выглядеть это будет примерно так:
f = λx.λy.t Функция с двумя аргументами x и y и телом t
f v w Подставляем в f значения v и w
(f v) w Эта запись аналогична предыдущей, но скобки явно указывают на последовательность подстановки
((λy.[x → v]t) w) Подставили v вместо x. [x → v]t означает «тело t, в котором все вхождения x заменены на v»
[y → w][x → v]t Подставили w вместо y. Преобразование закончено.

И напоследок несколько слов об области видимости. Переменная x называется связанной, если она находится в теле t λ-абстракции λx.t. Если же x не связана какой-либо вышележащей абстракцией, то её называют свободной. Например, вхождения x в x y и λy.x y свободны, а вхождения x в λx.x и λz.λx.λy.x(y z) связаны. В (λx.x)x первое вхождение x связано, а второе свободно. Если все переменные в терме связаны, то его называют замкнутым, или комбинатором. Мы с вами будем использовать следующий простейший комбинатор (функцию тождества): id = λx.x. Она не выполняет никаких действий, а просто возвращает без изменений свой аргумент.

Процесс вычисления

Рассмотрим следующий терм-применение:

(λx.t) y

Его левая часть — (λx.t) — это функция с одним аргументом x и телом t. Каждый шаг вычисления будет заключаться в замене всех вхождений переменной x внутри t на y. Терм-применение такого вида носит имя редекса (от reducible expression, redex — «сокращаемое выражение»), а операция переписывания редекса в соответствии с указанным правилом называется бета-редукцией.

Существует несколько стратегий выбора редекса для очередного шага вычисления. Рассматривать их мы будем на примере следующего терма:

(λx.x) ((λx.x) (λz. (λx.x) z)),

который для простоты можно переписать как

id (id (λz. id z))

(напомним, что id — это функция тождества вида λx.x)

В этом терме содержится три редекса:


  1. Полная β-редукция. В этом случае каждый раз редекс внутри вычисляемого терма выбирается произвольным образом. Т.е. наш пример может быть вычислен от внутреннего редекса к внешнему:

  2. Нормальный порядок вычислений. Первым всегда сокращается самый левый, самый внешний редекс.

  3. Вызов по имени. Порядок вычислений в этой стратегии аналогичен предыдущей, но к нему добавляется запрет на проведение сокращений внутри абстракции. Т.е. в нашем примере мы останавливаемся на предпоследнем шаге:

    Оптимизированная версия такой стратегии (вызов по необходимости) используется Haskell. Это так называемые «ленивые» вычисления.
  4. Вызов по значению. Здесь сокращение начинается с самого левого (внешнего) редекса, у которого в правой части стоит значение — замкнутый терм, который нельзя вычислить далее.

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

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

Недостатком стратегии вызова по значению является то, что она может зациклиться и не найти существующее нормальное значение терма. Рассмотрим для примера выражение

(λx.λy. x) z ((λx.x x)(λx.x x))

Этот терм имеет нормальную форму z несмотря на то, что его второй аргумент такой формой не обладает. На её-то вычислении и зависнет стратегия вызова по значению, в то время как стратегия вызова по имени начнёт с самого внешнего терма и там определит, что второй аргумент не нужен в принципе. Вывод: если у редекса есть нормальная форма, то «ленивая» стратегия её обязательно найдёт.

Ещё одна тонкость связана с именованием переменных. Например, терм (λx.λy.x)y после подстановки вычислится в λy.y. Т.е. из-за совпадения имён переменных мы получим функцию тождества там, где её изначально не предполагалось. Действительно, назови мы локальную переменную не y, а z — первоначальный терм имел бы вид(λx.λz.x)y и после редукции выглядел бы как λz.y. Для исключения неоднозначностей такого рода надо чётко отслеживать, чтобы все свободные переменные из начального терма после подстановки оставались свободными. С этой целью используют α-конверсию — переименование переменной в абстракции с целью исключения конфликтов имён.

Так же бывает, что у нас есть абстракция λx.t x, причём x свободных вхождений в тело t не имеет. В этом случае данное выражение будет эквивалентно просто t. Такое преобразование называется η-конверсией.

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

Список источников

  1. «What is Lambda Calculus and should you care?», Erkki Lindpere
  2. «Types and Programming Languages», Benjamin Pierce
  3. Вики-конспект «Лямбда-исчисление»
  4. «Учебник по Haskell», Антон Холомьёв
  5. Лекции по функциональному программированию
Tags:
Hubs:
+44
Comments 34
Comments Comments 34

Articles