1. Нашёл ошибку?
2. Выдели её мышью.
3. Нажми Ctrl-Enter.

[ закрыть ]

Лекция 10. "Формализация Функционального Программирования на основе l-исчисления"

Понравились лекции? Используете их для обучения? Можете отблагодарить автора:

рублей Яндекс.Деньгами
на счет 4100137733052 (Лекции по Функциональному программированию)

  • Объект изучения: множество определений функций.
  • Предположение: будет считаться, что любая функция может быть определена при помощи некоторого l-выражения.
  • Цель исследования: установить по двум определениям функций <f1> и <f2> их тождество на всей области определения — . (Здесь использована такая нотация: f — некоторая функция, — определения этой функции в терминах l-исчисления)

Проблема заключается в том, что обычно при описании функций задается интенсионал этих функций, а потом требуется установить экстенсиональное равенство. Под экстенсионалом функции понимается её график (ну или таблица в виде множества пар <аргумент, значение>). Под интенсионалом функции понимаются правила вычисления значения функции по заданному аргументу.

Возникает вопрос: как учесть семантику встроенных функций при сравнении их экстенсионалов (т.к. явно определения этих функций не известны)? Варианты ответов:

  1. Можно попытаться выразить семантику встроенных функций при помощи механизма l-исчисления. Этот процесс можно довести до случая, когда все встроенные функции не содержат непроинтерпретированных операций.
  2. Говорят, что <f1> и <f2> семантически равны (этот факт обозначается как |= f1 = f2), если f1 (x) = f2 (x) при любой интерпретации непроинтерпретированных идентификаторов.

Понятие формальной системы

Формальная система представляет собой четверку:

P = <V, Ф, A, R>, где

V — алфавит.

Ф — множество правильно построенных формул.

А — аксиомы (при этом А in Ф).

R — правила вывода.

В рассматриваемой задаче формулы имеют вид (t1 = t2), где t1 и t2 &mdashl l-выражения. Если некоторая формула выводима в формальной системе, то этот факт записывается как (|- t1 = t2).

Говорят, что формальная система корректна, если (|- t1 = t2) => (|= t1 = t2).

Говорят, что формальная система полна, если (|= t1 = t2) => (|- t1 = t2).

Семантическое определение понятия "конструкция" (обозначение — Exp):





  1. Никаких других Exp нет.

Примечание: Id — множество идентификаторов.

Говорят, что v свободна в M Exp, если:

  1. M = v.
  2. M = (M1M2), и v свободна в M1 или в M2.
  3. M = lv'.M', и v != v', и v свободна в M'.
  4. M = (M'), и v свободна в M'.

Множество идентификаторов v, свободных в M, обозначается как FV (M).

Говорят, что v связана в M in Exp, если:

  1. M = lv'.M', и v = v'.
  2. M = (M1M2), и v связана в M1 или в M2 (т.е. один и тот же идентификатор может быть свободен и связан в Exp).
  3. M = (M'), и v связана в M'.

Пример 26. Свободные и связанные идентификаторы.

    M = v. v — свободна. M = lx.xy. x — связана, y — свободна. M = (lv.v)v. v входит в это выражение как свободно, так и связанно. M = VW. V и W — свободны.

Правило подстановки: подстановка в выражение E выражения E' вместо всех свободных вхождений переменной x обозначается как E[x <- E']. Во время подстановки иногда случается так, что получается конфликт имён, т.е. коллизия переменных. Примеры коллизий:

(lx.yx)[y <- lz.z] = lx.(lz.z)x = lx.x — корректная подстановка

(lx.yx)[y <- xx] = lx.(xx)x — коллизия имён переменных

(lz.yz)[y <- xx] = lz.(xx)z — корректная подстановка

Точное определение базисной подстановки:

  1. x[x <- E'] = E'
  2. y[x <- E'] = y
  3. (lx.E)[x <- E'] = lx.E
  4. (ly.E)[x <- E'] = ly.E[x <- E'], при условии, что y in FV (E')
  5. (ly.E)[x <- E'] = (lz.E[y <- z])[x <- E'], при условии, что y !in FV (E')
  6. (E1E2)[x <- E'] = (E1[x <- E']E2[x <- E'])

Построение формальной системы

Таким образом, сейчас уже все готово для того, чтобы перейти к построению формальной системы, определяющей Функциональное Программирование в терминах l-исчисления.

Правильно построенные формулы выглядят так: Exp = Exp.

Аксиомы:

(a): |- lx.E = ly.E[x <- y]

(b): |- (lx.E)E' = E[x <- E']

(r): |- t = t, в случае, если t — идентификаторы

Правила вывода:

(m): t1 = t2 => t1t3 = t2t3

(n): t1 = t2 => t3t1 = t3t2

(s): t1 = t2 => t2 = t1

(t): t1 = t2, t2 = t3 => t1 = t3

(x): t1 = t2 => lx.t1 = lx.t2

Пример 27. Доказать выводимость формулы: (lx.xy)(lz.(lu.zu))v = (lv.yv)v

(lx.xy)(lz.(lu.zu))v = (lv.yv)v

(m): (lx.xy)(lz.(lu.zu)) = (lv.yv)

(b): z.(lu.zu))y = (lv.yv)

(a): u.yu = lv.yv — выводима.

Во втором варианте формализации Функционального Программирования можно воспользоваться не свойством симметричности отношения "=", а свойством несимметричности отношения "->".

Во второй формальной системе правильно построенные формулы выглядят абсолютно так же, как и в первом варианте. Однако аксиомы принимают несколько иной вид:

(a'): |- lx.M -> ly.M[x <- y]

(b'): |- (lx.M)N -> M[x <- N]

(r'): |- M -> M

Правило вывода во втором варианте формальной системы одно:

(p): t1 -> t1', t2 -> t2' => t1t2 -> t1't2'

По существу это правило вывода гласит, что в любом выражении можно выделить вхождения подвыражения и заменить их все любой редукцией из этого подвыражения.

Определения:

  • Выражение вида lx.M называется a-редексом.
  • Выражение вида (lx.M)N называется b-редексом.
  • Выражения, не содержащие b-редексов, называются выражениями в нормальной форме.

Несколько теорем (без доказательств):

  • |- E1 = E2 => E1 -> E2 | E2 -> E1.
  • E -> E1 & E -> E2 => Существует F : E1 -> F & E2 > F. (Теорема Чёрча-Россера).
  • Если E имеет нормальные формы E1 и E2, то они эквивалентны с точностью до a-конверсии, т.е. различаются только обозначением связанных переменных.
Стратегия редукции

1. Нормальная редукционная стратегия. На каждом шаге редукции выбирается текстуально самый левый b-редекс. Доказано, что нормальная редукционная стратегия гарантирует получение нормальной формы выражения, если она существует.

2. Аппликативная редукционная стратегия. На каждом шаге редукции выбирается b-редекс, не содержащий внутри себя других b-редексов. Далее будет показано, что аппликативная редукционная стратегия не всегда позволяет получить нормальную форму выражения.

Пример 28. Редукция выражения M = (ly.x)(EE), где E = lx.xx

1. НРС: (ly.x)(EE) = (ly.x)[y <- EE] = x.

2. АРС: (ly.x)(EE) = (ly.x)((lx.xx)(lx.xx)) = (ly.x)((lx.xx)(lx.xx)) = ...

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

Примечание: красным шрифтом выделен b-редекс, редуцируемый следующим шагом.

Пример 29. Редукция выражения M = (lx.xyxx)((lz.z)w)

1. НРС: (lx.xyxx)((lz.z)w) = ((lz.z)w)y((lz.z)w)((lz.z)w) = wy((lz.z)w)((lz.z)w) = wyw((lz.z)w) = wyww.

2. АРС: (lx.xyxx)((lz.z)w) = (lx.xyxx)w = wyww.

В программировании нормальная редукционная стратегия соответствует вызову по имени. Т.е. аргумент выражения не вычисляется до тех пор, пока к нему не возникнет обращения в теле выражения. Аппликативная редукционная стратегия соответствует вызову по значению.

Соответствие между вычислениями функциональных программ и редукцией

Работа интерпретатора описывается несколькими шагами:

  1. В выражении необходимо выделить некоторое обращение к рекурсивной или встроенной функции с полностью означенными аргументами. Если выделенное обращение к встроенной функции существует, то происходит его выполнение и возврат к началу первого шага.
  2. Если выделенное на первом шаге обращение к рекурсивной функции, то вместо него подставляется тело функции с фактическими параметрами (т.к. они уже означены). Далее происходит переход на начало первого шага.
  3. Если больше обращений нет, то происходит остановка.

В принципе, вычисления в функциональной парадигме повторяют шаги редукции, но дополнительно содержат вычисления встроенных функций.

Представление определений функций в виде l-выражений

Показано, что любое определение функции можно представить в виде l-выражения, не содержащего рекурсии. Например:

fact = ln.if n == 0 then 1 else n * fact (n - 1)

То же самое определение можно описать при помощи использования некоторого функционала:

fact = (lf.ln.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)

Теорема (без доказательства):

Любой l-терм имеет неподвижную точку.

l-исчисление позволяет выразить любую функцию через чистое l-выражение без использования встроенных функций. Например:

1.

prefix = lxyz.zxy
head = lp.p(lxy.x)
tail = lp.p(lxy.y)

2. Моделирование условных выражений:

True = lxy.x
False = lxy.y
if B then M else N = BNM, где B in {True, False}.

Наверх | Содержание | Лекции | НАУКА ·]

Сайт управляется системой uCoz