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

Основы функционального программирования

• Вводная лекция
  
• Структуры данных и базисные операции:
  • Первая часть
    
  • Вторая часть
    

• Основы языка Haskell
  
  • Служебные слова и синтаксис
    
  • Модули и монады
    
  • Ввод-вывод
    
  • Другие статьи и учебники по Haskell →

• Конструирование функций
  
• Доказательство свойств функций
  
• Формализация функционального программирования на основе λ-исчисления
  
• Трансформация программ

• Категория «Функциональное программирование» →

• Объект изучения: множество определений функций.
• Предположение: будет считаться, что любая функция может быть определена при помощи некоторого λ-выражения.
• Цель исследования: установить по двум определениям функций $\langle f_{1}\rangle$ и $\langle f_{2}\rangle$ их тождество на всей области определения — $\forall x:f_{1}(x)=f_{2}(x)$. (Здесь использована такая нотация: $f$ — некоторая функция, $\langle f\rangle$ — определения этой функции в терминах λ-исчисления.)

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

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

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

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

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

$P=\langle V,\,\Phi ,\,A,\,R\rangle$,

где $V$ — алфавит;

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

$A$ — аксиомы (при этом $A\subseteq \Phi$);

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

В рассматриваемой задаче формулы имеют вид $(t_{1}=t_{2})$, где $t_{1}$ и $t_{2}$ — λ-выражения. Если некоторая формула выводима в формальной системе, то этот факт записывается как $(\vdash t_{1}=t_{2})$.

Говорят, что формальная система корректна, если $(\vdash t_{1}=t_{2})\Rightarrow (\vDash t_{1}=t_{2})$.

Говорят, что формальная система полна, если $(\vDash t_{1}=t_{2})\Rightarrow (\vdash t_{1}=t_{2})$.

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

1°. $v\in \mathrm {Id} \Rightarrow v\in \mathrm {Exp}$.

2°. $v\in \mathrm {Id} ,\,E\in \mathrm {Exp} \Rightarrow \lambda v.E\in \mathrm {Exp}$

3°. $E,E'\in \mathrm {Exp} \Rightarrow (EE')\in \mathrm {Exp}$

4°. $E\in \mathrm {Exp} \Rightarrow (E)\in \mathrm {Exp}$

5°. Никаких других $\mathrm {Exp}$ нет.

Примечание: $\mathrm {Id}$ — множество идентификаторов.

Говорят, что $v$ свободна в $M\in \mathrm {Exp}$, если:

1°. $M=v$.

2°. $M=(M_{1}M_{2})$, и $v$ свободна в $M_{1}$ или в $M_{2}$.

3°. $M=\lambda v'.M'$, и $v\neq v'$, и $v$ свободна в $M'$.

4°. $M=(M')$, и $v$ свободна в $M'$.

Множество идентификаторов $v$, свободных в $M$, обозначается как $FV(M)$.

Говорят, что $v$ связана в $M\in \mathrm {Exp}$, если:

1°. $M=\lambda v'.M'$, и $v=v'$.

2°. $M=(M_{1}M_{2})$, и $v$ связана в $M_{1}$ или в $M_{2}$ (то есть один и тот же идентификатор может быть свободен и связан в $\mathrm {Exp}$).

3°. $M=(M')$, и $v$ связана в $M'$.

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

1. $M=v$. $v$ — свободна.
2. $M=\lambda x.xy$. $x$ — связана, $y$ — свободна.
3. $M=(\lambda v.v)v$. $v$ входит в это выражение как свободно, так и связанно.
4. $M=VW$. $V$ и $W$ — свободны.

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

$(\lambda x.yx)[y\leftarrow \lambda z.z]=\lambda x.(\lambda z.z)x=\lambda x.x$ — корректная подстановка;

$(\lambda x.yx)[y\leftarrow xx]=\lambda x.(xx)x$ — коллизия имён переменных;

$(\lambda z.yz)[y\leftarrow xx]=\lambda z.(xx)z$ — корректная подстановка.

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

1°. $x[x\leftarrow E']=E'$.

2°. $y[x\leftarrow E']=y$.

3°. $(\lambda x.E)[x\leftarrow E']=\lambda x.E$.

4°. $(\lambda y.E)[x\leftarrow E']=\lambda y.E[x\leftarrow E']$, при условии, что $y\not \in FV(E')$.

5°. $(\lambda y.E)[x\leftarrow E']={\Big (}\lambda z.E[y\leftarrow z]{\Big )}[x\leftarrow E']$, при условии, что $y\in FV(E')$.

6°. $(E_{1}\,E_{2})[x\leftarrow E']={\Big (}E_{1}[x\leftarrow E']\,E_{2}[x\leftarrow E']{\Big )}$.

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

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

Правильно построенные формулы выглядят так: $\mathrm {Exp} =\mathrm {Exp}$.

Аксиомы:

$\vdash \lambda x.E=\lambda y.E[x\leftarrow y]$;	(α)
$\vdash (\lambda x.E)E'=E[x\leftarrow E']$;	(β)
$\vdash t=t$, в случае, если $t$ — идентификаторы.	(ρ)

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

$t_{1}=t_{2}\Rightarrow t_{1}t_{3}=t_{2}t_{3}$;	(μ)
$t_{1}=t_{2}\Rightarrow t_{3}t_{1}=t_{3}t_{2}$;	(ν)
$t_{1}=t_{2}\Rightarrow t_{2}=t_{1}$;	(σ)
$t_{1}=t_{2},\,t_{2}=t_{3}\Rightarrow t_{1}=t_{3}$;	(τ)
$t_{1}=t_{2}\Rightarrow \lambda x.t_{1}=\lambda x.t_{2}$.	(ξ)

Пример 27. Доказать выводимость формулы $(\lambda x.xy)(\lambda z.(\lambda u.zu))v=(\lambda v.yv)v$

	$(\lambda x.xy)(\lambda z.(\lambda u.zu))v=(\lambda v.yv)v$;
(μ):	$(\lambda x.xy)(\lambda z.(\lambda u.zu))=(\lambda v.yv)$;
(β):	$(\lambda z.(\lambda u.zu))y=(\lambda v.yv)$;
(α):	$\lambda u.yu=\lambda v.yv$ — выводима.

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

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

$\vdash \lambda x.M\to \lambda y.M[x\leftarrow y]$	(α′)
$\vdash (\lambda x.M)N\to M[x\leftarrow N]$	(β′)
$\vdash M\to M$	(ρ′)

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

$t_{1}\to t_{1}',\,t_{2}\to t_{2}'\Rightarrow t_{1}t_{2}\to t_{1}'t_{2}'$

(π)

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

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

• Выражение вида $\lambda x.M$ называется α-редексом.
• Выражение вида $(\lambda x.M)N$ называется β-редексом.
• Выражения, не содержащие β-редексов, называются выражениями в нормальной форме.

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

• $\vdash E_{1}=E_{2}\Rightarrow E_{1}\to E_{2}\lor E_{2}\to E_{1}$.
• $E\to E_{1}\land E\to E_{2}\Rightarrow \exists F:E_{1}\to F\land E_{2}\to F$. (Теорема Чёрча—Россера).
• Если $E$ имеет нормальные формы $E_{1}$ и $E_{2}$, то они эквивалентны с точностью до α-конверсии, то есть различаются только обозначением связанных переменных.

Стратегия редукции

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

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

Пример 28. Редукция выражения $M=(\lambda y.x)(EE)$, где $E=\lambda x.xx$

1°. НРС: ${\underline {(\lambda y.x)}}(EE)={\underline {(\lambda y.x)}}[y\leftarrow EE]=x$.

2°. АРС: $(\lambda y.x){\underline {(EE)}}=(\lambda y.x){\underline {{\Big (}(\lambda x.xx)(\lambda x.xx){\Big )}}}=(\lambda y.x){\underline {{\Big (}(\lambda x.xx)(\lambda x.xx){\Big )}}}=\dots$.

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

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

Пример 29. Редукция выражения $M=(\lambda x.xyxx){\Big (}(\lambda z.z)w{\Big )}$

1°. НРС: ${\underline {(\lambda x.xyxx)}}{\Big (}(\lambda z.z)w{\Big )}={\underline {{\Big (}(\lambda z.z)w{\Big )}}}y{\Big (}(\lambda z.z)w{\Big )}{\Big (}(\lambda z.z)w{\Big )}=$

$=wy{\underline {{\Big (}(\lambda z.z)w{\Big )}}}{\Big (}(\lambda z.z)w{\Big )}=wyw{\underline {{\Big (}(\lambda z.z)w{\Big )}}}=wyww$.

2°. АРС: $(\lambda x.xyxx){\underline {{\Big (}(\lambda z.z)w{\Big )}}}={\underline {(\lambda x.xyxx)}}w=wyww$.

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

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

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

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