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

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

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

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

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

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

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

$\operatorname {Int} (P,\,d)=d\,'$

где $P$ — программа;

$d$ — исходные данные;

$d\,'$ — выходные данные.

Если интерпретатор $\mathrm {Int}$ представлен в виде каррированной функции $f$ такой, что $f\,P\,d=d\,'$, тогда определение $f=M\,f$, а точнее функционал $M$ называется денотационной семантикой языка $L$. В этом случае имеет смысл $\lambda$-выражение: $f\,P=\lambda d.M':D\to D'$. При этом частичную функцию $f\,P$ можно рассматривать как функцию $f_{P}$ одного аргумента, которая есть функция, реализующая программу $P$. Как было показано в предыдущей лекции, можно построить рекурсивное определение вида: $f_{P}=M_{P}\,f_{P}$. Такой вид изначально имеют все программы на функциональном языке. Но эту запись можно понимать двояко:

• Это определение можно понимать просто как строку символов, подаваемую на вход интерпретатора. Функция, вычисляемая интерпретатором по тексту $f=M\,f$, обозначается как $f_{\mathrm {int} }$.
• $f=M\,f$ — есть чистое математическое определение функции $f$. Решение этого уравнения обозначается как $f_{\mathrm {mat} }$.

Резонный вопрос: каково соотношение этих двух функций — $f_{\mathrm {int} }$ и $f_{\mathrm {mat} }$? Надо полагать, что корректный интерпретатор как раз вычисляет $f_{\mathrm {mat} }$.

Определение: говорят, что функция $f_{1}$ менее определена, чем функция $f_{2}$ (обозначается как $f_{1}\subseteq f_{2}$), если $\forall x:f_{1}x=y\Rightarrow f_{2}x=y$. Если для двух функций одновременно выполняется $f_{1}\subseteq f_{2}$ и $f_{2}\subseteq f_{1}$, то имеет место тождество функций.

Как правило, $f_{\mathrm {int} }\subseteq f_{\mathrm {mat} }$ — это происходит потому, что обычно интерпретатор реализует аппликативную стратегию редукции. Однако в дальнейших рассуждениях будет полагаться тождество функций $f_{\mathrm {int} }$ и $f_{\mathrm {mat} }$, поэтому тексты программ будут рассматриваться как математическое определение функций. Тогда эквивалентное преобразование функциональных программ есть просто эквивалентные преобразования специального вида математических определений функций.

Трансформация программ — это просто синтаксические преобразования, во время которых совершенно не затрагивается семантика программ, так как программа воспринимается просто как набор символов. Обозначение того факта, что один текст $f_{1}$ получаем при помощи синтаксических трансформаций другого текста $f_{2}$, выглядит следующим образом: $f_{1}\vdash f_{2}$.

Говорят, что преобразование корректно, если $f_{1}\subseteq f_{2}$.

Говорят, что преобразование эквивалентно, если $f_{1}\equiv f_{2}$.

Далее вводится еще несколько специальных обозначений:

1. Имеется исходный набор клозов (то есть объектов преобразования), и этот набор будет обозначаться либо DEF, либо SPEC.
2. Клозы, описывающие функцию, которая содержит отображения из исходных клозов, обозначается как INV.
3. Некоторые равенства, выражающие свойства внутренних (зарезервированных) функций, обозначаются как LAW.

Определение: пусть $F(X)$ — некоторое выражение (равенство), в котором выделены все свободные вхождения терма $X$. Тогда $F[X\leftarrow M]$ называется примером $F$. При этом считается, что $M$ — это некоторое выражение.

Виды преобразований

1°. Конкретизация (instantiation) — INS.

${\frac {E_{1}(X)=E_{2}(X)}{E_{1}[X\leftarrow M]=E_{2}[X\leftarrow M]}}$

2°. Преобразование — без названия :)

${\frac {M(Y)=N(Y),\,E_{1}=E_{2}[X\leftarrow M'],\,M'=M[Y\leftarrow G]}{E_{1}=E_{2}[X\leftarrow N'],\ {\mbox{where}}\ N'=N[Y\leftarrow G]}}$

3°. Развёртка (unfolding) — UNF.

${\frac {M(Y)=N(Y),\,E_{1}=E_{2}(M'),\,M'=M[Y\leftarrow G]}{E_{1}=E_{2}(N'),\ {\mbox{where}}\ N'=N[Y\leftarrow G]}}$

4°. Свёртка (folding) — FLD.

${\frac {M(Y)=N(Y),\,E_{1}=E_{2}(N'),\,N'=N[Y\leftarrow G]}{E_{1}=E_{2}(M'),\ {\mbox{where}}\ M'=M[Y\leftarrow G]}}$

5°. Закон (law) — LAW.

${\frac {M(Y)=N(Y),\,E_{1}=E_{2}(M'),\,M'=M[Y\leftarrow G]}{E_{1}=E_{2}(N'),\ {\mbox{where}}\ N'=N[Y\leftarrow G]}}$

6°. Абстракция и аппликация (abstraction & application) — ABS.

${\frac {M[X\leftarrow G]=(\lambda X.M)G,\,E_{1}=E_{2}{\Big (}M[X\leftarrow G]{\Big )}}{E_{1}=E_{2}{\Big (}(\lambda X.M)G{\Big )}}}$

Пример 30. Преобразование функции length.

length []    = 0                                   1 (DEF)
length (H:T) = 1 + length T                        2 (DEF)

length_2 L1 L2   = length L1 + length L2           3 (SPEC)
length_2 [] L    = length [] + length L            4 (INS 3)
                   = 0 + length L                  5 (UNF 1)
                   = length L                      6 (LAW +) (*)

length_2 (H:T) L = length (H:T) + length L         7 (INS 3)
                   = (1 + length T) + length L     8 (UNF 2)
                   = 1 + (length T + length L)     9 (LAW +)
                   = 1 + length_2 T L             10 (FLD 3) (**)

Теперь остаётся взять два полученных клоза (*) и (**) и составить из них новое рекурсивное определение новой функции, не использующее вызова старой функции:

length_2 []    L = length L
length_2 (H:T) L = 1 + length_2 T L

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

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

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

Второй закон информатики

• Существуют неразрешимые задачи.
• Не существует эффективной реализации для декларативных языков, если они универсальны.

Концепция трансформационного синтеза: позволить программисту писать определения функций, не заботясь об их эффективности.

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

Частичные вычисления

Пусть $P$ и $S$ — два языка, работающих со строками символов (это не нарушает общности рассуждений), а $\mathbf {P}$ и $\mathbf {S}$ — множества синтаксически правильных программ на соответствующих языках. $D$ — домен всевозможных символьных последовательностей.

$P::D\to (D^{*}\to D)$

Если $p$ — программа из $\mathbf {P}$, то:

$P(p)::D^{*}\to D$

$P(p)(\langle d_{1},\,\dots ,\,d_{n}\rangle )=d$, и $d\in D$

$P(r)(\langle y_{1},\,\dots ,\,y_{n}\rangle )=P(p)(\langle d_{1},\,\dots ,\,d_{m},\,y_{1},\,\dots ,\,y_{n}\rangle )$

В последнем равенстве переменными $y_{i}$ обозначены неизвестные данные. Для программы $p$ эти $n$ переменных представляют остаточный код.

Частичным вычислителем MIX называется программа из $\mathbf {P}$ (хотя, частичный вычислитель может быть реализован на любом языке) такая, что:

$\forall p\in \mathbf {P} ,\,p(x_{1},\,\dots ,\,x_{m},\,x_{m+1},\,\dots ,\,x_{n}):P(\mathrm {MIX} )(\langle p,\,d_{1},\,\dots ,\,d_{m}\rangle )=r$.

То есть MIX — это программа, которая, получив некоторую исходную программу и данные для её известных параметров, выдаёт остаточную программу для исходной.

Интерпретатором языка $S$ называется программа $\mathrm {INT} \in \mathbf {P}$ такая, что:

$\forall s\in \mathbf {S} ,\,\langle d_{1},\,\dots ,\,d_{n}\rangle \in D^{*}:P(\mathrm {INT} )(\langle s,\,d_{1},\,\dots ,\,d_{n}\rangle )=S(s)(\langle d_{1},\,\dots ,\,d_{n}\rangle )$.

Компилятором языка $S$ называется программа $\mathrm {COMP} \in \mathbf {P}$ такая, что:

$P(\mathrm {COMP} )(\langle s\rangle )=\mathrm {TARGET}$

$P(\mathrm {TARGET} )(\langle d_{1},\,\dots ,\,d_{n}\rangle )=S(s)(\langle d_{1},\,\dots ,\,d_{n}\rangle )$.

Или, что то же:

$P{\Big (}P(\mathrm {COMP} )(\langle s\rangle ){\Big )}(\langle d_{1},\,\dots ,\,d_{n}\rangle )=S(s)(\langle d_{1},\,\dots ,\,d_{n}\rangle )$.

Компилятором компиляторов языка $S$ называется программа $\mathrm {COCOM} \in \mathbf {P}$ такая, что:

$P(\mathrm {COCOM} )(\langle \mathrm {INT} \rangle )=\mathrm {COMP}$

$P{\biggr (}P{\Big (}P(\mathrm {COCOM} )(\langle \mathrm {INT} \rangle ){\Big )}(\langle s\rangle ){\biggr )}(\langle d_{1},\,\dots ,\,d_{n}\rangle )=S(s)(\langle d_{1},\,\dots ,\,d_{n}\rangle )$.

Проекции Футамуры

• $\mathrm {TARGET} =P(\mathrm {MIX} )(\langle \mathrm {INT} ,\,s\rangle )$
• $\mathrm {COMP} =P(\mathrm {MIX} )(\langle \mathrm {MIX} ,\,\mathrm {INT} \rangle )$
• $\mathrm {COCOM} =P(\mathrm {MIX} )(\langle \mathrm {MIX} ,\,\mathrm {MIX} \rangle )$

Строго говоря, эти три утверждения являются теоремами, которые, однако, вполне легко доказываются при помощи определений, данных выше.