Основы функционального программирования/Трансформация программ
Под программой 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.
Говорят, что преобразование корректно, если .
Говорят, что преобразование эквивалентно, если .
Далее вводится еще несколько специальных обозначений:
- Имеется исходный набор клозов (т.е. объектов преобразования), и этот набор будет обозначаться либо DEF, либо SPEC.
- Клозы, описывающие функцию, которая содержит отображения из исходных клозов, обозначается как INV.
- Некоторые равенства, выражающие свойства внутренних (зарезервированных) функций, обозначаются как LOW.
Определение: пусть F (X) — некоторое выражение (равенство), в котором выделены все свободные вхождения терма X. Тогда F [X M] называется примером F. При этом считается, что M — это некоторое выражение.
Виды преобразований[править | править код]
- Конкретизация (instantiation) — INS.
- Преобразование без названия :)
- Развертка (unfolding) — UNF.
- Свертка (folding) — FLD.
- Закон (law) — LAW.
- Абстракция и аппликация (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>)
Строго говоря, эти три утверждения являются теоремами, которые, однако, вполне легко доказываются при помощи определений, данных выше.