Основы функционального программирования/Формализация функционального программирования на основе лямбда-исчисления: различия между версиями
Содержимое удалено Содержимое добавлено
Пока лишь копия текста из MS Word - необходима стилизация |
Первоначальная викификация |
||
Строка 1:
= Лекция 10. «Формализация Функционального Программирования на основе
*Объект изучения: множество определений функций.
*Предположение: будет считаться, что любая функция может быть определена при помощи некоторого -выражения.
*Цель исследования: установить по двум определениям функций <f1> и <f2> их тождество на всей области определения — . (Здесь использована такая нотация: f — некоторая функция, <f> — определения этой функции в терминах -исчисления).
Проблема заключается в том, что обычно при описании функций задается интенсионал этих функций, а потом требуется установить экстенсиональное равенство. Под экстенсионалом функции понимается её график (ну или таблица в виде множества пар <аргумент, значение>). Под интенсионалом функции понимаются правила вычисления значения функции по заданному аргументу.
Возникает вопрос: как учесть семантику встроенных функций при сравнении их экстенсионалов (т.к. явно определения этих функций не известны)? Варианты ответов:
#Можно попытаться выразить семантику встроенных функций при помощи механизма -исчисления. Этот процесс можно довести до случая, когда все встроенные функции не содержат непроинтерпретированных операций.
#Говорят, что <f1> и <f2> семантически равны (этот факт обозначается как |= f1 = f2), если f1 (x) = f2 (x) при любой интерпретации непроинтерпретированных идентификаторов.
== Понятие формальной системы ==
Формальная система представляет собой четверку:
P = <V, Ф, A, R>, где
V — алфавит.
Ф — множество правильно построенных формул.
А — аксиомы (при этом А Ф).
R — правила вывода.
В рассматриваемой задаче формулы имеют вид (t1 = t2), где t1 и t2 — -выражения. Если некоторая формула выводима в формальной системе, то этот факт записывается как (| t1 = t2).
Говорят, что формальная система корректна, если (| t1 = t2) (|= t1 = t2).
Говорят, что формальная система полна, если (|= t1 = t2) (| t1 = t2).
Семантическое определение понятия «конструкция» (обозначение — Exp):
Примечание: Id — множество идентификаторов.
Говорят, что v свободна в M Exp, если:
#M = (M1M2), и v свободна в M1 или в M2. Множество идентификаторов v, свободных в M, обозначается как FV (M).
Говорят, что v связана в M Exp, если:
#M = v’.M’, и v = v’.
#M = (M1M2), и v связана в M1 или в M2 (т.е. один и тот же идентификатор может быть свободен и связан в Exp).
#M = (M’), и v связана в M’.
'''Пример 26. Свободные и связанные идентификаторы.'''
#M = x.xy. x — связана, y — свободна.
#M = (v.v)v. v входит в это выражение как свободно, так и связанно.
#M = VW. V и W — свободны.
Правило подстановки: подстановка в выражение E выражения E’ вместо всех свободных вхождений переменной x обозначается как E[x E’]. Во время подстановки иногда случается так, что получается конфликт имён, т.е. коллизия переменных. Примеры коллизий:
(x.yx)[y z.z] = x.(z.z)x = x.x — корректная подстановка
(x.yx)[y xx] = x.(xx)x — коллизия имён переменных
(z.yz)[y xx] = z.(xx)z — корректная подстановка
Точное определение базисной подстановки:
#(x.E)[x E’] = x.E == Построение формальной системы ==
Таким образом, сейчас уже все готово для того, чтобы перейти к построению формальной системы, определяющей Функциональное Программирование в терминах Правильно построенные формулы выглядят так: Exp = Exp.
Аксиомы:
|- x.E = y.E[x y] ()
|- (x.E)E’ = E[x E’] ()
|- t = t, в случае, если t — идентификаторы ()
Правила вывода:
t1 = t2 t1t3 = t2t3 ()
t1 = t2 t3t1 = t3t2 ()
t1 = t2 t2 = t1 ()
t1 = t2, t2 = t3 t1 = t3 ()
t1 = t2 x.t1 = x.t2 ()
(x.xy)(z.(u.zu))v = (v.yv)v
(): (x.xy)(z.(u.zu)) = (v.yv)
(): (z.(u.zu))y = (v.yv)
(): u.yu = v.yv — выводима.
Во втором варианте формализации Функционального Программирования можно воспользоваться не свойством симметричности отношения «=», а свойством несимметричности отношения «».
Во второй формальной системе правильно построенные формулы выглядят абсолютно так же, как и в первом варианте. Однако аксиомы принимают несколько иной вид:
|- x.M y.M[x y] (’)
|- (x.M)N M[x N] (’)
|- M M (’)
Правило вывода во втором варианте формальной системы одно:
t1 t1’, t2 t2’ t1t2 t1’t2’ ()
По существу это правило вывода гласит, что в любом выражении можно выделить вхождения подвыражения и заменить их все любой редукцией из этого подвыражения.
Определения:
*Выражение вида (x.M)N называется -редексом.
*Выражения, не содержащие -редексов, называются выражениями в нормальной форме.
Несколько теорем (без доказательств):
*E E1 E E2 F : E1 F E2 F. (Теорема Чёрча-Россера). == Стратегия редукции ==
#Нормальная редукционная стратегия. На каждом шаге редукции выбирается текстуально самый левый -редекс. Доказано, что нормальная редукционная стратегия гарантирует получение нормальной формы выражения, если она существует.
#Аппликативная редукционная стратегия. На каждом шаге редукции выбирается редекс, не содержащий внутри себя других -редексов. Далее будет показано, что аппликативная редукционная стратегия не всегда позволяет получить нормальную форму выражения.
'''Пример 28. Редукция выражения M = (y.x)(EE), где E = x.xx'''
#НРС: (y.x)(EE) = (y.x)[y EE] = x.
#АРС: (y.x)(EE) = (y.x)((x.xx)(x.xx)) = (y.x)((x.xx)(x.xx)) = ...
В этом примере видно, как апликативная редукционная стратегия может привести к выпадению в дурную бесконечность. Получить нормальную форму выражения M в случае применения аппликативной редукционной стратегии невозможно.
Примечание: красным шрифтом выделен -редекс, редуцируемый следующим шагом.
'''Пример 29. Редукция выражения M = (x.xyxx)((z.z)w)'''
#НРС: (x.xyxx)((z.z)w) = ((z.z)w)y((z.z)w)((z.z)w) = wy((z.z)w)((z.z)w) = wyw((z.z)w) = wyww.
#АРС: (x.xyxx)((z.z)w) = (x.xyxx)w = wyww.
В программировании нормальная редукционная стратегия соответствует вызову по имени. Т.е. аргумент выражения не вычисляется до тех пор, пока к нему не возникнет обращения в теле выражения. Аппликативная редукционная стратегия соответствует вызову по значению.
== Соответствие между вычислениями функциональных программ и редукцией ==
Работа интерпретатора описывается несколькими шагами:
#Если выделенное на первом шаге обращение к рекурсивной функции, то вместо него подставляется тело функции с фактическими параметрами (т.к. они уже означены). Далее происходит переход на начало первого шага.
#Если больше обращений нет, то происходит остановка.
В принципе, вычисления в функциональной парадигме повторяют шаги редукции, но дополнительно содержат вычисления встроенных функций.
== Представление определений функций в виде λ-выражений ==
Показано, что любое определение функции можно представить в виде -выражения, не содержащего рекурсии. Например:
fact = n.if n == 0 then 1 else n * fact (n – 1)
То же самое определение можно описать при помощи использования некоторого функционала:
fact = (f.n.if n == 0 then 1 else n * f (n – 1)) fact
Жирным шрифтом в представленном выражении выделен функционал F. Таким образом, функцию вычисления факториала можно записать так: fact = F fact. Можно видеть, что любое рекурсивное определение некоторой функции f можно представить в таком виде:
f = F f
Это выражение можно трактовать как уравнение, в котором рекурсивная функция f является неподвижной точкой функционала F. Соответственно интерпретатор функционального языка можно в таком же ключе рассматривать как численный метод решения этого уравнения.
Можно сделать предположение, что этот численный метод (т.е. интерпретатор) в свою очередь может быть реализован при помощи некоторой функции Y, которая для функционала F находит его неподвижную точку (соответственно определяя искомую функцию) — f = Y F.
Свойства функции Y определяются равенством:
Y F = F (Y F)
Теорема (без доказательства):
Любой λ-терм имеет неподвижную точку.
λ-исчисление позволяет выразить любую функцию через чистое λ-выражение без использования встроенных функций. Например:
#prefix = λxyz.zxy
head = λp.p(λxy.x)
tail = λp.p(λxy.y)
#Моделирование условных выражений:
True = λxy.x
False = λxy.y
if B then M else N = BNM, где B = {True, False}.
| |||