Основы функционального программирования/Формализация функционального программирования на основе лямбда-исчисления

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

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

Возникает вопрос: как учесть семантику встроенных функций при сравнении их экстенсионалов (так как явно определения этих функций неизвестны)? Варианты ответов:

  1. Можно попытаться выразить семантику встроенных функций при помощи механизма λ-исчисления. Этот процесс можно довести до случая, когда все встроенные функции не содержат непроинтерпретированных операций.
  2. Говорят, что и семантически равны (этот факт обозначается как ), если при любой интерпретации непроинтерпретированных идентификаторов.

Понятие формальной системы[править]

Формальная система представляет собой четвёрку:

,

где алфавит;

— множество правильно построенных формул;

аксиомы (при этом );

— правила вывода.

В рассматриваемой задаче формулы имеют вид , где и — λ-выражения. Если некоторая формула выводима в формальной системе, то этот факт записывается как .

Говорят, что формальная система корректна, если .

Говорят, что формальная система полна, если .

Семантическое определение понятия «конструкция» (обозначение — ):

1°. .

2°.

3°.

4°.

5°. Никаких других нет.

Примечание: — множество идентификаторов.

Говорят, что свободна в , если:

1°. .

2°. , и свободна в или в .

3°. , и , и свободна в .

4°. , и свободна в .

Множество идентификаторов , свободных в , обозначается как .

Говорят, что связана в , если:

1°. , и .

2°. , и связана в или в (то есть один и тот же идентификатор может быть свободен и связан в ).

3°. , и связана в .

Пример 26. Свободные и связанные идентификаторы.

  1. . — свободна.
  2. . — связана, — свободна.
  3. . входит в это выражение как свободно, так и связанно.
  4. . и — свободны.

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

— корректная подстановка;

— коллизия имён переменных;

— корректная подстановка.

Точное определение базисной подстановки:

1°. .

2°. .

3°. .

4°. , при условии, что .

5°. , при условии, что .

6°. .

Построение формальной системы[править]

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

Правильно построенные формулы выглядят так: .

Аксиомы:

; (α)
; (β)
, в случае, если — идентификаторы. (ρ)

Правила вывода:

; (μ)
; (ν)
; (σ)
; (τ)
. (ξ)

Пример 27. Доказать выводимость формулы

;
(μ): ;
(β): ;
(α): — выводима.

Во втором варианте формализации функционального программирования можно воспользоваться не свойством симметричности отношения «», а свойством несимметричности отношения «».

Во второй формальной системе правильно построенные формулы выглядят абсолютно так же, как и в первом варианте. Однако аксиомы принимают несколько иной вид:

(α′)
(β′)
(ρ′)

Правило вывода во втором варианте формальной системы одно:

(π)

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

Определения:

  • Выражение вида называется α-редексом.
  • Выражение вида называется β-редексом.
  • Выражения, не содержащие β-редексов, называются выражениями в нормальной форме.

Несколько теорем (без доказательств):

  • .
  • . (Теорема Чёрча—Россера).
  • Если имеет нормальные формы и , то они эквивалентны с точностью до α-конверсии, то есть различаются только обозначением связанных переменных.

Стратегия редукции[править]

1°. Нормальная редукционная стратегия (НРС). На каждом шаге редукции выбирается текстуально самый левый β-редекс. Доказано, что нормальная редукционная стратегия гарантирует получение нормальной формы выражения, если она существует.

2°. Аппликативная редукционная стратегия (АРС). На каждом шаге редукции выбирается β-редекс, не содержащий внутри себя других β-редексов. Далее будет показано, что аппликативная редукционная стратегия не всегда позволяет получить нормальную форму выражения.

Пример 28. Редукция выражения , где

1°. НРС: .

2°. АРС: .

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

Примечание: подчёркиванием выделен β-редекс, редуцируемый следующим шагом.

Пример 29. Редукция выражения

1°. НРС:

.

2°. АРС: .

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

Соответствие между вычислениями функциональных программ и редукцией[править]

Работа интерпретатора описывается несколькими шагами:

  1. В выражении необходимо выделить некоторое обращение к рекурсивной или встроенной функции с полностью означенными аргументами. Если выделенное обращение к встроенной функции существует, то происходит его выполнение и возврат к началу первого шага.
  2. Если выделенное на первом шаге обращение к рекурсивной функции, то вместо него подставляется тело функции с фактическими параметрами (так как они уже означены). Далее происходит переход на начало первого шага.
  3. Если больше обращений нет, то происходит остановка.

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

Представление определений функций в виде λ-выражений[править]

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

fact = λn.if n == 0 then 1 else n * fact (n – 1)

То же самое определение можно описать при помощи использования некоторого функционала:

fact = (λf.λn.if n == 0 then 1 else n * f (n – 1)) fact

Жирным шрифтом в представленном выражении выделен функционал F. Таким образом, функцию вычисления факториала можно записать так: fact = F fact. Можно видеть, что любое рекурсивное определение некоторой функции f можно представить в таком виде:

f = F f

Это выражение можно трактовать как уравнение, в котором рекурсивная функция f является неподвижной точкой функционала F. Соответственно интерпретатор функционального языка можно в таком же ключе рассматривать как численный метод решения этого уравнения.

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

Свойства функции Y определяются равенством:

Y F = F (Y F)

Теорема (без доказательства):

Любой λ-терм имеет неподвижную точку.

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

1°.

prefix = λxyz.zxy
head = λp.p(λxy.x)
tail = λp.p(λxy.y)

2°. Моделирование условных выражений:

True = λxy.x
False = λxy.y
if B then M else N = BNM, где B = {True, False}.