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

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

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

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

  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}.