Формализм Бёрда – Меертенса

Формализм Бёрда -Меертенса ( BMF ) представляет собой расчет для получения программ на основе спецификаций программ (в условиях функционального программирования ) посредством процесса эквациональных рассуждений. Он был разработан Ричардом Бёрдом и Ламбертом Меертенсом в рамках их работы в рамках Рабочей группы 2.1 ИФИП .

В публикациях его иногда называют BMF, как отсылку к форме Бэкуса-Наура . В шутку его также называют Squiggol , как дань уважения ALGOL , который также входил в компетенцию WG 2.1, а также из-за используемых в нем «волнистых» символов. Менее используемый вариант имени, но фактически предложенный первым — SQUIGOL .Мартин и Нипкоу предоставили автоматизированную поддержку для проверки разработки Squiggol, используя Larch Prover .

Основные примеры и обозначения

Map — это хорошо известная функция второго порядка, которая применяет заданную функцию к каждому элементу списка; в БМФ написано $*$:

$f*[e_{1},\dots ,e_{n}]=[f\ e_{1},\dots ,f\ e_{n}].$

Аналогично, сокращение — это функция, которая сворачивает список в одно значение путем многократного применения бинарного оператора . Написано/в BMF.принимая $\oplus$ в качестве подходящего бинарного оператора с нейтральным элементом e мы имеем

$\oplus /[e_{1},\dots ,e_{n}]=e\oplus e_{1}\oplus \dots \oplus e_{n}.$

Используя эти два оператора и примитивы $+$ (как обычное дополнение) и $+\!\!\!+$ (для объединения списков) мы можем легко выразить сумму всех элементов списка и функцию выравнивания как ${\rm {sum}}=+/$ и ${\rm {flatten}}=+\!\!\!+/$, в бесточечный стиль . У нас есть:

${\rm {sum}}\ [e_{1},\dots ,e_{n}]=+/[e_{1},\dots ,e_{n}]=0+e_{1}+\dots +e_{n}=\sum _{k}e_{k}.$

${\rm {flatten}}\ [l_{1},\dots ,l_{n}]=+\!\!\!+/[l_{1},\dots ,l_{n}]=[\,]+\!\!\!+\;l_{1}+\!\!\!+\dots +\!\!\!+\;l_{n}={\text{ the concatenation of all lists }}l_{k}.$

Вывод алгоритма Кадане

Аналогично, написав $\cdot$ функционального состава и $\land$ для конъюнкции легко написать функцию, проверяющую, что все элементы списка удовлетворяют предикату p , просто как ${\rm {all}}\ p=(\land /)\cdot (p*)$:

${\begin{aligned}{\rm {all}}\ p\ [e_{1},\dots ,e_{n}]&=(\land /)\cdot (p*)\ [e_{1},\dots ,e_{n}]\\&=\land /(p*[e_{1},\dots ,e_{n}])\\&=\land /[p\ e_{1},\dots ,p\ e_{n}]\\&=p\ e_{1}\land \dots \land p\ e_{n}\\&=\forall k\ .\ p\ e_{k}.\end{aligned}}$

Берд (1989) преобразует неэффективные, простые для понимания выражения («спецификации») в эффективные сложные выражения («программы») посредством алгебраических манипуляций. Например, спецификация " $\mathrm {max} \cdot \mathrm {map} \;\mathrm {sum} \cdot \mathrm {segs}$«является почти дословным переводом задачи о максимальной сумме сегментов , но запуск этой функциональной программы в списке размера $n$ потребуется время ${\mathcal {O}}(n^{3})$ в общем. Исходя из этого, Берд вычисляет эквивалентную функциональную программу, работающую во времени. ${\mathcal {O}}(n)$, и по сути является функциональной версией алгоритма Кадане .

Вывод показан на рисунке, с вычислительными сложностями выделены синим цветом, а юридические применения обозначены красным.Примеры законов можно открыть, нажав на [показать] ; они используют списки целых чисел, сложение, минус и умножение. Обозначения в статье Берда отличаются от использованных выше: $\mathrm {map}$, $\mathrm {concat}$, и $\mathrm {foldl}$ соответствуют $*$, $\mathrm {flatten}$и обобщенная версия $/$ выше, соответственно, в то время как $\mathrm {inits}$ и $\mathrm {tails}$ вычислить список всех префиксов и суффиксов своих аргументов соответственно. Как и выше, композиция функций обозначается « $\cdot$", который имеет наименьший приоритет привязки . В примерах списки раскрашиваются в зависимости от глубины вложенности; в некоторых случаях новые операции определяются ad hoc (серые прямоугольники).

Лемма о гомоморфизме и ее приложения к параллельным реализациям.

Функция h в списках называется гомоморфизмом списка , если существует ассоциативный бинарный оператор $\oplus$ и нейтральный элемент $e$ такой, что имеет место следующее:

${\begin{aligned}&h\ [\,]&&=\ e\\&h\ (l+\!\!\!+\;m)&&=\ h\ l\oplus h\ m.\end{aligned}}$

Лемма о гомоморфизме утверждает, что h является гомоморфизмом тогда и только тогда, когда существует оператор $\oplus$ и функция f такая, что $h=(\oplus /)\cdot (f*)$.

Большой интерес для этой леммы представляет ее применение к выводу высокопараллельных реализаций вычислений. Действительно, тривиально увидеть, что $f*$ имеет высокопараллельную реализацию, как и $\oplus /$ — наиболее очевидно, как двоичное дерево. Таким образом, для любого гомоморфизма списка h существует параллельная реализация. Эта реализация разбивает список на фрагменты, которые назначаются разным компьютерам; каждый вычисляет результат на своем собственном фрагменте. Именно эти результаты проходят по сети и окончательно объединяются в один. В любом приложении, где список огромен, а результатом является очень простой тип (скажем, целое число), преимущества распараллеливания значительны. Это основа подхода уменьшения карты .

См. также

• Катаморфизм
• Анаморфизм
• Параморфизм
• гиломорфизм

Ссылки

• Меертенс, Ламберт (1986). «Алгоритмика: На пути к программированию как математической деятельности» . Ин де Баккер, JW; Хазевинкель, М.; Ленстра, Дж. К. (ред.). Математика и информатика . Монографии КРИ. Том. 1. Северная Голландия. стр. 289–334.
• Меертенс, Ламберт ; Берд, Ричард (1987). «Два упражнения из книги по алгоритмике» (PDF) . Северная Голландия.
• Бэкхаус, Роланд (1988). Исследование формализма Берда-Меертенса (PDF) (Технический отчет).
• Берд, Ричард С. (1989). «Алгебраические тождества для вычислений в программах» (PDF) . Компьютерный журнал . 32 (2): 122–126. дои : 10.1093/comjnl/32.2.122 .
• Коул, Мюррей (1993). «Параллельное программирование, гомоморфизмы списков и проблема максимальной суммы сегментов» . Параллельные вычисления: тенденции и приложения, PARCO 1993, Гренобль, Франция . стр. 489–492.
• Бэкхаус, Роланд ; Хугендейк, Пол (1993). Элементы реляционной теории типов данных (PDF) . стр. 7–42. дои : 10.1007/3-540-57499-9_15 . ISBN  978-3-540-57499-6 .
• Банкенбург, Александр (1994). О'Доннелл, Джон Т.; Хаммонд, Кевин (ред.). Иерархия бума (PDF) . Функциональное программирование, Глазго, 1993: Материалы семинара по функциональному программированию в Глазго 1993 года, Эр, Шотландия, 5–7 июля 1993 года . Лондон: Спрингер. стр. 1–8. дои : 10.1007/978-1-4471-3236-3_1 . ISBN  978-1-4471-3236-3 .
• Бёрд, Ричард ; де Мур, Оге (1997). Алгебра программирования . Международная серия по информатике. Том. 100. Прентис Холл. ISBN  0-13-507245-Х .
• Гиббонс, Джереми (2020). Трой Астарта (ред.). Школа Сквиггола: История формализма Берда-Меертенса (PDF) . Формальные методы (Практикум по истории формальных методов) . ЛНКС. Том. 12233. Спрингер. дои : 10.1007/978-3-030-54997-8_2 .