Основы функционального программирования/Трансформация программ: различия между версиями
Содержимое удалено Содержимое добавлено
мНет описания правки |
Вставлены формулы, ссылки. Прочие правки |
||
Строка 1:
__TOC__
{{ОФП Содержание}}
Под [[w:Компьютерная программа|программой]] <math>P</math> на некотором [[w:Язык программирования|языке]] <math>L</math> понимается некоторый текст на <math>L</math>. В случае [[w:Язык функционального программирования|функционального языка]] под программой понимается набор [[w:Клоз|клозов]]. [[w:Семантика в программировании|Семантика]] же языка <math>L</math> определяется, если задан [[w:Интерпретатор|интерпретатор]] этого языка. Интерпретатор определяется формулой:
<math>\operatorname{Int} (P,\, d) =
<math>d</math> — исходные [[w:Данные (вычислительная техника)|данные]];
▲P — программа;
<math>d
Если интерпретатор <math>\mathrm{Int}</math> представлен в виде [[w:Лямбда-исчисление#Карринг|каррированной]] [[w:Функция (программирование)|функции]] <math>f</math> такой, что <math>f\, P\, d =
* Это определение можно понимать просто как [[w:Строковый тип|строку символов]], подаваемую на вход интерпретатора. Функция, вычисляемая интерпретатором по тексту <math>f = M\, f</math>, обозначается как
▲Если интерпретатор Int представлен в виде каррированной функции f такой, что f P d = d’, тогда определение f = M f, а точнее функционал M называется денотационной семантикой языка L. В этом случае имеет смысл -выражение: f P = d.M’ : D D’. При этом частичную функцию f P можно рассматривать как функцию fP одного аргумента, которая есть функция, реализующая программу P. Как было показано в предыдущей лекции, можно построить рекурсивное определение вида: fP = MP fP. Такой вид изначально имеют все программы на функциональном языке. Но эту запись можно понимать двояко:
* <math>f = M\, f</math> — есть чистое [[w:Функция (математика)|математическое определение функции]] <math>f</math>. Решение этого уравнения обозначается как
Резонный вопрос: каково соотношение этих двух функций —
▲*Это определение можно понимать просто как строку символов, подаваемую на вход интерпретатора. Функция, вычисляемая интерпретатором по тексту f = M f, обозначается как fint.
▲*f = M f — есть чистое математическое определение функции f. Решение этого уравнения обозначается как fmat.
'''Определение:''' говорят, что функция
▲Резонный вопрос: каково соотношение этих двух функций — fint и fmat? Надо полагать, что корректный интерпретатор как раз вычисляет fmat.
Как правило, <math>f_\mathrm{int} \subseteq f_\mathrm{mat}</math> — это происходит потому, что
▲Определение: говорят, что функция f1 менее определена, чем функция f2 (обозначается как ), если . Если для двух функций одновременно выполняется и , то имеет место тождество функций.
Трансформация программ — это просто [[w:Синтаксис (программирование)|синтаксические]] преобразования, во время которых совершенно не затрагивается семантика программ,
▲Как правило, — это происходит потому что, обычно интерпретатор реализует аппликативную стратегию редукции. Однако в дальнейших рассуждениях будет полагаться тождество функций fint и fmat, поэтому тексты программ будут рассматриваться как математическое определение функций. Тогда эквивалентное преобразование функциональных программ есть просто эквивалентные преобразования специального вида математических определений функций.
▲Трансформация программ — это просто синтаксические преобразования, во время которых совершенно не затрагивается семантика программ, т.к. программа воспринимается просто как набор символов. Обозначение того факта, что один текст f1 получаем при помощи синтаксических трансформаций другого текста f2, выглядит следующим образом: f1 |- f2.
Говорят, что преобразование
▲Говорят, что преобразование эквивалентно, если .
Далее вводится еще несколько специальных обозначений:
# Имеется исходный набор клозов (
# Клозы, описывающие функцию, которая содержит отображения из исходных клозов, обозначается как INV.
# Некоторые равенства, выражающие свойства внутренних (зарезервированных) функций, обозначаются как
'''Определение:''' пусть <math>F
== Виды преобразований ==
<math>\frac
{E_1(X) = E_2(X)}
{E_1[X \leftarrow M] = E_2[X \leftarrow M]}
</math>
<math>\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]}
</math>
<math>\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 ]}
</math>
<math>\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 ]}
</math>
<math>\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 ]}
</math>
<math>\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)}</math>
'''Пример 30. Преобразование функции <code>length</code>.'''
<code>length [] = 0
length (H:T) = 1 + length T
length_2
length_2 [] L
= length L 6 (LAW +) (*)
length_2 (H:T) L
Теперь остаётся взять два полученных клоза (*) и (**) и составить из них новое рекурсивное определение новой функции, не использующее вызова старой функции:
<code>length_2 [] L = length L
length_2 (H:T) L = 1 + length_2 T L</code>
Однако следует отметить, что выбор новых клозов для формирования нового определения требует дополнительных исследований, а не выполняется автоматически.
Подобная трансформация определений функций часто будет приводить к уменьшению сложности определения функций. Например, для функции, вычисляющей <math>N</math>-ое [[w:Числа Фибоначчи|число Фиббоначи]] можно построить определение, сложность вычисления которого линейно зависит от <math>N</math>, а не по закону Фиббоначи, как это есть для обычного определения.
Но трансформации следует делать обдуманно,
=== Второй закон информатики ===
* Существуют [[w:Алгоритмическая неразрешимость|неразрешимые задачи]].
* Не существует эффективной реализации для [[w:Декларативный язык программирования|декларативных языков]], если они универсальны.
'''Концепция трансформационного синтеза:''' позволить программисту писать определения функций, не заботясь об их эффективности.
Однако было доказано, что по [[w:Язык спецификаций|языку спецификаций]] невозможно выработать (
== Частичные вычисления ==
Пусть <math>P</math> и <math>S</math> — два языка, работающих со строками символов (это не нарушает общности рассуждений), а <math>\mathbf P</math> и <math>\mathbf S</math> — [[w:Множество|множества]] синтаксически правильных программ на соответствующих языках. <math>D</math> — [[w:Домен (базы данных)|домен]] всевозможных символьных последовательностей.
<math>P :: D
Если <math>p</math> — программа из <math>\mathbf P</math>, то:
<math>P
<math>P
<math>P
В последнем равенстве переменными
Частичным вычислителем MIX называется программа из <math>\mathbf P</math> (хотя, частичный вычислитель может быть реализован на любом языке)
<math>\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</math>.
Интерпретатором языка <math>S</math> называется программа <math>\mathrm{INT}
<math>\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)</math>.
Компилятором языка <math>S</math> называется программа <math>\mathrm{COMP}
<math>P(\mathrm{COMP})(\langle s \rangle) = \mathrm{TARGET}</math>
<math>P(\mathrm{TARGET})(\langle d_1,\, \dots,\, d_n \rangle) = S(s)(\langle d_1,\, \dots,\, d_n \rangle)</math>.
Или, что то же:
<math>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)</math>.
Компилятором компиляторов языка <math>S</math> называется программа <math>\mathrm{COCOM}
<math>P(\mathrm{COCOM})(\langle \mathrm{INT} \rangle) = \mathrm{COMP}</math>
▲Компилятором компиляторов языка S называется программа COCOM P, такая что:
<math>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)</math>.
=== Проекции
* <math>\mathrm{TARGET} = P
* <math>\mathrm{COMP} = P
* <math>\mathrm{COCOM} = P
Строго говоря, эти три утверждения являются [[w:Теорема|теоремами]], которые, однако, вполне легко [[w:Математическое доказательство|доказываются]] при помощи определений, данных выше.
| |||