Формализм Берда-Меертенса - Bird–Meertens formalism

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

Иногда это упоминается в публикациях как BMF, как намек на Форма Бэкуса – Наура. В шутку это также называют Squiggol, как дань уважения АЛГОЛ, который также входил в компетенцию WG 2.1, а также из-за «волнистых» символов, которые он использует. Менее используемый вариант имени, но на самом деле первый из предложенных: СКВИГОЛ.

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

карта хорошо известная функция второго порядка, которая применяет данную функцию к каждому элементу списка; в BMF написано ${displaystyle *}$:

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

Так же, уменьшать это функция, которая сворачивает список в одно значение с помощью повторное применение бинарного оператора. Написано / в BMF. ${displaystyle oplus }$ как подходящий бинарный оператор с нейтральным элементом е, у нас есть

${displaystyle oplus /[e_{1},dots ,e_{n}]=eoplus e_{1}oplus dots oplus e_{n}.}$

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

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

${displaystyle {m {flatten}} [l_{1},dots ,l_{n}]=+!!!+/[l_{1},dots ,l_{n}]=[,]+!!!+;l_{1}+!!!+dots +!!!+;l_{n}={ ext{ the concatenation of all lists }}l_{k}.}$

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

Примеры применяемых законов
Закон о продвижении карт
Сложите закон о продвижении
Обобщенное правило Хорнера
Лемма про сканирование
Закон слияния с разверткой

Точно так же написание ${displaystyle cdot }$ за функциональный состав и ${displaystyle land }$ за соединение, легко написать функцию, проверяющую, что все элементы списка удовлетворяют предикату п, просто как ${displaystyle {m {all}} p=(land /)cdot (p*)}$:

${displaystyle {egin{aligned}{m {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) преобразует неэффективные простые для понимания выражения («спецификации») в эффективные задействованные выражения («программы») с помощью алгебраических манипуляций. Например, спецификация "${displaystyle mathrm {max} cdot mathrm {map} ;mathrm {sum} cdot mathrm {segs} }$"является почти дословным переводом" алгоритм максимальной суммы сегмента ",^[1] но запуск этой функциональной программы в списке размеров ${displaystyle n}$ потребуется время ${displaystyle {mathcal {O}}(n^{3})}$ в целом. Исходя из этого, Bird вычисляет эквивалентную функциональную программу, которая выполняется во времени. ${displaystyle {mathcal {O}}(n)}$, и фактически является функциональной версией Алгоритм Кадане.

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

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

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

${displaystyle {egin{aligned}&h [,]&&= e&h (l+!!!+;m)&&= h loplus h m.end{aligned}}}$

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

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

Смотрите также

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

Рекомендации

1. Где ${displaystyle mathrm {max} }$, ${displaystyle mathrm {sum} }$, и ${displaystyle mathrm {segs} }$ возвращает наибольшее значение, сумму и список всех сегментов (то есть подсписок) данного списка.
2. Каждое выражение в строке обозначает исполняемую функциональную программу для вычисления максимальной суммы сегментов.

• Ламберт Меертенс (1986). «Алгоритмика: к программированию как математической деятельности».. В J.W. де Баккер; М. Хазевинкель; J.K. Ленстра (ред.). Математика и информатика, Монографии CWI Том 1. Северная Голландия. С. 289–334.
• Ламберт Меертенс; Ричард Берд (1987). «Два упражнения из книги по алгоритмике» (PDF). Северная Голландия.
• Ричард С. Берд (1989). «Алгебраические тождества для программного расчета» (PDF). Компьютерный журнал. 32 (2): 122–126. Дои:10.1093 / comjnl / 32.2.122.
• Ричард Берд; Oege de Moor (1997). Алгебра программирования, Международная серия по вычислительной технике, Vol. 100. Прентис Холл. ISBN  0-13-507245-X.

• Коул, Мюррей (1993). "Параллельное программирование, гомоморфизмы списков и проблема максимальной суммы отрезков". Параллельные вычисления: тенденции и приложения, PARCO 1993, Гренобль, Франция. С. 489–492.