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

Материал из Викиучебника

< Основы функционального программирования

Перейти к: навигация, поиск

Содержание

1 Понятие формальной системы
- 1.1 Построение формальной системы
- 1.2 Стратегия редукции
2 Соответствие между вычислениями функциональных программ и редукцией
- 2.1 Представление определений функций в виде λ-выражений

Основы функционального программирования

Вводная лекция
Структуры данных и базисные операции:
- Первая часть
- Вторая часть

Основы языка Haskell

Конструирование функций
Доказательство свойств функций
Формализация функционального программирования на основе λ-исчисления
Трансформация программ

Категория «Функциональное программирование» →

Объект изучения: множество определений функций.
Предположение: будет считаться, что любая функция может быть определена при помощи некоторого λ-выражения.
Цель исследования: установить по двум определениям функций $\langle f_1 \rangle$ и $\langle f_2 \rangle$ их тождество на всей области определения — $\forall x : f_1(x) = f_2(x)$ . (Здесь использована такая нотация: $f$ — некоторая функция, $\langle f \rangle$ — определения этой функции в терминах λ-исчисления.)

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

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

Можно попытаться выразить семантику встроенных функций при помощи механизма λ-исчисления. Этот процесс можно довести до случая, когда все встроенные функции не содержат непроинтерпретированных операций.
Говорят, что $\langle f_1 \rangle$ и $\langle f_2 \rangle$ семантически равны (этот факт обозначается как $\vDash f_1 = f_2$ ), если $f 1 (x) = f 2 (x)$ при любой интерпретации непроинтерпретированных идентификаторов.

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

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

$P = \langle V,\, \Phi,\, A,\, R \rangle$ ,

где $V$ — алфавит;

$Φ$ — множество правильно построенных формул;

$A$ — аксиомы (при этом $A \subseteq \Phi$ );

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

В рассматриваемой задаче формулы имеют вид $(t 1 = t 2)$ , где $t 1$ и $t 2$ — λ-выражения. Если некоторая формула выводима в формальной системе, то этот факт записывается как $(\vdash t_1 = t_2)$ .

Говорят, что формальная система корректна, если $(\vdash t_1 = t_2) \Rightarrow (\vDash t_1 = t_2)$ .

Говорят, что формальная система полна, если $(\vDash t_1 = t_2) \Rightarrow (\vdash t_1 = t_2)$ .

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

1°. $v \in \mathrm{Id} \Rightarrow v \in \mathrm{Exp}$ .

2°. $v \in \mathrm{Id},\, E \in \mathrm{Exp} \Rightarrow \lambda v.E \in \mathrm{Exp}$

3°. $E, E' \in \mathrm{Exp} \Rightarrow (EE') \in \mathrm{Exp}$

4°. $E \in \mathrm{Exp} \Rightarrow (E) \in \mathrm{Exp}$

5°. Никаких других $Exp$ нет.

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

Говорят, что $v$ свободна в $M \in \mathrm{Exp}$ , если:

1°. $M = v$ .

2°. $M = (M 1 M 2)$ , и $v$ свободна в $M 1$ или в $M 2$ .

3°. $M = λ v'. M'$ , и $v \neq v'$ , и $v$ свободна в $M'$ .

4°. $M = (M')$ , и $v$ свободна в $M'$ .

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

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

1°. $M = λ v'. M'$ , и $v = v'$ .

2°. $M = (M 1 M 2)$ , и $v$ связана в $M 1$ или в $M 2$ (то есть один и тот же идентификатор может быть свободен и связан в $Exp$ ).

3°. $M = (M')$ , и $v$ связана в $M'$ .

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

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

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

$(\lambda x.yx)[y \leftarrow \lambda z.z] = \lambda x.(\lambda z.z)x = \lambda x.x$ — корректная подстановка;

$(\lambda x.yx)[y \leftarrow xx] = \lambda x.(xx)x$ — коллизия имён переменных;

$(\lambda z.yz)[y \leftarrow xx] = \lambda z.(xx)z$ — корректная подстановка.

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

1°. $x[x \leftarrow E'] = E'$ .

2°. $y[x \leftarrow E'] = y$ .

3°. $(\lambda x.E)[x \leftarrow E'] = \lambda x.E$ .

4°. $(\lambda y.E)[x \leftarrow E'] = \lambda y.E[x \leftarrow E']$ , при условии, что $y \not\in FV(E')$ .

5°. $(\lambda y.E)[x \leftarrow E'] = \Big( \lambda z.E[y \leftarrow z] \Big) [x \leftarrow E']$ , при условии, что $y \in FV(E')$ .

6°. $(E_1\,E_2)[x \leftarrow E'] = \Big( E_1[x \leftarrow E']\, E_2[x \leftarrow E'] \Big)$ .

[править] Построение формальной системы

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

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

Аксиомы:

$\vdash \lambda x.E = \lambda y.E[x \leftarrow y]$ ;	(α)
$\vdash (\lambda x.E)E' = E[x \leftarrow E']$ ;	(β)
$\vdash t = t$ , в случае, если $t$ — идентификаторы.	(ρ)

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

$t_1 = t_2 \Rightarrow t_1t_3 = t_2t_3$ ;	(μ)
$t_1 = t_2 \Rightarrow t_3t_1 = t_3t_2$ ;	(ν)
$t_1 = t_2 \Rightarrow t_2 = t_1$ ;	(σ)
$t_1 = t_2,\, t_2 = t_3 \Rightarrow t_1 = t_3$ ;	(τ)
$t_1 = t_2 \Rightarrow \lambda x.t_1 = \lambda x.t_2$ .	(ξ)

Пример 27. Доказать выводимость формулы $(λ x . x y)(λ z .(λ u . z u)) v = (λ v . y v) v$

	$(λ x . x y)(λ z .(λ u . z u)) v = (λ v . y v) v$ ;
(μ):	$(λ x . x y)(λ z .(λ u . z u)) = (λ v . y v)$ ;
(β):	$(λ z .(λ u . z u)) y = (λ v . y v)$ ;
(α):	$λ u . y u = λ v . y v$ — выводима.

Во втором варианте формализации функционального программирования можно воспользоваться не свойством симметричности отношения « $=$ », а свойством несимметричности отношения « $\to$ ».

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

$\vdash \lambda x.M \to \lambda y.M[x \leftarrow y]$	(α′)
$\vdash (\lambda x.M)N \to M[x \leftarrow N]$	(β′)
$\vdash M \to M$	(ρ′)

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

$t_1 \to t_1',\, t_2 \to t_2' \Rightarrow t_1t_2 \to t_1't_2'$

(π)

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

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

Выражение вида $λ x . M$ называется α-редексом.
Выражение вида $(λ x . M) N$ называется β-редексом.
Выражения, не содержащие β-редексов, называются выражениями в нормальной форме.

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

$\vdash E_1 = E_2 \Rightarrow E_1 \to E_2 \lor E_2 \to E_1$ .
$E \to E_1 \land E \to E_2 \Rightarrow \exist F : E_1 \to F \land E_2 \to F$ . (Теорема Чёрча—Россера).
Если $E$ имеет нормальные формы $E 1$ и $E 2$ , то они эквивалентны с точностью до α-конверсии, то есть различаются только обозначением связанных переменных.

[править] Стратегия редукции

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

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

Пример 28. Редукция выражения $M = (λ y . x)(E E)$ , где $E = λ x . x x$

1°. НРС: $\underline{(\lambda y.x)}(EE) = \underline{(\lambda y.x)}[y \leftarrow EE] = x$ .

2°. АРС: $(\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$ .

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

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

Пример 29. Редукция выражения $M = (\lambda x.xyxx) \Big( (\lambda z.z)w \Big)$

1°. НРС: $\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) =$

$= wy \underline{ \Big( (\lambda z.z)w \Big) } \Big( (\lambda z.z)w \Big) = wyw \underline{ \Big( (\lambda z.z)w \Big) } = wyww$ .

2°. АРС: $(\lambda x.xyxx) \underline{ \Big( (\lambda z.z)w \Big)} = \underline{(\lambda 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)

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

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

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

1°.

prefix = λxyz.zxy
head = λp.p(λxy.x)
tail = λp.p(λxy.y)

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

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

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

Материал из Викиучебника

Содержание

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

[править] Построение формальной системы

[править] Стратегия редукции

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

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

Просмотры

Личные инструменты

Навигация

участие

Поиск

Инструменты

Печать/Экспорт