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

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

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

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

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

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

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

$P=⟨V,\mathrm{\Phi },A,R⟩$,

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

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

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

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

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

Говорят, что формальная система корректна, если $(⊢t_1=t_2)\Rightarrow (\models t_1=t_2)$.

Говорят, что формальная система полна, если $(\models t_1=t_2)\Rightarrow (⊢t_1=t_2)$.

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

1°. $v\in \mathrm{I}\mathrm{d}\Rightarrow v\in \mathrm{E}\mathrm{x}\mathrm{p}$.

2°. $v\in \mathrm{I}\mathrm{d},E\in \mathrm{E}\mathrm{x}\mathrm{p}\Rightarrow \lambda v.E\in \mathrm{E}\mathrm{x}\mathrm{p}$

3°. $E,E^{\prime }\in \mathrm{E}\mathrm{x}\mathrm{p}\Rightarrow (E{E}^{\prime })\in \mathrm{E}\mathrm{x}\mathrm{p}$

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

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

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

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

1°. $M=v$.

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

3°. $M=\lambda v^{\prime }.M^{\prime }$, и $v\ne v^{\prime }$, и $v$ свободна в $M^{\prime }$.

4°. $M=(M^{\prime })$, и $v$ свободна в $M^{\prime }$.

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

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

1°. $M=\lambda v^{\prime }.M^{\prime }$, и $v=v^{\prime }$.

2°. $M=(M_1{M}_2)$, и $v$ связана в $M_1$ или в $M_2$ (то есть один и тот же идентификатор может быть свободен и связан в $\mathrm{E}\mathrm{x}\mathrm{p}$).

3°. $M=(M^{\prime })$, и $v$ связана в $M^{\prime }$.

Пример 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^{\prime }$ вместо всех свободных вхождений переменной $x$ обозначается как $E[x\leftarrow E^{\prime }]$. Во время подстановки иногда случается так, что получается конфликт имён, то есть коллизия переменных. Примеры коллизий:

$(\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^{\prime }]=E^{\prime }$.

2°. $y[x\leftarrow E^{\prime }]=y$.

3°. $(\lambda x.E)[x\leftarrow E^{\prime }]=\lambda x.E$.

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

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

6°. $(E_1{E}_2)[x\leftarrow E^{\prime }]=(E_1[x\leftarrow E^{\prime }]E_2[x\leftarrow E^{\prime }])$.

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

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

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

Аксиомы:

$⊢\lambda x.E=\lambda y.E[x\leftarrow y]$;	(α)
$⊢(\lambda x.E)E^{\prime }=E[x\leftarrow E^{\prime }]$;	(β)
$⊢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$».

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

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

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

$t_1\to {t_1}^{\prime },t_2\to {t_2}^{\prime }\Rightarrow t_1{t}_2\to {t_1}^{\prime }{t_2}^{\prime }$

(π)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

$=wy\underset{\_}{((\lambda z.z)w)}((\lambda z.z)w)=wyw\underset{\_}{((\lambda z.z)w)}=wyww$.

2°. АРС: $(\lambda x.xyxx)\underset{\_}{((\lambda z.z)w)}=\underset{\_}{(\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}.