Викиучебник

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

Интерактивная навигация по истории
← Предыдущая правкаСледующая правка →
Содержимое удалено Содержимое добавлено
ВизуальныйВики-текст
Вставлены формулы, ссылки. Прочие правки.
Строка 1:
__TOC__
 
{{ОФП Содержание}}
 
* '''Объект изучения:''' [[w:Множество|множество]] определений [[w:Функция (математика)|функций]].
* '''[[w:Гипотеза|Предположение]]:''' будет считаться, что любая функция может быть определена при помощи некоторого λ[[w:Лямбда-исчисление|λ]]-[[w:Алгебраическое выражение|выражения]].
* '''Цель исследования:''' установить по двум определениям функций <f1math>\langle f_1 \rangle</math> и <f2math>\langle f_2 \rangle</math> их [[w:Тождество (математика)|тождество]] на всей [[w:Область определения|области определения]] — <math>\forall x : f_1(x) = f_2(x)</math>. (Здесь использована такая [[w:Математическая нотация|нотация]]: <math>f</math> — некоторая функция, <math>\langle f \rangle</math> — определения этой функции в терминах &lambda;[[w:Лямбда-исчисление|λ-исчисления)]].)
 
Проблема заключается в том, что обычно при описании функций задаетсязадаётся [[w:Интенсионал|интенсионал]] этих функций, а потом требуется установить [[w:Экстенсионал|экстенсиональное]] равенство. Под экстенсионалом функции понимается её [[w:График функции|график]] (ну или таблица в виде множества пар <〈аргумент, значение>〉). Под интенсионалом функции понимаются правила [[w:Вычисление|вычисления]] [[w:Значение функции|значения функции]] по заданному [[w:Аргумент функции|аргументу]].
 
Возникает вопрос: как учесть [[w:Семантика в программировании|семантику]] встроенных функций при сравнении их экстенсионалов (т.к.так как явно определения этих функций не известнынеизвестны)? Варианты ответов:
 
# Можно попытаться выразить семантику встроенных функций при помощи механизма &lambda;λ-исчисления. Этот процесс можно довести до случая, когда все встроенные функции не содержат [[w:Интерпретация (информатика)|непроинтерпретированных]] операций.
# Говорят, что <f1math>\langle f_1 \rangle</math> и <f2math>\langle f_2 \rangle</math> семантически равны (этот факт обозначается как |=<math>\vDash f1f_1 = f2f_2</math>), если f1 <math>f_1(x) = f2 f_2(x)</math> при ''любой'' интерпретации непроинтерпретированных идентификаторов.
 
== Понятие [[w:Формальная система|формальной системы]] ==
 
Формальная система представляет собой четверкучетвёрку:
 
<math>P = <\langle V,\, Ф\Phi,\, A,\, R \rangle</math>, где
 
где <math>V</math> — [[w:Алфавит (математика)|алфавит.]];
 
Ф<math>\Phi</math> — множество правильно построенных [[w:Математическая формула|формул.]];
 
А<math>A</math> — [[w:Аксиома|аксиомы]] (при этом А<math>A &lambda;\subseteq Ф\Phi</math>).;
 
<math>R</math> — правила [[w:Вывод формулы|вывода]].
 
В рассматриваемой задаче формулы имеют вид <math>(t1t_1 = t2t_2)</math>, где t1<math>t_1</math> и t2<math>t_2</math> — &lambda;λ-выражения. Если некоторая формула выводима в формальной системе, то этот факт записывается как <math>(|\vdash t1t_1 = t2t_2)</math>.
 
Говорят, что формальная система корректна, если <math>(|\vdash t1t_1 = t2t_2) &lambda;\Rightarrow (|=\vDash t1t_1 = t2t_2)</math>.
 
Говорят, что формальная система полна, если <math>(|=\vDash t1t_1 = t2t_2) &lambda;\Rightarrow (| \vdash t1t_1 = t2t_2)</math>.
 
Семантическое определение понятия «конструкция» (обозначение — <math>\mathrm{Exp}</math>):
# .
# .
# .
# .
#Никаких других Exp нет.
 
1°. <math>v \in \mathrm{Id} \Rightarrow v \in \mathrm{Exp}</math>.
Примечание: Id — множество идентификаторов.
 
2°. <math>v \in \mathrm{Id},\, E \in \mathrm{Exp} \Rightarrow \lambda v.E \in \mathrm{Exp}</math>
Говорят, что v свободна в M &lambda; Exp, если:
 
3°. <math>E, E' \in \mathrm{Exp} \Rightarrow (EE') \in \mathrm{Exp}</math>
#M = v.
#M = (M1M2), и v свободна в M1 или в M2.
#M = &lambda;v’.M’, и v &lambda; v’, и v свободна в M’.
#M = (M’), и v свободна в M’.
 
4°. <math>E \in \mathrm{Exp} \Rightarrow (E) \in \mathrm{Exp}</math>
Множество идентификаторов v, свободных в M, обозначается как FV (M).
 
5°. Никаких других <math>\mathrm{Exp}</math> нет.
Говорят, что v связана в M &lambda; Exp, если:
 
Примечание: <math>\mathrm{Id}</math> — множество [[w:Идентификатор|идентификаторов]].
#M = &lambda;v’.M’, и v = v’.
#M = (M1M2), и v связана в M1 или в M2 (т.е. один и тот же идентификатор может быть свободен и связан в Exp).
#M = (M’), и v связана в M’.
 
Говорят, что <math>v</math> свободна в <math>M \in \mathrm{Exp}</math>, если:
'''Пример 26. Свободные и связанные идентификаторы.'''
 
1°. <math>M = v</math>.
#M = v. v — свободна.
#M = &lambda;x.xy. x — связана, y — свободна.
#M = (&lambda;v.v)v. v входит в это выражение как свободно, так и связанно.
#M = VW. V и W — свободны.
 
2°. <math>M = (M_1M_2)</math>, и <math>v</math> свободна в <math>M_1</math> или в <math>M_2</math>.
Правило подстановки: подстановка в выражение E выражения E’ вместо всех свободных вхождений переменной x обозначается как E[x &lambda; E’]. Во время подстановки иногда случается так, что получается конфликт имён, т.е. коллизия переменных. Примеры коллизий:
 
3°. <math>M = \lambda v'.M'</math>, и <math>v \neq v'</math>, и <math>v</math> свободна в <math>M'</math>.
(&lambda;x.yx)[y  &lambda;z.z] = &lambda;x.(&lambda;z.z)x = &lambda;x.x — корректная подстановка
 
4°. <math>M = (M')</math>, и <math>v</math> свободна в <math>M'</math>.
(&lambda;x.yx)[y  xx] = &lambda;x.(xx)x — коллизия имён переменных
 
Множество идентификаторов <math>v</math>, свободных в <math>M</math>, обозначается как <math>FV(M)</math>.
(&lambda;z.yz)[y  xx] = &lambda;z.(xx)z — корректная подстановка
 
Говорят, что <math>v</math> связана в <math>M \in \mathrm{Exp}</math>, если:
Точное определение базисной подстановки:
 
1°. <math>M = \lambda v'.M'</math>, и <math>v = v'</math>.
#x[x  E’] = E’
#y[x  E’] = y
#(&lambda;x.E)[x  E’] = &lambda;x.E
#(&lambda;y.E)[x  E’] = &lambda;y.E[x  E’], при условии, что y  FV (E’)
#(&lambda;y.E)[x  E’] = (&lambda;z.E[y  z])[x  E’], при условии, что y  FV (E’)
#(E1E2)[x  E’] = (E1[x  E’]E2[x  E’])
 
2°. <math>M = (M_1M_2)</math>, и <math>v</math> связана в <math>M_1</math> или в <math>M_2</math> (то есть один и тот же идентификатор может быть свободен и связан в <math>\mathrm{Exp}</math>).
== Построение формальной системы ==
 
3°. <math>M = (M')</math>, и <math>v</math> связана в <math>M'</math>.
Таким образом, сейчас уже все готово для того, чтобы перейти к построению формальной системы, определяющей Функциональное Программирование в терминах λ-исчисления.
 
'''Пример 26. Свободные и связанные идентификаторы.'''
Правильно построенные формулы выглядят так: Exp = Exp.
 
# <math>M = v</math>. <math>v</math> — свободна.
Аксиомы:
# <math>M = \lambda x.xy</math>. <math>x</math> — связана, <math>y</math> — свободна.
# <math>M = (\lambda v.v)v</math>. <math>v</math> входит в это выражение как свободно, так и связанно.
# <math>M = VW</math>. <math>V</math> и <math>W</math> — свободны.
 
'''Правило подстановки:''' подстановка в выражение <math>E</math> выражения <math>E'</math> вместо всех свободных вхождений переменной <math>x</math> обозначается как <math>E[x \leftarrow E']</math>. Во время подстановки иногда случается так, что получается конфликт имён, то есть коллизия переменных. Примеры коллизий:
|- &lambda;x.E = &lambda;y.E[x  y] ()
 
<math>(\lambda x.yx)[y \leftarrow \lambda z.z] = \lambda x.(\lambda z.z)x = \lambda x.x</math> — корректная подстановка;
|- (&lambda;x.E)E’ = E[x  E’] ()
 
<math>(\lambda x.yx)[y \leftarrow xx] = \lambda x.(xx)x</math> — коллизия имён переменных;
|- t = t, в случае, если t — идентификаторы ()
 
<math>(\lambda z.yz)[y \leftarrow xx] = \lambda z.(xx)z</math> — корректная подстановка.
Правила вывода:
 
Точное определение базисной подстановки:
t1 = t2  t1t3 = t2t3 ()
 
1°. <math>x[x \leftarrow E'] = E'</math>.
t1 = t2  t3t1 = t3t2 ()
 
2°. <math>y[x \leftarrow E'] = y</math>.
t1 = t2  t2 = t1 ()
 
3°. <math>(\lambda x.E)[x \leftarrow E'] = \lambda x.E</math>.
t1 = t2, t2 = t3  t1 = t3 ()
 
4°. <math>(\lambda y.E)[x \leftarrow E'] = \lambda y.E[x \leftarrow E']</math>, при условии, что <math>y \not\in FV(E')</math>.
t1 = t2  &lambda;x.t1 = &lambda;x.t2 ()
 
5°. <math>(\lambda y.E)[x \leftarrow E'] = \Big( \lambda z.E[y \leftarrow z] \Big) [x \leftarrow E']</math>, при условии, что <math>y \in FV(E')</math>.
'''Пример 27. Доказать выводимость формулы: (&lambda;x.xy)(&lambda;z.(&lambda;u.zu))v = (&lambda;v.yv)v'''
 
6°. <math>(E_1\,E_2)[x \leftarrow E'] = \Big( E_1[x \leftarrow E']\, E_2[x \leftarrow E'] \Big)</math>.
(&lambda;x.xy)(&lambda;z.(&lambda;u.zu))v = (&lambda;v.yv)v
 
=== Построение формальной системы ===
(): (&lambda;x.xy)(&lambda;z.(&lambda;u.zu)) = (&lambda;v.yv)
 
Таким образом, сейчас уже всё готово для того, чтобы перейти к построению формальной системы, определяющей [[w:Функциональное программирование|функциональное программирование]] в терминах λ-исчисления.
(): (&lambda;z.(&lambda;u.zu))y = (&lambda;v.yv)
 
Правильно построенные формулы выглядят так: <math>\mathrm{Exp} = \mathrm{Exp}</math>.
(): &lambda;u.yu = &lambda;v.yv — выводима.
 
Аксиомы:
Во втором варианте формализации Функционального Программирования можно воспользоваться не свойством симметричности отношения «=», а свойством несимметричности отношения «».
{| width="100%"
| <math>\vdash \lambda x.E = \lambda y.E[x \leftarrow y]</math>; || align="right" | (α)
|-
| <math>\vdash (\lambda x.E)E' = E[x \leftarrow E']</math>; || align="right" | (β)
|-
| <math>\vdash t = t</math>, в случае, если <math>t</math> — идентификаторы. || align="right" | (ρ)
|}
 
Правила вывода:
Во второй формальной системе правильно построенные формулы выглядят абсолютно так же, как и в первом варианте. Однако аксиомы принимают несколько иной вид:
 
{| width="100%"
|- &lambda;x.M  &lambda;y.M[x  y] (’)
| <math>t_1 = t_2 \Rightarrow t_1t_3 = t_2t_3</math>; || align="right" | (μ)
|-
| <math>t_1 = t_2 \Rightarrow t_3t_1 = t_3t_2</math>; || align="right" | (ν)
|-
| <math>t_1 = t_2 \Rightarrow t_2 = t_1</math>; || align="right" | (σ)
|-
| <math>t_1 = t_2,\, t_2 = t_3 \Rightarrow t_1 = t_3</math>; || align="right" | (τ)
|-
| <math>t_1 = t_2 \Rightarrow \lambda x.t_1 = \lambda x.t_2</math>. || align="right" | (ξ)
|-
|}
 
'''Пример 27. [[w:w:Математическое доказательство|Доказать]] выводимость формулы <math>(\lambda x.xy)(\lambda z.(\lambda u.zu))v = (\lambda v.yv)v</math>'''
|- (&lambda;x.M)N  M[x  N] (’)
 
{|
| || <math>(\lambda x.xy)(\lambda z.(\lambda u.zu))v = (\lambda v.yv)v</math>;
|-
| (μ): || <math>(\lambda x.xy)(\lambda z.(\lambda u.zu)) = (\lambda v.yv)</math>;
|-
| (β): || <math>(\lambda z.(\lambda u.zu))y = (\lambda v.yv)</math>;
|-
| (α): || <math>\lambda u.yu = \lambda v.yv</math> — выводима.
|}
 
Во втором варианте формализации функционального программирования можно воспользоваться не свойством симметричности отношения «<math>=</math>», а свойством несимметричности отношения «<math>\to</math>».
 
Во второй формальной системе правильно построенные формулы выглядят абсолютно так же, как и в первом варианте. Однако аксиомы принимают несколько иной вид:
 
{| width="100%"
|- M  M (’)
| <math>\vdash \lambda x.M \to \lambda y.M[x \leftarrow y]</math> || align="right" | (α′)
|-
| <math>\vdash (\lambda x.M)N \to M[x \leftarrow N]</math> || align="right" | (β′)
|-
| <math>\vdash M \to M</math> || align="right" | (ρ′)
|}
 
Правило вывода во втором варианте формальной системы одно:
 
{| width="100%"
t1  t1’, t2  t2’  t1t2  t1’t2’ ()
| <math>t_1 \to t_1',\, t_2 \to t_2' \Rightarrow t_1t_2 \to t_1't_2'</math> || align="right" | (π)
|}
 
По существу это правило вывода гласит, что в любом выражении можно выделить вхождения подвыражения и заменить их все любой [[w:Редукция|редукцией]] из этого подвыражения.
 
'''Определения:'''
 
* Выражение вида &<math>\lambda; x.M</math> называется α-редексом.
* Выражение вида <math>(&\lambda; x.M)N</math> называется β-редексом.
* Выражения, не содержащие β-редексов, называются выражениями в нормальной форме.
 
Несколько [[w:Теорема|теорем]] (без доказательств):
 
* <math>\vdash E_1 = E_2 \Rightarrow E_1 \to E_2 \lor E_2 \to E_1</math>.
*|- E1 = E2  E1  E2  E2  E1.
* <math>E \to E1E_1 \land E \to E2E_2 \Rightarrow F\exist F : E1E_1 \to F \land E2E_2 \to F</math>. ([[w:Теорема Чёрча—Россера|Теорема Чёрча-РоссераЧёрча—Россера]]).
* Если <math>E</math> имеет нормальные формы E1<math>E_1</math> и E2<math>E_2</math>, то они эквивалентны с точностью до α-конверсии, т.е.то есть различаются только обозначением связанных переменных.
 
=== Стратегия редукции ===
 
#1°. '''[[w:Нормальная редукционная стратегия|Нормальная редукционная стратегия]] (НРС).''' На каждом шаге редукции выбирается текстуально самый левый β-редекс. Доказано, что нормальная редукционная стратегия гарантирует получение нормальной формы выражения, если она существует.
#Аппликативная редукционная стратегия. На каждом шаге редукции выбирается  редекс, не содержащий внутри себя других -редексов. Далее будет показано, что аппликативная редукционная стратегия не всегда позволяет получить нормальную форму выражения.
 
2°. '''[[w:Аппликативная редукционная стратегия|Аппликативная редукционная стратегия]] (АРС).''' На каждом шаге редукции выбирается β-редекс, не содержащий внутри себя других β-редексов. Далее будет показано, что аппликативная редукционная стратегия не всегда позволяет получить нормальную форму выражения.
'''Пример 28. Редукция выражения M = (&lambda;y.x)(EE), где E = &lambda;x.xx'''
 
'''Пример 28. Редукция выражения <math>M = (\lambda y.x)(EE)</math>, где <math>E = \lambda x.xx</math>'''
#НРС: (&lambda;y.x)(EE) = (&lambda;y.x)[y  EE] = x.
#АРС: (&lambda;y.x)(EE) = (&lambda;y.x)((&lambda;x.xx)(&lambda;x.xx)) = (&lambda;y.x)((&lambda;x.xx)(&lambda;x.xx)) = ...
 
1°. НРС: <math>\underline{(\lambda y.x)}(EE) = \underline{(\lambda y.x)}[y \leftarrow EE] = x</math>.
В этом примере видно, как апликативная редукционная стратегия может привести к выпадению в дурную бесконечность. Получить нормальную форму выражения M в случае применения аппликативной редукционной стратегии невозможно.
 
2°. АРС: <math>(\lambda y.x)\underline{(EE)} = (\lambda y.x)\underline{ \Big( (\lambda x.xx)(\lambda x.xx) \Big)} = (\lambda y.x)\underline{ \Big( (\lambda x.xx)(\lambda x.xx) \Big)} = \dots</math>.
Примечание: красным шрифтом выделен -редекс, редуцируемый следующим шагом.
 
В этом примере видно, как апликативная редукционная стратегия может привести к выпадению в [[w:Дурная бесконечность|дурную бесконечность]]. Получить нормальную форму выражения <math>M</math> в случае применения аппликативной редукционной стратегии невозможно.
'''Пример 29. Редукция выражения M = (&lambda;x.xyxx)((&lambda;z.z)w)'''
 
''Примечание:'' подчёркиванием выделен β-редекс, редуцируемый следующим шагом.
#НРС: (&lambda;x.xyxx)((&lambda;z.z)w) = ((&lambda;z.z)w)y((&lambda;z.z)w)((&lambda;z.z)w) = wy((&lambda;z.z)w)((&lambda;z.z)w) = wyw((&lambda;z.z)w) = wyww.
#АРС: (&lambda;x.xyxx)((&lambda;z.z)w) = (&lambda;x.xyxx)w = wyww.
 
'''Пример 29. Редукция выражения <math>M = (\lambda x.xyxx) \Big( (\lambda z.z)w \Big)</math>'''
В программировании нормальная редукционная стратегия соответствует вызову по имени. Т.е. аргумент выражения не вычисляется до тех пор, пока к нему не возникнет обращения в теле выражения. Аппликативная редукционная стратегия соответствует вызову по значению.
 
1°. НРС: <math>\underline{(\lambda x.xyxx)} \Big( (\lambda z.z)w \Big) = \underline{ \Big( (\lambda z.z)w \Big) } y \Big( (\lambda z.z)w \Big) \Big( (\lambda z.z)w \Big) =</math>
 
<math>= wy \underline{ \Big( (\lambda z.z)w \Big) } \Big( (\lambda z.z)w \Big) = wyw \underline{ \Big( (\lambda z.z)w \Big) } = wyww</math>.
 
2°. АРС: <math>(\lambda x.xyxx) \underline{ \Big( (\lambda z.z)w \Big)} = \underline{(\lambda x.xyxx)} w = wyww</math>.
 
В программировании нормальная редукционная стратегия соответствует вызову по имени. То есть аргумент выражения не вычисляется до тех пор, пока к нему не возникнет обращения в теле выражения. Аппликативная редукционная стратегия соответствует вызову по значению.
 
== Соответствие между вычислениями функциональных программ и редукцией ==
 
Работа [[w:Интерпретатор|интерпретатора]] описывается несколькими шагами:
 
# В выражении необходимо выделить некоторое обращение к [[w:Рекурсия|рекурсивной]] или встроенной функции с полностью означенными аргументами. Если выделенное обращение к встроенной функции существует, то происходит его выполнение и возврат к началу первого шага.
# Если выделенное на первом шаге обращение к рекурсивной функции, то вместо него подставляется тело функции с фактическими параметрами (т.к.так как они уже означены). Далее происходит переход на начало первого шага.
# Если больше обращений нет, то происходит остановка.
 
В принципе, вычисления в функциональной парадигме повторяют шаги редукции, но дополнительно содержат вычисления встроенных функций.
 
=== Представление определений функций в виде λ-выражений ===
 
Показано, что любое определение функции можно представить в виде &lambda;λ-выражения, не содержащего рекурсии. Например:
 
<code>fact = &lambda;nλn.if n == 0 then 1 else n * fact (n – 1)</code>
 
То же самое определение можно описать при помощи использования некоторого [[w:Функция высшего порядка|функционала]]:
 
<code>fact = '''(&lambda;fλf.&lambda;nλn.if n == 0 then 1 else n * f (n – 1))''' fact</code>
 
Жирным шрифтом в представленном выражении выделен функционал <code>F</code>. Таким образом, функцию вычисления [[w:Факториал|факториала]] можно записать так: <code>fact = F fact</code>. Можно видеть, что любое рекурсивное определение некоторой функции <code>f</code> можно представить в таком виде:
 
<code>f = F f</code>
 
Это выражение можно трактовать как уравнение, в котором рекурсивная функция <code>f</code> является [[w:Неподвижная точка (математика)|неподвижной точкой]] функционала <code>F</code>. Соответственно интерпретатор функционального языка можно в таком же ключе рассматривать как численный метод решения этого уравнения.
 
Можно сделать предположение, что этот численный метод (т.е.то есть интерпретатор) в свою очередь может быть реализован при помощи некоторой функции <code>Y</code>, которая для функционала <code>F</code> находит его неподвижную точку (соответственно определяя искомую функцию) — <code>f = Y F</code>.
 
Свойства функции <code>Y</code> определяются равенством:
 
<code>Y F = F (Y F)</code>
 
'''Теорема''' (без доказательства):
 
Любой λ-терм имеет неподвижную точку.
Строка 204 ⟶ 235 :
λ-исчисление позволяет выразить любую функцию через чистое λ-выражение без использования встроенных функций. Например:
 
1°.
#prefix = λxyz.zxy
<code>prefix = λxyz.zxy
head = λp.p(λxy.x)
tail head = λp.p(λxy.yx)
tail = λp.p(λxy.y)</code>
#Моделирование условных выражений:
True = λxy.x
2°. Моделирование условных выражений:
False = λxy.y
 
if B then M else N = BNM, где B = {True, False}.
<code>True = λxy.x
False = λxy.y
if B then M else N = BNM, где B = {True, False}</code>.
Источник — https://ru.wikibooks.org/wiki/Основы_функционального_программирования/Формализация_функционального_программирования_на_основе_лямбда-исчисления