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

Лекции по функциональному программированию

1. Вводная лекция 2. Структуры данных и базисные операции 3. Структуры данных и базисные операции — 2 4. Основы языка Haskell 5. Служебные слова и синтаксис Haskell'а 6. Модули и монады в Haskell'е 7. Операции ввода/вывода в Haskell'е 8. Конструирование функций 9. Доказательство свойств функций 10. Формализация ФП на основе λ-исчисления 11. Трансформация программ

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

Int (P, d) = d’

где:

P — программа;

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

d’ — выходные данные.

Если интерпретатор Int представлен в виде каррированной функции f такой, что f P d = d’, тогда определение f = M f, а точнее функционал M называется денотационной семантикой языка L. В этом случае имеет смысл -выражение: f P = d.M’ : D  D’. При этом частичную функцию f P можно рассматривать как функцию fP одного аргумента, которая есть функция, реализующая программу P. Как было показано в предыдущей лекции, можно построить рекурсивное определение вида: fP = MP fP. Такой вид изначально имеют все программы на функциональном языке. Но эту запись можно понимать двояко:

• Это определение можно понимать просто как строку символов, подаваемую на вход интерпретатора. Функция, вычисляемая интерпретатором по тексту f = M f, обозначается как fint.
• f = M f — есть чистое математическое определение функции f. Решение этого уравнения обозначается как fmat.

Резонный вопрос: каково соотношение этих двух функций — fint и fmat? Надо полагать, что корректный интерпретатор как раз вычисляет fmat.

Определение: говорят, что функция f1 менее определена, чем функция f2 (обозначается как ), если . Если для двух функций одновременно выполняется и , то имеет место тождество функций.

Как правило, — это происходит потому что, обычно интерпретатор реализует аппликативную стратегию редукции. Однако в дальнейших рассуждениях будет полагаться тождество функций fint и fmat, поэтому тексты программ будут рассматриваться как математическое определение функций. Тогда эквивалентное преобразование функциональных программ есть просто эквивалентные преобразования специального вида математических определений функций.

Трансформация программ — это просто синтаксические преобразования, во время которых совершенно не затрагивается семантика программ, т.к. программа воспринимается просто как набор символов. Обозначение того факта, что один текст f1 получаем при помощи синтаксических трансформаций другого текста f2, выглядит следующим образом: f1 |- f2.

Говорят, что преобразование корректно, если .

Говорят, что преобразование эквивалентно, если .

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

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

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

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

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

1. Преобразование без названия :)

1. Развертка (unfolding) — UNF.

1. Свертка (folding) — FLD.

1. Закон (law) — LAW.

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

Пример 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 — два языка, работающих со строками символов (это не нарушает общности рассуждений), а P и S — множества синтаксически правильных программ на соответствующих языках. D — домен всевозможных символьных последовательностей.

P :: D  (D*  D)

Если p — программа из P, то:

P (p) :: D*  D

P (p) (<d1, ..., dn>) = d, и d  D

P (r) (<y1, ..., yn>) = P (p) (<d1, ..., dm, y1, ..., yn>)

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

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

.

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

Интерпретатором языка S называется программа INT  P, такая что:

.

Компилятором языка S называется программа COMP  P, такая что:

.

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

.

Компилятором компиляторов языка S называется программа COCOM  P, такая что:

.

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

• TARGET = P (MIX) (<INT, s>)
• COMP = P (MIX) (<MIX, INT>)
• COCOM = P (MIX) (<MIX, MIX>)

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