Основы функционального программирования/Доказательство свойств функций

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

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

• Основы языка Haskell
  
  • Служебные слова и синтаксис
    
  • Модули и монады
    
  • Ввод-вывод
    
  • Другие статьи и учебники по Haskell →

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

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

Формальная задача: пусть имеется набор функций $f=\langle f_{1},\,\ldots ,\,f_{n}\rangle$, определённых на областях $D=\langle D_{1},\,\ldots ,\,D_{n}\rangle$. Требуется доказать, что для любого набора значений $d$ имеет место некоторое свойство, то есть:

$\forall \,d\in D:P{\Big (}f(d){\Big )}$,

где $P$ — рассматриваемое свойство. Например:

$\forall \,d\in D:f(d)\geqslant 0$

$\forall \,d\in D:f(d)=f{\Big (}f(d){\Big )}$

$\forall \,d\in D:f(d)=f_{1}(d)$

Вводится принципиальное ограничение на рассматриваемые свойства — свойства только тотальные, то есть справедливые для всей области $D$.

Далее рассматриваются некоторые виды областей определения $D$.

1. $D$ — линейно упорядоченное множество.

Полуформально линейно упорядоченное множество можно определить как такое множество, для каждых элементов которого можно сказать, какой меньше (или больше), либо они равны, то есть:

$\forall \,d_{1},d_{2}\in D:(d_{1}\geqslant d_{2})\lor (d_{1}\leqslant d_{2})$.

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

Для доказательства свойств функций на линейно упорядоченных множествах достаточно провести индукцию по данным. То есть достаточно доказать два пункта:

1. $P{\Big (}f(\varnothing ){\Big )}$ — базис индукции;
2. $\forall \,d_{1},d_{2}\in D,\ d_{1}\leqslant d_{2}:P{\Big (}f(d_{1}){\Big )}$ — шаг индукции.

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

2. $D$ — определяется как индуктивный класс

Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант $d_{i}=0,n\in D$, либо набор первичных типов $A_{i}=0,n:d\in A_{i}\Rightarrow d\in D$. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы $g_{1},\ldots ,g_{m}$, определённые над $A_{i}$ и $D$, и справедливо, что:

$(a_{i}\in A_{i})\land (x_{j}\in D)\Rightarrow g_{k}(a_{i},x_{j})\in D,\ k={\overline {1,m}}$.

В этом случае доказательство свойств функций также резонно проводить в виде индукции по даным. Метод индукции по даным в этом случае также очень прост:

1. $P{\Big (}f(d){\Big )}$ необходимо доказать для базиса класса;
2. Шаг индукции: $P{\Big (}f(d){\Big )}=P{\bigg (}f{\Big (}g_{i}(d){\Big )}{\bigg )}$.

Например, для доказательства свойств функций для списков (тип $\operatorname {List} (A)$), достаточно доказать рассматриваемое свойство для двух следующих случаев:

1. $P{\Big (}f([\,]){\Big )}$.
2. $\forall \,a\in D,\,\forall \,L\in \operatorname {List} (A):P{\Big (}f(L){\Big )}\Rightarrow P{\Big (}f(a:L){\Big )}$.

Доказательство свойств функций над $S$-выражениями (тип $\operatorname {S-expr} (A)$) можно проводить на основе следующей индукции:

1. $\forall \,a\in A:P{\Big (}f(a){\Big )}$.
2. $\forall \,x,y\in \operatorname {S-expr} (A):P{\Big (}f(x){\Big )}\land P{\Big (}f(y){\Big )}\Rightarrow P{\Big (}f(x:y){\Big )}$.

Пример 23. Доказать, что $\forall \,L\in \operatorname {List} (A):L*[\,]=L$.

Для доказательства этого свойства можно использовать только определение типа $\operatorname {List} (A)$ и самой функции $\operatorname {append}$ (в инфиксной записи используется символ $*$).

1. $L=[\,]:[\,]*[\,]=[\,]=L$. Базис индукции доказан.
2. $\forall \,L\in \operatorname {List} (A):L*[\,]=L$. Теперь пусть применяется конструктор: $a:L$. Необходимо доказать, что $(a:L)*[\,]=a:L$. Это делается при помощи применения второго клоза определения функции $\operatorname {append}$:

$(a:L)*[\,]=a:(L*[\,])=a:(L)=a:L$.

Пример 24. Доказать ассоциативность функции $\operatorname {append}$.

То есть необходимо доказать, что для любых трёх списков $L_{1}$, $L_{2}$ и $L_{3}$ имеет место равенство $(L_{1}*L_{2})*L_{3}=L_{1}*(L_{2}*L_{3})$. При доказательстве индукция будет проводиться по первому операнду, то есть списку $L_{1}$:

1. $L_{1}=[\,]$:

$([\,]*L_{2})*L_{3}=(L_{2})*L_{3}=L_{2}*L_{3}$.

$[\,]*(L_{2}*L_{3})=(L_{2}*L_{3})=L_{2}*L_{3}$.

1. Пусть для списков $L_{1}$, $L_{2}$ и $L_{3}$ ассоциативность функции $\operatorname {append}$ доказана. Необходимо доказать для $(a:L_{1})$, $L_{2}$ и $L_{3}$:

${\Big (}(a:L_{1})*L_{2}{\Big )}*L_{3}={\Big (}a:(L_{1}*L_{2}){\Big )}*L_{3}=a:{\Big (}(L_{1}*L_{2})*L_{3}{\Big )}$.

$(a:L_{1})*(L_{2}*L_{3})=a:{\Big (}L_{1}*(L_{2}*L_{3}){\Big )}$.

Как видно, последние два выведенных выражения равны, так как для списков $L_{1}$, $L_{2}$ и $L_{3}$ ассоциативность полагается доказанной.

Пример 25. Доказательство тождества двух определений функции $\operatorname {reverse}$.

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

$\operatorname {reverse} \ [\,]=[\,]$

$\operatorname {reverse} \ (H:T)=(\operatorname {reverse} \ T)*[H]$

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

$\operatorname {reverse} '\;L=\operatorname {rev} \ L[\,]$

$\operatorname {rev} \ [\,]\ L=L$

$\operatorname {rev} \ (H:T)\ L=\operatorname {rev} \ T\ (H:L)$

Видно, что первое определение функции обращения списков — это обычное рекурсивное определение. Второе же определение использует аккумулятор. Требуется доказать, что:

$\forall \,L\in \operatorname {List} (A):\operatorname {reverse} \ L=\operatorname {reverse} '\;L$.

1. Базис — $L=[\,]$:

$\operatorname {reverse} \ [\,]=[\,]$.

$\operatorname {reverse} '\;[\,]=\operatorname {rev} \ [\,]\ [\,]=[\,]$.

2. Шаг — пусть для списка $L$ тождество функций $\operatorname {reverse}$ и $\operatorname {reverse} '$ доказано. Необходимо доказать его для списка $(H:L)$.

$\operatorname {reverse} \ (H:L)=(\operatorname {reverse} \ L)*[H]=(\operatorname {reverse} '\;L)*[H]$.

$\operatorname {reverse} '\;(H:L)=\operatorname {rev} \ (H:L)\ [\,]=\operatorname {rev} \ L\ (H:[\,])=\operatorname {rev} \ L\ [H]$.

Теперь необходимо доказать равенство двух последних выведенных выражений для любых списков над типом $A$. Это также делается по индукции:

2.1. Базис — $L=[\,]$:

$(\operatorname {reverse} '\;[\,])*[H]=(\operatorname {rev} \ [\,]\;[\,])*[H]=[\,]*[H]=[H]$.

$\operatorname {rev} \ [\,]\ [H]=[H]$.

2.2. Шаг — $L=(A:T)$:

${\Big (}\operatorname {reverse} '\;(A:T){\Big )}*[H]={\Big (}\operatorname {rev} \ (A:T)\ [\,]{\Big )}*[H]={\Big (}\operatorname {rev} \ T\ (A:[\,]){\Big )}*[H]=(\operatorname {rev} \ T\ [A])*[H]$.

$\operatorname {rev} \ (A:T)\ [H]=\operatorname {rev} \ L\ (A:H)$.

Здесь произошло выпадение в дурную бесконечность. Если дальше пытаться проводить доказательство по индукции для новых выведенных выражений, то эти самые выражения будут всё усложняться и усложняться. Но это не причина для того, чтобы отчаиваться, ибо доказательство всё равно можно провести. Надо просто придумать некую «индукционную гипотезу», как это было сделано в предыдущем примере.

Индукционная гипотеза: $(\operatorname {reverse} '\;L_{1})*L_{2}=\operatorname {rev} \ L_{1}\ L_{2}$. Эта индукционная гипотеза является обобщением выражения $(\operatorname {reverse} '\;L)*[H]=\operatorname {rev} \ L\ [H]$.

Базис индукции для этой гипотезы очевиден. Шаг индукции в применении к выражению в пункте 2.2 выглядит следующим образом:

${\Big (}\operatorname {reverse} '\;(A:T){\Big )}*L_{2}=(\operatorname {rev} \ (A:T)\ [\,])*L_{2}=(\operatorname {rev} \ T\ [A])*L_{2}=$

$={\Big (}(\operatorname {reverse} '\;T)*[A]{\Big )}*L_{2}=(\operatorname {reverse} '\;T)*([A]*L_{2})=(\operatorname {reverse} '\;T)*(A:L_{2})$.

$\operatorname {rev} \ (A:T)\ L_{2}=\operatorname {rev} \ T\ (A:L_{2})=(\operatorname {reverse} '\;T)*(A:L_{2})$.

Что и требовалось доказать.

Общий вывод: в общем случае для доказательства свойств функций методом индукции может потребоваться применение некоторых эвристических шагов, а именно введение индукционных гипотез. Эвристический шаг — это формулирование утверждения, которое ниоткуда не следует. Таким образом, доказательство свойств функций есть своего рода творчество.