Пользователь
0,0
рейтинг
24 марта 2014 в 11:24

Разработка → λ-исчисление. Часть первая: история и теория tutorial

Идею, короткий план и ссылки на основные источники для этой статьи мне подал хабраюзер 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. Лекции по функциональному программированию
@AveNat
карма
212,0
рейтинг 0,0

Самое читаемое Разработка

Комментарии (33)

  • +1
    Выглядеть это будет примерно так: (λx.λy.x + y)x' y' = (λy.x' + y)y' = x' + y'.

    а почему вы вводите терм "+" без его описания?
    • 0
      Потому что суть здесь не в терме "+", а в логике каррирования. Мне показалось, что это нагляднее, чем

      f = λx.λy.s
      (f v) w
      ((λy.[x → v]s) w)
      [y → w][x → v]s
      • +2
        Ну мне как человеку, спустя 12 лет окунувшимся в математическую логику снова и просто ради интереса, конечно непонятной будет ваша наглядная запись, а вот та, которую вы написали выше уже более понятна, но правда опять появляется новый терм →, и мне снова приходится спрашивать, что такое → здесь. Ну вы не отвечайте, для этого есть учебный материал. Просто когда сталкиваешься со сложными темами на хабре, всегда хочется прочитать про них не как они описаны в учебных материалах, а так как они связываются с реальными объектами в мире, чтобы было побольше живых примеров, с каким-нибудь, например кодом иллюстрирующим сложные лямда конструкции, если это возможно конечно. Ну в любом случае спасибо, тема хорошая, интересная и нужная!
        • 0
          опять появляется новый терм →

          Это не терм, это операция подстановки, которая повляется при применении β-редукции к терму f v w в такой вот обобщенной форме записи.

          P.S. по-моему, статья написана легким для восприятия языком; читать приятно.
          • 0
            а я пользовался понятием «терм» как сокращение для «терминал (терминальный символ)» используемое в формальной грамматике, ведь для лямбда исчисления можно тоже построить грамматику, таким образом в любом случае все специальные символы типа +, → и т.д., вводимые в грамматику лямбда исчисления, будут сначала терминальными символами, а потом они буду приобретать другие свойства и становиться термами в рамках уже формальной логики.
  • +1
    Можно пояснить, почему терм (λx.x x)(λx.x x) на каждом шаге будет порождать себя? Разве не верна цепочка вычислений (λx.x x)(λx.x x) -> (x) (λx.x x) -> (x) (x), которая не упрощается без дальнейшего понимания, что такое x?
    • +1
      Здесь первые скобки — функция, имеющая тело x x, а вторые скобки — подставляемое значение аргумента x. Поэтому после подстановки (λx.x x) в x x снова получим (λx.x x)(λx.x x).
  • +6
    Я понял лишь часть про историю :)
    А если серьёзно — определитесь с аудиторией:
    1) голым новичкам, имхо, уже невозможно читать (я совсем запутался на аппликации и каррировании, и разобрался лишь после чтения других материалов (!), что делает этот цикл мало интересным)
    2) «адепты математики» видимо скучают, раз начинают придираться к формальностям (судя по предыдущим комментариям).
    • +1
      Спасибо за замечания, я постараюсь это учесть на будущее.
  • +1
    Каррирование называется так по имени блюда «карри». Залить рис карри так, чтобы только часть его была покрыта карри, а часть оставалась белой.
    • +1
      Всю жизнь думал что в честь Хаскелла Карри (вики)
      • +1
        Распространенная путаница.
        • 0
          Вы хотите сказать, что Хаскелл Карри не изобретал каррирование? (Хоть и позже Моисея Шейнфинкеля.)
  • 0
    Извините, но всё же возьму на себя смелость утверждать, что лямбда-исчисление должен знать любой уважающий себя программист. Уважающий себя программист должен уметь работать с абстракциями, понимать классику обработки списков (Lisp) и regex'ы.

    Вставьте больше примеров по каждой операции. Новичкам проще будет разобраться.

    И таки да, классическую нотацию лучше не нарушать. Если кто-то в самом деле заинтересуется и полезет изучать материал подробнее (ведь это является целью статьи, я правильно понял?), долго будут разбираться, где творчество автора, а где общепринятая нотация… На этом этапе это совсем ненужная головоломка…
    • 0
      Извините, но всё же возьму на себя смелость утверждать, что вместо regex вы имели ввиду redex.
  • 0
    применение функции: x y

    А какая функция применяется? Я правильно понимаю, что и x и y здесь — переменные?
    • 0
      Да, непонятно получилось. x — функция, y — фактический параметр.
  • 0
    Можете рассказать как работает Y-комбинатор?

    Мне как-то непонятно, почему, зачем и как он принимает значение рекурсивно заданного типа.
    • +6
      Я могу.

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

      image

      Все эти if, =, −, ×, 0, 1 можно считать сокращениями (макросами), которые на самом деле раскрываются в нормальные комбинаторы (замкнутые абстракции):

      image
      image
      image
      image
      image
      image
      image
      image
      image
      image
      image

      Но вот F уже таким образом не раскроешь, так как она обращается к некоей переменной F, которая ни с чем не связывается ни одной лямбда-абстракцией внутри её определения. Если у нас есть глобальное окружение, которое магическим образом свяжет переменную F с функцией F внутри определения функции F, то проблемы с её рекурсивным определением не будет. Иначе остаётся только ухищрение в виде Y-комбинатора.

      Суть ухищрения в явном использовании так называемых продолжений. Обычно считается, что функция возвращает своё значение в абстрактный «наверх» — тому, кто хочет получить вычисленное значение функции. Можно этот возврат значения сделать явным, передавая функции A другую функцию B, которую A вычислит, передав ей результат собственного вычисления в виде аргумента. Например, вычисление (+ 1 (+ 2 3)) можно представить в виде (+ 2 3 λx.(+ 1 x •)). Здесь функция + тернарная: принимает два слагаемых и продолжение, которому она передаёт результат сложения. Как видите, результат сложения 2 и 3 передаётся следующей функции под именем x, где к нему прибавляется 1, а результат сложения передаётся в некий •, что обозначает дальнейшие вычисления.

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

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

      Кульбит №1. Изящный способ удовлетворить предыдущее требование — это определить Y так, чтобы он возвращал то же, что передаёт в f. Тогда рекурсивный вызов (f n) можно записать в виде ((Y g) n), где g = λfn.• — рекурсивная функция f, в которой все рекурсивные вызовы делаются через локальную переменную f. Таким образом, должно выполняться равенство:

      Y \equiv \lambda f.f (Y f)

      Однако, по этой формуле нельзя понять, как записать Y в виде лямбда-терма, не используя Y. Собственно, формула кристаллизует проблему, возникающую при рекурсивном вызове.

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

      Y \equiv \lambda f.(X X)

      Кульбит №2. X надо записать в виде лямбда-терма:

      X = \lambda x. ???

      причём в нём нельзя ссылаться на X или Y, можно использовать только свою переменную x или свободную переменную f. Аргументом X может быть некоторый другой терм Z, который равен X с точностью до альфа-конверсии (Z — такой же X, только его переменная x переименована в z). Вот именно этот хитрый момент и позволяет осуществить «рекурсивный вызов», применяя одную анонимную функцию к другой, но «такой же» анонимной функции — для этого надо считать вызов эквивалентной функции эквивалентным рекурсивному вызову функции.

      Идём дальше, теперь немного очевидных наблюдений:





      Синтезировав эти наблюдения, можно заметить, что



      Кульбит №3. Cледим за руками. Предыдущее равенство подставляем в первое очевидное наблюдение:



      и в то же время



      то есть



      Кульбит №4. Какой должна быть функция эта функция X



      чтобы предыдущее свойство выполнялось? Достаточно заметить, что X используется таким образом, что переменная x внутри неё всегда связана с X (а вернее, с некоей функцией, которая ведёт себя так же, как X). Маленькое напряжение ума и желаемое определение становится очевидным:



      Теперь подставляем X в Y и получаем определение Y-комбинатора из палаты мер и весов:



      Как этим пользоваться. Возьмём факториал:



      и дополним его её одним аргументом — функцией, которая вычисляет факториал.



      Теперь F' не имеет рекурсии. Это обычный комбинатор (после раскрытия всяких if). Отлично, но что передать ему первым аргументом? От этой головной боли Y-комбинатор и избавляет:



      Теперь F — это функция, которая принимает одно число, и рекурсивно вычисляет факториал. Проверим, выполняя редукцию в нормальном порядке (всё не раскрываю, так как запутаться можно же):

















      • 0
        Вот этот комментарий прям в отдельную статью оформлять надо) Только продолжения как-то неожиданно вводятся, не совсем я понял, при чем здесь они.
        • +1
          Не при чём. Это просто был бред моего мозга в три часа ночи.
  • НЛО прилетело и опубликовало эту надпись здесь
    • 0
      Суть её в том, что вот есть у нас некий формальный язык, на котором можно написать какое-либо утверждение. Существует ли алгоритм, за конечное число шагов определяющий его истинность или ложность? Ответ был найден двумя великими учёными того времени Алонзо Чёрчем и Аланом Тьюрингом.


      Вообще-то за несколько лет до Тьюринга и Черча был Гедель со своими теоремами о неполноте.


      Вы в данном случае не совсем правы. Проблема разрешимости (Чёрч и Тьюринг) и проблема полноты (Гёдель) — это совсем разные проблемы. Полнота формальной системы означает только сам факт того, что для любого утверждения из данной системы существует доказательство его истинности или ложности. А разрешимость — наличие алгоритма, способного такое доказательство построить.

      Так, например, исчисление предикатов является полным, но не является разрешимым. Т.е. для любого утверждения есть доказательство его истинности или ложности, но принципиально не существует алгоритма, способного для любого утверждения это доказательство построить.
      • 0
        А можно вопрос в тему? Под логикой предикатов подразумевается логика первого порядка? Я не совсем понимаю, что это такое. Где граница между логикой первого парядка и логикой высшего порядка?
        • 0
          Правильно ли я понимаю, что в логике первого порядка есть фиксированное число предикатов и я могу их произвольно комбинировать с помощью кванторов и логических операций. Но в логике первого порядка нельзя сформулировать утверждение «для любого предиката P(x) верно ...»
          • 0
            Да, именно так. В логике второго порядка можно квантифицировать не только переменные, но и предикаты.

            Вообще, в «обычной» математике логика второго порядка используется не очень часто, но иногда в ней возникает потребность. Например она используется при формулировке аксиомы математической индукции, которая выглядит примерно так: для любого предиката, если этот предикат истинен для 0, а также если из его истинности для n следует его истинность для n+1, то тогда он истинен для любого числа.
            • НЛО прилетело и опубликовало эту надпись здесь
      • НЛО прилетело и опубликовало эту надпись здесь
        • 0
          Полнота и существование алгоритма, который решает истинно утверждение или нет, это одно и то же.
          Это совершенно точно неверно. Об этом говорит, хотя бы, существование, с одной стороны, теоремы о полноте исчисления предикатов (Гёдель), и, с другой стороны, доказательство неразрешимости исчисления предикатов (Тьюринг и Чёрч).

          Если для любого утверждения существует доказательство истинности или ложности, то элементарный переборный алгоритм его найдет.
          Честно говоря, точно не помню, в чем тут дело, но, по-моему, это объясняется тем, что исчисление предикатов содержит бесконечное число сигнатур.
          • НЛО прилетело и опубликовало эту надпись здесь
            • НЛО прилетело и опубликовало эту надпись здесь
  • 0
    Добавьте, пожалуйста, хаб Математика. Подписан на Математику, но Ваша статья обнаружена случайно.
  • –1
    image

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