Декларативное программирование

[ Содержание | 1 | 2 | 3 | 4 | 5 | 5.1 | 5.2 | 5.3 | 5.4 | 5.5 | 5.6 | 5.7 | 5.8 | 5.9 | 6 | 6.1 | 6.2 | 6.3 | 6.4 | 6.5 | 7 | 7.1 | Литература ]

© 2003 И.А. Дехтяренко

5.9 Математические свойства функциональных программ.

Математические функции имеют приятное свойство независимости от контекста вычислений. Значение выражения 2+2 - всегда 4, независимо от того считаем мы 3*(2+2) или (2 + 2)². Если заменить какую-нибудь часть выражения эквивалентным подвыражением, это не повлияет конечный результат. Функциональные программы соответствуют функциям в математическом смысле. Они обладают тем же свойством: вызов функции с теми же самыми параметрами всегда выдаст то же самое значение. (Это свойство часто называют "прозрачностью ссылок", или "безразличием к состоянию"). Поэтому, они лучше поддаются формальным манипуляциям, чем императивные программы.

Но для чего могут понадобиться формальные манипуляции? С их помощью мы можем доказывать правильность наших программ - их соответствие формальным спецификациям. Мы можем преобразовывать программы в более эффективные программы. Два выражения, равенство которых доказано, могут иметь различные вычислительные характеристики. В таком случае медленное (или требовательное к памяти) определение может быть заменено другим, более быстрым (или требующим меньше памяти). Кроме того, изучение математических свойств помогает нам лучше понимать программы, благодаря чему мы можем находить им новые, подчас неожиданные, применения.

Возможность и необходимость доказательства правильности программ вызывает множество споров. Как известно, подчас бывает очень трудно, написать программу, которая является правильной, то есть делает точно то, что от неё требуется. Многие программы содержат ошибки. Последствия этих ошибок могут быть различными. Некоторые ошибки безопасны, некоторые просто раздражающие, некоторые смертельны. Например, программы автопилота самолета, или системы управления ядерным реактором критичны к требованиям надежности. Ошибка в них может привести к катастрофическим последствиям. С другой стороны, ошибка в компьютерной игре ничем особо неприятным не грозит. К ошибкам в экономических программах традиционно относятся довольно терпимо, хотя они и могут привести к значительным убыткам.

Как удостовериться, что программа правильна? Очень распространенный метод - просто проверить её в различных ситуациях. Мы испытываем программу на тестовых данных, предназначенных, для того чтобы вызвать выполнение различных частей программы и показать возможные ошибки.¹

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

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

Имеются, однако, и возражения против такого подхода. Некоторые из них чисто экономические и организационные.

• Применение формальных методов требует определенного уровня квалификации, чего многие менеджеры всячески стремятся избежать.
• В процессе доказательства приходится выполнять большое количество выкладок. Как правило, доказательство правильности достаточно сложной программы превосходит по объему любую математическую работу. Это должно привести к увеличению сроков разработки что, конечно, не добавляет привлекательности, данной методике. С другой стороны, учитывая типичные затраты на тестирование и отладку, не все так очевидно. Кроме того, выкладки, применяемые при доказательствах, достаточно просты и хорошо поддаются автоматизации.

Существуют и более существенные ограничения. Давайте рассмотрим идеализированную схему решения задачи. Исходя из фактических требований, часто выраженных неформально, составляется формальная спецификация. Затем создаётся программа, удовлетворяющая этой спецификации. Эта программа - абстрактная математическая модель реальной программы, выполняющейся на компьютере.

Реальный мир		Абстрактный мир
Фактические требования		Формальная спецификация
Реальная система		Формальная система

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

1. Нет гарантии, что выполнение программы на компьютере точно соответствует абстрактной математической модели. Несоответствия, могут быть вызваны ошибками в компиляторах и операционных системах или дефектами аппаратуры. Кроме того, формальные модели программ часто содержат упрощения и предположения, естественные в большинстве ситуаций, но не всегда строго выполняющиеся. Например, машинные арифметические операции не вполне соответствуют их математическим прообразам.
2. Возможно, что формальная спецификация недостаточно точно отражает то, что требуется на самом деле. Часто бывает трудно, получить математически точную формулировку требований. Многие серьезные проблемы в компьютерных системах были вызваны не ошибками кодирования в обычном смысле, а ошибочным представлением о том, что фактически требуется. Стоит отметить, что формализация требований к программе часто ценна сама по себе, безотносительно к применению формальных методов.

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

Мы можем интерпретировать набор уравнений, составляющих программу как аксиомы некоторых математических объектов, а процесс вычислений как вывод некоторого утверждения. Но, исходя из тех же аксиом, можно вывести и другие утверждения об этих объектах. Доказательства утверждений, в общем, подобны обычным математическим доказательствам и могут принимать различную форму. Однако в математике можно обнаружить часто повторяющиеся шаблоны доказательств. Например, линейные цепочки тождественных преобразований уравнений, рассуждения в терминах "епсилон - дельта", характерные для анализа, или метод математической индукции. Подобным образом, возникают шаблоны доказательств утверждений о программах.

Очевидно, в процессе доказательства придется использовать не только уравнения, входящие в программу, но и некоторые свойства используемых в ней функций, в том числе и встроенных. Некоторые из этих свойств аксиоматические (то есть они истинны потому, что мы так определили соответствующие функции), другие могут быть легко получены из аксиом, или интуитивно очевидны. В более сложных случаях свойства функций могут быть не так очевидны, и нам потребуются формальные средства для их доказательства. Мы будем доказывать главным образом очевидные свойства, просто чтобы продемонстрировать технику доказательств. Кроме того, полезно бывает убедиться, что интуиция нас не подводит.

Индуктивные доказательства.

Простейшие доказательства производятся прямыми подстановками, точно так же как в школе доказывались законы типа (x+y)(x-y) = x²-y². Но часто приходится прибегать к более сложным рассуждениям.

Мы определяли факториал числа n как произведение всех чисел от 1 до n.

n! = 1*2*3*...*n.

Это определение кажется вполне удовлетворительным, пока мы не попытаемся записать его формально. В самом деле, что означают эти три точки. Интуитивно вроде бы все ясно, но как выразить это математически? Если мы попытаемся дать совершенно строгое определение, не прибегая к абстракциям более высокого уровня (которые сами нуждаются в определениях) мы, так или иначе, придем к двум очевидным правилам, на которых и основывалась наша процедура вычисления факториала.

1! = 1,
n! = n*(n-1)!, при n>1.

Мы можем объявить эти правила определением факториала. Однако действительно ли они однозначно определяют функцию? Это нетрудно доказать.

Пусть две функции f и g удовлетворяют следующим условиям

f(1) = 1
f(n) = n* f (n-1), при n>1.

g(1) = 1
g(n) = n* g(n-1), при n>1.

Тогда эти функции совпадают для всех натуральных аргументов.
Действительно,

f(1) = 1 = g(1) .

Предположим теперь, что f(n) = g(n). Тогда

f(n+1) = n* f (n)= n* g(n) = g(n+1).

Мы применили известный метод математической индукции. Для того чтобы доказать, что некоторое утверждение P(n) истинно для всех натуральных чисел мы выполняем два шага:

1. доказываем истинность утверждения для базового случая, то есть P(1);
2. доказываем, что, если утверждения верно для некоторого числа n, то оно должно выполняться и для n+1, то есть P(n) => P(n+1).

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

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

Для того чтобы доказать, что некоторое утверждение P истинно для всех списков, мы

1. доказываем истинность утверждения для базового случая, то есть P([]);
2. доказываем, что, если утверждение верно для произвольного списка xs, то оно должно выполняться и для списка [x|xs], где x - произвольный объект, то есть P(xs) => P([x|xs]).

Эта схема допускает различные модификации. Например, мы можем доказать что некоторое утверждение P истинно для всех списков, элементы которых удовлетворяют условию R. Для этого мы

1. доказываем  P([]);
2. доказываем, что, если P верно для списка xs, и x удовлетворяет условию R, то P выполняется и для списка [x|xs], то есть P(xs), R(x)=> P([x|xs]).

С другой стороны, возможно, что данное утверждение выполняется только для непустых списков. Тогда мы базовый случай принимает вид P([x]). Вообще, шаги, применяемые в индуктивных доказательствах, тесно связаны с рекурсивными определениями функций. Определяя рекурсивные функции, мы сначала описываем базовый случай, а затем - случай n в терминах случая n-1 (для функций на целых числах), или случай [x|xs] в терминах случая xs (для функций, которые используют списки). Таким образом, рекурсивное определение функции предлагает схему индуктивного доказательства.

Примеры индуктивных доказательств.

Функция соединения списков определяется двумя правилами:

append([], xs) = xs
append([x|xs], ys) = [x| append(xs,ys)]

или, используя инфиксную запись

[] ++ xs = xs
[x|xs] ++ ys = [x| xs ++ ys].

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

Одно из таких следствий:

[x] ++ xs = [x|xs].

Его доказательство элементарно.

[x] ++ xs = [x|[]] ++ xs = [x | [] ++ xs] = [x|xs].

Первое правило в определении операции соединения списков утверждает, что пустой список - левый  нейтральный элемент этой операции. Докажем, что он является правым нейтральным элементом, то есть, что xs ++ [] = xs.

1. Базис:
   [] ++ [] = [].
2. Шаг индукции:
   Пусть xs ++ [] = xs.
   Тогда [x|xs] ++ [] = [x| xs ++ []] = [x| xs].
   Q.E.D.

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

Докажем что операция ++ ассоциативна. То есть, для любых трех списков xs, ys и zs:

xs ++ (ys ++ zs) = (xs ++ ys) ++zs.

Доказательство выполним структурной индукцией по xs.

1. [] ++ (ys++zs) = ys ++ zs = ([]++ ys)++ zs
2. Предположим, что для любых ys и zs:
   xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
   Отсюда:
   [x | xs] ++ (ys ++ zs ) =
   [x | xs ++ (ys ++ zs) ] =
   [x | (xs ++ ys) ++ zs] =
   [x | (xs ++ ys)] ++ xs) =
   ([x | xs] ++ ys) ++ zs.
   Q.E.D.²

Функция length, вычисляющая длину списка определяется двумя правилами

length([]) = 0;
length([x|xs]) = 1 + length(xs).

Докажем очевидное утверждение

length(xs ++ ys) = length(xs) + length(ys)

Доказательство все той же индукцией по xs. Но теперь, доказывая равенство двух выражений, мы не будем пытаться привести одно к другому, а приведем каждое из них  к третьему.

1. length([] ++ ys) = length(ys) .
   length([]) + length(ys) = 0 + length(ys) = length(ys).
2. Предположим, что для любых xs и ys:
   length(xs ++ ys) = length(xs) + length(ys)
   Тогда:
   length(([x|xs] ++ ys)) = length([x|xs ++ys]) = 1 + length(xs ++ys)) .
   length([x|xs]) + length(ys) = 1 + length(xs) + length(ys) .
   Q.E.D.
   

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

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

reverse([]) = []
reverse([x|xs]) = reverse(xs) ++ [x]

Исходя из этого определения докажем что reverse(reverse(xs)) = xs.

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

Лемма 1

reverse([x]) =  [x]

Доказательство:

reverse([x]) = reverse([]) ++ [x] = [] ++ [x] = [x].

Лемма 2

Для любых списков xs и ys
reverse(xs ++ ys) = reverse(ys)++ reverse(xs)

Доказательство (структурная индукция по xs):

1. reverse([]++ys)= reverse(ys) = reverse(ys)++[] = reverse(ys)++reverse([])
2. Пусть reverse(xs++ys) = reverse(ys)++ reverse(xs).
   Тогда
   reverse([x|xs] ++ ys) = reverse([x|xs++ys] ) =
   reverse(xs ++ ys) ++ [x] = reverse(ys)++ reverse(xs) ++[x]
   
   reverse(ys) ++ reverse([x|xs]) = reverse(ys) ++ reverse(xs) ++ [x]
   Q.E.D.

Теперь можно переходить к доказательству утверждения.

Теорема

Для любого списка xs: reverse(reverse(xs)) = xs.

Доказательство (структурная индукция по xs):

1. reverse(reverse([])) = reverse([])  = []
2. Пусть reverse(reverse(xs)) = xs.
   Тогда
   reverse(reverse([x|xs]) =
   reverse(reverse(xs)++[x]) =
   reverse([x]) ++ reverse(reverse(xs)) =
   [x] ++ reverse(reverse(xs)) =
   [x] ++ xs = [x|xs]
   Q.E.D.

Наивное обращение называется так потому, что оно очень просто и очень неэффективно. Для обращения списка из N элементов потребуется O(N²) операций - многовато для такой простой задачи. Следующая процедура, использующая аккумулятор, делает то же за время O(N).

fast_reverse(xs) = rev(xs, [])
rev([],ys) = ys
rev([x|xs], ys) = rev(xs, [x|ys]).

Можем ли мы убедиться, что эффективная версия обращения эквивалентна оригинальной? Прежде всего заметим, что процедура  fast_reverse просто обеспечивает интерфейс к rev, и нам надо доказать что   rev(xs,[]) = reverse(xs). Попытаемся сделать это, используя структурную индукцию.

1. rev([], []) = [] = reverse([]).
2. Пусть rev(xs,[]) = reverse(xs).
   Тогда
   rev([x|xs], []) = rev(xs, [x])
   reverse([x|xs]) = reverse(xs) ++ [x] = rev(xs,[]) ++ [x].

Теперь надо доказать равенство выражений rev(xs, [x]) и rev(xs,[]) ++ [x].

1. rev([], []) ++ [x] = [] ++ [x] = [x].
   rev([], [x]) = [x].
2. Пусть rev(xs, [x]) = rev(xs,[]) ++ [x].
   Тогда
   rev([x|xs],[]) ++ [y] = rev(xs,[x]) ++ [y].
   rev([x|xs],[y]) = rev(xs,[x,y]).

Новая цель: rev(xs,[y]) ++ [z] = rev(xs,[y,z]).

Попытавшись доказать её, придём к цели rev(xs, [y1,y2]) ++ [z] = rev(xs, [y1,y2,z]), затем к цели rev(xs,[y1,y2,y3]) ++ [z] = rev(xs, [y1,y2,y3,z]) и т. д. Как видно, выражения  все усложняются и усложняются. Попытка использовать индукцию часто оказывается неудачной, из-за того что гипотеза слишком слаба, чтобы провести доказательство. Именно так обстоит дело в данном случае. Мы можем попытаться обобщить наше предположение и доказать более сильное утверждение. Выражения, которые мы получали, подсказывают нам каким образом сделать обобщение. Например, rev(xs,ys) ++ [z] = rev(xs,ys++[z]) или, еще более общо, rev(xs,ys) ++ zs = rev(xs,ys++zs).

Эти гипотезы доказываются без труда. Но мы немного вернемся назад и изменим наше начальное утверждение. Действительно, применив к нему наше последнее предположение, получим новое утверждение, а именно: reverse(xs) ++ ys = rev(xs,ys). Это общее утверждение легко доказывается по индукции, а утверждение rev(xs,[]) = reverse(xs), которое требуется доказать, будет для него частным случаем.

Теорема

Для любых списков xs и ys: reverse(xs) ++ ys = rev(xs,ys).

Доказательство

1. reverse([]) ++ ys = [] ++ ys = ys = rev([], ys)
2. Пусть reverse(xs) ++ ys = rev(xs,ys).
   Тогда
   reverse([x|xs]) ++ ys = reverse(xs) ++ [x] ++ ys =
   reverse(xs) ++ [x|ys] = rev ([x|xs],ys)
   Q.E.D.

Наше обобщение, радикальным образом упрощающее доказательство, выглядит как deus ex mashina, но это потому, что мы пытаемся доказать утверждение об уже полученной функции. В действительности, оно вполне естественно возникает в процессе её написания. Опытный программист сразу напишет процедуру с накопителем, для менее опытного потребуется некоторое "озарение". Но можно пререйти от одной формы к другой более-менее систематически.

Вернемся к определению reverse.

reverse([]) = []
reverse([x|xs]) = reverse(xs) ++ [x] 

Правая часть второго уравнения содержит композицию reverse и append. Определим ее как функцию revapp.

revapp(xs,ys) = reverse(xs) ++ ys.

Легко выразить reverse через полученную функцию.

reverse(xs) = reverse(xs ++ []) = revapp(xs,[]).

Казалось бы, мы достигли немногого, поскольку определение revapp само ссылается на  reverse. Но мы можем  избавиться от этого, "развертывая" reverse, то есть заменяя вызов функции ее телом. Сначала сделаем это для пустого списка.

revapp([],ys) = reverse([]) ++ ys = ys.

Затем для непустого.

revapp([x|xs],ys) = 
reverse([x|xs]) ++ ys = 
reverse(xs) ++ [x] ++ ys = 
reverse(xs) ++ [x|ys] 

Но последнее выражение может быть "свернуто" в revapp(xs,[x|ys]). Итак, мы получили определение

reverse(xs ) =  revapp(xs,[]).

revapp([],ys) = ys.
revapp([x|xs],ys) = revapp(xs,[x|ys]).

А это как раз и есть то самое быстрое обращение.

Упражнение.

Исходя из определения sum
sum([]) = 0
sum([x|xs]) = x + sum(xs)
Докажите, что
sum (xs ++ ys) = sum (xs) + sum (ys)

Упражнение.

Обычно функция map определяется следующим образом
map(F, []) = []
map(F, [x|xs]) = [F(x) | map(F,xs)]
Докажите, что для любой функции f
map(f, xs ++ ys) = map(f, xs) ++ map(f, ys)

Упражнение.

Докажите, что если функция fg - композиция функций f и g, то есть fg(x)= f(g(x))
то map(fg,xs) = map(f , map(g, xs)).

Упражнение.

Функция concat (или append/1 в Erlang) соединяет все подсписки данного списка.

concat ([]) = []
concat ([x|xs]) = x ++ concat (xs).

Докажите следующие утверждения
length(concat(xs)) = sum(map(length, xs))
sum(concat(xs)) = sum(map(sum, xs))

Упражнение.

Докажите, что
map(f, concat(xs)) = concat(map(f^*,xs)), где
f^*(xs)= map(f,xs)

Упражнение. (Структурная индукция в общем случае).

Пусть задан набор конструкторов c₁, ..., c_n (некоторые из них могут быть константами). Множество D определено как множество объектов, полученных в результате применения конструкторов. Сформулируйте индуктивный метод доказательства утверждений о функциях, определенных на  D.

Упражнение.

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

 

Неформальные рассуждения.

Формальные индуктивные доказательства довольно громоздки и трудоемки. Поэтому часто прибегают к полуформальным доказательствам, используя запись списков в виде [x₁,x₂,...x_n].

Например, из определения reverse получаем.

reverse([x₁,x₂,...x_n]) = reverse([x₂,...x_n]) ++ [x₁]= reverse([x₃,...xn]) ++ [x₂,x₁]=...= [x_n,...x₂,x₁].

То есть

reverse([x₁,...x_n]) = [x_n,...x₁]

Можно сказать, что это и есть "настоящее" определение функции обращения списка, поскольку оно ясно описывает, какой смысл мы вкладываем в это понятие. Доказательство ???идемпотентностиЮЮЮ становится тривиальным.

reverse(reverse([x₁,...x_n])) = reverse([x_n,...x₁]) = [x₁,...x_n].

Рассмотрим определение суммы списка.

sum([x₁,x₂,...x_n]) = x₁+sum([x₂,...x_n]) = ... = x₁+x₂+...x_n + sum([]) = x₁+x₂+...x_n + 0 = x₁+x₂+...x_n

С таким определением совсем нетрудно показать, что sum(xs ++ ys) = sum(xs) + sum(ys)

sum([x₁,...x_n] ++ [y₁,...y_m]) =
sum([x₁,...x_n, y₁,...y_m]) =
x₁+...x_n+ y₁+...y_m=
(x₁+...x_n) + (y₁+...y_m)=
sum([x₁,...x_n]) + sum([y₁,...y_m])

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

Полиморфные функции.⁴

Из определения map непосредственно следует:

1. map(f,hd(xs)) = hd(map(f,xs))
2. map(f,tl(xs)) = tl(map(f,xs)),

или, используя обозначение f^*(xs)= map(f,xs),

1. f(hd(xs)) = hd(f^*(xs))
2. f^*(tl(xs)) = tl(f^*(xs)).

Эти утверждения выполняются для любой функции f и их можно рассматривать как свойства функций hd и tl. Интуитивно ясно, что свойством (1) обладает функция last и вообще любая функция, выбирающая некоторый элемент списка способом,  не зависящим от свойств элементов и что свойством (2) обладает функция reverse и, вообще любая функция, преобразующая один список в другой и не использующая никаких свойств элементов списка. Формализация условия, что функция не "использует никаких свойств элементов" требует привлечения довольно сложного математического аппарата. В теории типов такие функции называются "полиморфными", а в теории категорий им соответствует понятие "естественного преобразования". Пока же можно рассмотреть эти функции неформально.

Пусть функция s выбирает из списка xs = [x₁,...x_n] элемент x_k некоторым способом, не зависящим от свойств элементов списка. Это означает, из списка f^*(xs) = [f(x₁),...f(x_n)], полученного применением функции f к каждому элементу, будет выбран элемент f(x_k). Другими словами

s(f^*(xs)) = f(s(xs)).

Аналогичные рассуждения для функции r преобразующей список приводят к уравнению

r(f^*(xs)) = f^*(r(xs)).

Далее, если функция h преобразует список списков в список элементов этих списков и, опять же, не зависит от свойств этих элементов, то

h(f^**(xs)) = f^*(h(xs))

Типичный пример - функция concat

concat(f^**(xs)) = f^*(concat(xs))

К этому же классу относятся комбинаторные функции, возвращающие списки списков. Для них выполняется равенство.

c(f^*(xs)) = f^**(с(xs))

Можно обобщить это наблюдение. Если (полиморфная) функция g получает список вложенности n и возвращает список вложенности m, то

g(f^*n(xs)) = f^*m(g(xs))

Здесь f^*n означает "n-кратное map" и определяется как

f^*0(x) = f(x)
f^*n+1(x) = map(f^*n, x).

Функции высшего порядка как средство доказательства.

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

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

Так, из определения

twice([]) = []
twice([x|xs]) = [2*x | twice(xs)]

мы тут же заключаем

twice(xs ++ ys) = twice(xs) ++ twice(ys).

Это заключение основано на уже доказанном утверждении о функции map и на том факте, что

twice(xs) = map(f, xs), где
f(x) = 2*x

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

foldr(f, a, []) = a;
foldr(f, a, [x | xs]) = f(x, foldr(f, a, xs)).

Смысл этого оператора хорошо виден из следующего примера.

foldr(+, a, [x1,x2,...xn]) = 
foldr(+, a, [x1|[x2|...[xn|[]]...] ) = 
            (x1+(x2+...(xn+ a)...) )

Здесь список выписан в явном (развернутом) виде, чтобы показать, что каждый конструктор "|" заменяется применяемой операцией("+"), а конструктор "[]", которым заканчивается каждый список - значением a.

В программировании оператор свертки появился под названиями "приведение" или "вставка" и определялся для непустых списков.

foldr(f, [x]) = x
foldr(f, [x | xs]) = f(x, foldr(f, xs)).

Название "вставка" связано с тем, оператор как бы вставляет знак операции между элементами списка.

foldr(+, [x₁,x₂,...x_n] ) = x₁+x₂+...x_n

Нетрудно показать что, если e правый нейтральный элемент бинарной операции f, а xs - непустой список то

foldr(f, xs) = foldr(f, e, xs)

С другой стороны, для любого значения a и любого списка xs.

foldr(f, a, xs) = foldr(f, xs++[a])

Таким образом, оба варианта по сути эквивалентны и выбор одного из них определяется соображениями удобства. Но все же первый более интересен с теоретической точки зрения.

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

sum(xs) = foldr(+,0, xs)
prod(xs) = foldr(*,1, xs)
all(xs) = foldr(and,true, xs)
any(xs) = foldr(or,false, xs)
concat(xs) = foldr(++,[], xs)

Интересно, какие еще функции можно выразить таким образом? Нетрудно видеть что,

если f(x) = foldr(g,a,x)
то
f([]) = foldr(g, a, []) = a
f([x|xs]) = foldr(g, a, [x|xs]) = f(x, foldr(g, a, xs))= g(x,f(xs))

Можно показать и обратное.

Теорема (универсальное свойство свертки)

Если функция f удовлетворяет условиям
f([]) = a
f([x|xs]) = g(x,f(xs))
то она может быть выражена как
f(xs) = foldr(g, a, xs).

Доказательство (структурная индукция по xs):

f([]) = a = foldr(g, a, []).

f([x|xs]) = g(x,f(xs))
foldr(g, a, [x|xs]) = g(x, foldr(g, a, xs)) = g(x,f(xs))

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

Длина списка (length).

length([]) = 0
length([x|xs]) = 1 + length(xs) .

length(xs)= foldr(suc2, 0, xs), где
suc2(_,N) = 1 + N
Функция suc2 игнорирует первый аргумент и добавляет единицу ко второму

Функция идентичности id(x)=x

id([]) = []
id([x|xs]) = [x|xs]

id(x) = foldr(cons,[],x), где
cons(x,xs) = [x|xs] - просто имя для конструктора списка.

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

Обращение списка (reverse)

reverse([]) = []
reverse([x|xs]) = reverse(xs) ++ [x]

reverse(xs)= foldr(snoc,[], xs).

Здесь функция snoc ("cons наоборот") добавляет элемент в конец списка.

snoc(x,xs) = xs ++ [x]

Соединение списков (append)

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

append_ys(xs) = xs ++ ys,

легко видеть, что

append_ys([]) = ys
append_ys([x|xs]) = cons(x,append_y(xs)).

Таким образом

append_ys(x) = foldr(cons,ys,x)

или

xs ++ ys = foldr(cons,ys,x).

Отображение списка (map)

Рассуждая аналогично определим

f*(xs) = map(f, xs).

f*([]) = []
f*([x|xs]) = [f(x) | f*(xs)].

Отсюда

f*(xs) = foldr(fcons_f,[],xs), где
fcons_f(x,xs) = [f(x) | xs]

Фильтрация списка (filter)

Точно так же определим

p^?(xs)= filter(p, xs)

p^?([]) = [];
p^?([x | xs]) = [x | p^?(xs)] , если p(x)
p^?([x | xs]) = p^?(xs)

Таким образом

p^?(xs) = foldr(cconsp,[],xs), где
ccons_p(x,xs) = [x | xs], если p(x)
ccons_p(x,xs) = xs.

Как видно, операция свертки обладает большой общностью и может использоваться, чтобы выразить множество функций. Но эта общность имеет обратную сторону. Свойства, которыми она обладает, оказываются слишком слабыми. Например, нетрудно убедится, что

foldr(f, a, xs++ys) = foldr(f, foldr(f,a,ys), xs).

Применив это свойство к определению sum(xs) = foldr(+, 0, xs), получим

sum(xs++ys) = foldr(+, sum(ys), xs)

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

Если операция f ассоциативна а e - её нейтральный элемент ( f(a,f(b,c) = f(f(a,b)c) и  f(x,e)=x ) то

foldr(f,e, xs ++ ys) = f( foldr(f,e,xs),  foldr(f,e,ys))

Отсюда легко получаются такие утверждения, как

sum(xs ++ ys) = sum(xs) + sum(ys)
prod(xs ++ ys) =  prod(xs) * prod(ys)
all(xs ++ ys) = all(xs) and all(ys)

Это свойство допускает простое обобщение. Пусть операции f и g связаны соотношением 

f(x, g(y,z)) = g(f(x,y),z)  

(при g = f это в точности означает ассоциативность f) и пусть g(e,x) = x. Тогда

foldr(f,e, xs++ys) = g(foldr(f,e,xs),  foldr(f,e,ys))

Положив g = + , f = suc2, e = 0, получим (suc2(x,y+z) = suc2(x,y)+z). Отсюда

length(xs ++ ys) = length(xs) + length(ys)

Пусть теперь g = ++ и e= []. Если f удовлетворяет условию  f(x, y++z) = f(x,y) ++ z, то

foldr(f,e, xs++ys) = foldr(f,e,xs) ++  foldr(f,e,ys)

Поскольку определенные нами операции acons и ccons ему удовлетворяют, получаем

map(f, xs ++ ys) = map(f, xs) ++ map(f, ys)
filter(p, xs ++ ys) = filter(p, xs) ++ filter(p, ys).

При g(x,y) = y ++ x, условие для f принимает вид f(x, z++y) =  z ++ f(x,y). Очевидно, что оно выполняется для функции snoc. Поэтому

reverse(xs ++ ys) =  reverse(ys) ++ reverse(xs)

Обозначим h(xs) = foldr(f,e,xs). Тогда, учитывая полученные результаты

h([]) = e
h(xs ++ ys) = g(h(xs), h(ys))

Собственно, только эти свойства h нам и понадобятся, чтобы вывести, что

h(concat(xs)) =
h(x₁++...x_n) = 
g(h(x₁), g(h(x₂), ... h(x_n))..) =
foldr(g,e,[h(x1), ... h(xn)] =
foldr(g,e,map(h,xs)).

Отсюда простой подстановкой получаем

length(concat(xs)) = sum(map(length, xs))
sum(concat(xs)) = sum(map(sum, xs))
all(concat(xs)) = all(map(all,xs))
f*(concat(xs)) = concat(map(f^*,xs))
p^?(concat(xs)) = concat(map(p^?,xs))

Вспоминая что concat(xs) = foldr(++, [], xs), можно предположить, что аналогичное свойство должно выполняться для свертки любой операции. Действительно, можно показать что, если

f(g(x,y)) = h(f(x), f(y))

то

f(foldr(g, a, xs)) =  foldr(h, f(a), map(f,xs)).

Рассматривая этот закон для логических функций f и положив h = and, получим:

Если
f(a) = true,
f(g(x,y)) = f(x) and f(y)
то
f(foldr(g, a, xs)) =  foldr(and, true, map(f,xs)) = all(map(f,xs)).

С практической точки зрения полезно перейти от равенства к отношению логического следования. Кроме того, удобнее рассматривать непустые списки. Тогда можно сформулировать следующий закон.

Если
f(x) and f(y) => f(g(x,y))
то
all(map(f,xs)) => f(foldr(g, xs)).

Другими словами если бинарная операция сохраняет некоторое свойство, то свертка этой операции также сохраняет это же свойство.

Левая свертка.

Рассматриваемый оператор обычно называют правой сверткой, потому, что операции выполняются справа налево. Мы определяли и левую свертку (foldl) выполняющую операции слева направо.

foldl(+, a, [x₁,x₂,...x_n]) = (...(a + x₁)+ x₂)+...x_n)

Левая свертка определяется уравнениями

foldl(f, a []) = a
foldl(f, a [x|xs]) = foldl(f, g(a,x), xs).

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

f([], a) = a
f([x|xs],a) =  f(xs, g(a,x))

можно представить как левую свертку

f(xs,a) = foldl(g,a,xa)

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

Теорема (закон двойственности для свертки).

Если f - ассоциативная операция, и e - нейтральный элемент то:
foldl(f, e, xs) = foldl(f, e, xs)

Упражнение.

Докажите этот закон индукцией.
Различие между [] и [x|xs] иногда не достаточно для доказательства. Вам придется различать три случая: пустой список, список из одного элемента и список по крайней мере с двумя элементами.

Используя закон двойственности, мы можем выразить через левую свертку многие функции, повышая их эффективность. Но не все операции ассоциативны. Рассмотрим случай когда f коммутативна f(x,y)=f(y,x)

foldr(f, e, [x₁,x₂,...x_n] ) =
f(x₁,f(x₂...f(x_n,e)...) ) =
f(f(x₂...f(x_n,e)...),x₁) =
...
f(f(...f(e,x_n)...),x₂),x₁) =
foldl(f, e, [x_n,...x₂,x₁] ).

То есть

foldl(f, e, xs) = foldl(f, e, reverse(xs))

Однако, коммутативные операции встречаются ещё реже. Тем не менее, для любой бинарной операции f можно определить симметричную ей операцию f', f'(x,y)=f(y,x). Повторяя с небольшими вариациями предыдущие рассуждения, получаем.

Второй закон двойственности

Для всех f, e и xs
foldl(f, e, xs) = foldl(f', e, reverse(xs))

Упражнение.

Докажите это утверждение.

Этот закон дает нам способ улучшить функцию reverse.

reverse(xs) =
id(reverse(xs))=
foldr(cons, [], reverse(xs)) =
foldl(cons', [], xs).

Легко видеть, что это и есть то самое определение fast_reverse, которое вызвало так много трудностей.

Упражнение.

Почему функция reverse часто встречается в программах?.

Сбалансированная свертка.

Давайте ещё раз обратимся к ассоциативным операциям. В этом случае результаты вычисления выражений

foldr(+, [a₁...a_n])  =  a₁ + (a₂ +...+ (a_n-1 + a_n)...) и
foldl(+, [a₁...a_n])  = (...(a₁ + a₂) +...) + a_n

совпадают. Более того, расставляя скобки произвольным образом мы будем получать все тот же результат. То есть, мы можем абстрагироваться от порядка вычислений и говорить об "абстрактной" свертке как о результате выражения

fold(+, [a₁...a_n])  =  a₁ + a₂ +...+ a_n

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

foldb(+, [a₁...a_n])  =   (...((a₁ + a₂) + (a₃ + a₄)) +(... (a_n-1 + a_n)...).

Ее можно выполнять "сверху вниз"

foldb(f,[x]) = x
foldb(f, xs) = f(foldb(take(length(xs)/2, xs)),foldb(drop(length(xs)/2, xs)))

take(0, xs) = []
take(n, [x|xs]) = [x | take(n-1, xs)]

drop(0, xs) = xs
drop(n, [x|xs]) = drop(n-1, xs)

или "снизу вверх"

foldb(f,[x]) = x
foldb(f, xs) = foldb(f,pair(f,xs))

pair(f,[]) = []
pair(f,[x]) = [x]
pair(f,[x1,x2|xs]) = [f(x1,x2) | pair(f,xs)];

Зачем это может понадобиться? Вспомним сортировку слиянием. Ее можно определить как свертку бинарной операции merge.

sort(xs) = foldb(merge, map(unit,xs))
unit(x) = [x]

Здесь важно, чтобы свертка была сбалансированной. Действительно, если мы используем правую свертку, то учитывая, что merge([x], ys) = insert(x, ys), получим сортировку вставками. С другой стороны, поскольку операция merge ассоциативна, все теоремы будут выполнятся для любой свертки и можем использовать их для доказательства правильности программы сортировки. Посмотрим как могло бы выглядеть такое доказательство.

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

I. ordered(sort(xs)),

где функция ordered(xs) возвращает true, если список xs упорядочен.

ordered([]) = true
ordered([x]) = true
ordered([x1,x2 | xs]) = (x1 =< x2) and ordered([x2 | xs])

Вторая часть несколько сложнее. Мы можем переформулировать её следующим образом: количество вхождений любого объекта в исходный список должно совпадать с количеством вхождений этого же объекта в список-результат.

II. count(a,sort(xs)) = count(a,xs)

Функция count(a,xs) возвращает число вхождений объекта a в список xs.

count(a,[]) = 0
count(a,[a | xs]) = 1 + count(a,xs)
count(a,[x | xs]) = count(a,xs) при x =/= a

Требуется доказать, что для функции sort выполняются утверждения I и II. Для доказательства нам потребуются следующие утверждения.

1. ordered(x) and ordered(y) => ordered(merge(x,y))
2. count(a, merge(x,y)) = count(a, x) + count(a, y)
3. count(a, x ++ y) = count(a, x) + count(a, y)
4. concat(map(unit, xs)) = xs

Последние два утверждения достаточно очевидны и легко доказываются. Утверждения 1 и 2 в сущности являются спецификацией функции merge. Их доказательство не сложно, но достаточно громоздко и мы примем их за аксиомы. Можно переходить к доказательству. 

I. Первая часть доказывается достаточно прямолинейно.

ordered(sort(xs)) =
ordered(fold(merge, map(unit, xs))) <= 
all(map(ordered, map(unit, xs))) =
all(map(ordered_unit(xs))) = true

Здесь ordered_unit - композиция функций ordered и unit, для которой

ordered_unit(x) = ordered(unit(x)) = ordered([x]) = true

II. Введем обозначение count_a(x) = count(a,xs). Заметим, что

count_a(sort(xs)) =
count_a(fold(merge, map(unit, xs))) =
fold(+, map(count_a,(map(unit, xs))).

С другой стороны

count_a(xs) =
count_a(concat(map(unit, xs)) =
count_a(foldr(++, map(unit, xs))) =
fold(+, map(count_a,(map(unit, xs))) .

Отсюда

count_a(sort(xs)) = count_a(xs)

Q.E.D.

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

unfold(p, f, g, x) = [] , при p(x)
unfold(p, f, g, x) = [f(x) | unfold(p, f, g, g(x))]

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

h(x) = [] , при p(x)
h(x) = [f(x)| h(g(x))]

может быть выражена через unfold

h(x) = unfold(p, f, g, x).

Упражнение.

Функция range(n,m) возвращает список чисел от n до m. Определите её через развертку.
Определите через развертку функции map и filter

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

¹ Свойство прозрачности ссылок оказывается полезным и для тестирования. Мы можем проверить каждую функцию отдельно и не заботиться о том, что её поведение может измениться вследствие изменения контекста.

² Если приведенные рассуждения показались слишком сложными, напишите функцию соединения списков на Си, а затем попытайтесь доказать её ассоциативность.

³ Его называют преобразованием развертки-свертки (unfold-fold transfirmation).

⁴ Не стоит путать термин "полиморфная функция" с одноименным понятием ООП. Иногда эти функции называют "параметрическими".

[ Содержание | 1 | 2 | 3 | 4 | 5 | 5.1 | 5.2 | 5.3 | 5.4 | 5.5 | 5.6 | 5.7 | 5.8 | 5.9 | 6 | 6.1 | 6.2 | 6.3 | 6.4 | 6.5 | 7 | 7.1 | Литература ]