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

Формальная задача: пусть имеется набор функций $f=⟨f_1,\dots ,f_n⟩$, определённых на областях $D=⟨D_1,\dots ,D_n⟩$. Требуется доказать, что для любого набора значений $d$ имеет место некоторое свойство, то есть:

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

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

$\mathrm{\forall }d\in D:f(d)⩾0$

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

$\mathrm{\forall }d\in D:f(d)=f_1(d)$

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

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

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

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

$\mathrm{\forall }{d}_1,d_2\in D:(d_1⩾d_2)\vee (d_1⩽d_2)$.

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

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

1. $P(f(\varnothing ))$ — базис индукции;
2. $\mathrm{\forall }{d}_1,d_2\in D,d_1⩽d_2:P(f(d_1))$ — шаг индукции.

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

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

Из прошлой лекции известно, что индуктивный класс определяется через ввод базиса класса (это либо набор каких либо констант $d_i=0,n\in D$, либо набор первичных типов $A_i=0,n:d\in A_i\Rightarrow d\in D$. Также индуктивный класс определяется при помощи шага индукции — заданы конструкторы $g_1,\dots ,g_m$, определённые над $A_i$ и $D$, и справедливо, что:

$(a_i\in A_i)\wedge (x_j\in D)\Rightarrow g_k(a_i,x_j)\in D,k=\overline{1,m}$.

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

1. $P(f(d))$ необходимо доказать для базиса класса;
2. Шаг индукции: $P(f(d))=P\left(f\right(g_i(d)\left)\right)$.

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

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

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

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

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

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

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

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

Пример 24. Доказать ассоциативность функции $\mathrm{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$ ассоциативность функции $\mathrm{append}$ доказана. Необходимо доказать для $(a:L_1)$, $L_2$ и $L_3$:

$((a:L_1)*L_2)*L_3=(a:(L_1*L_2))*L_3=a:((L_1*L_2)*L_3)$.

$(a:L_1)*(L_2*L_3)=a:(L_1*(L_2*L_3))$.

Как видно, последние два выведенных выражения равны, так как для списков $L_1$, $L_2$ и $L_3$ ассоциативность полагается доказанной.

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

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

$\mathrm{reverse}[]=[]$

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

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

${\mathrm{reverse}}^{\prime }L=\mathrm{rev}L[]$

$\mathrm{rev}[]L=L$

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

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

$\mathrm{\forall }L\in \mathrm{List}(A):\mathrm{reverse}L={\mathrm{reverse}}^{\prime }L$.

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

$\mathrm{reverse}[]=[]$.

${\mathrm{reverse}}^{\prime }[]=\mathrm{rev}[][]=[]$.

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

$\mathrm{reverse}(H:L)=(\mathrm{reverse}L)*[H]=({\mathrm{reverse}}^{\prime }L)*[H]$.

${\mathrm{reverse}}^{\prime }(H:L)=\mathrm{rev}(H:L)[]=\mathrm{rev}L(H:[])=\mathrm{rev}L[H]$.

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

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

$({\mathrm{reverse}}^{\prime }[])*[H]=(\mathrm{rev}[][])*[H]=[]*[H]=[H]$.

$\mathrm{rev}[][H]=[H]$.

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

$({\mathrm{reverse}}^{\prime }(A:T))*[H]=(\mathrm{rev}(A:T)[])*[H]=(\mathrm{rev}T(A:[]))*[H]=(\mathrm{rev}T[A])*[H]$.

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

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

Индукционная гипотеза: $({\mathrm{reverse}}^{\prime }{L}_1)*L_2=\mathrm{rev}{L}_1{L}_2$. Эта индукционная гипотеза является обобщением выражения $({\mathrm{reverse}}^{\prime }L)*[H]=\mathrm{rev}L[H]$.

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

$({\mathrm{reverse}}^{\prime }(A:T))*L_2=(\mathrm{rev}(A:T)[])*L_2=(\mathrm{rev}T[A])*L_2=$

$=(({\mathrm{reverse}}^{\prime }T)*[A])*L_2=({\mathrm{reverse}}^{\prime }T)*([A]*L_2)=({\mathrm{reverse}}^{\prime }T)*(A:L_2)$.

$\mathrm{rev}(A:T)L_2=\mathrm{rev}T(A:L_2)=({\mathrm{reverse}}^{\prime }T)*(A:L_2)$.

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

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