Общее функциональное программирование (также известное как сильное функциональное программирование , [1] , чтобы быть противопоставлено обычным или слабым функциональным программированием ) является программирование парадигмы , которая ограничивает спектр программ для тех, которые доказуемо прекращения . [2]
Ограничения
Прекращение действия гарантируется следующими ограничениями:
- Ограниченная форма рекурсии , которая работает только с «сокращенными» формами своих аргументов, такими как рекурсия Вальтера , субструктурная рекурсия или «строго нормализирующая», что доказано абстрактной интерпретацией кода. [3]
- Каждая функция должна быть общей (а не частичной ) функцией. То есть у него должно быть определение для всего, что находится в его области.
- Существует несколько возможных способов расширения часто используемых частичных функций, таких как деление, до итогового: выбор произвольного результата для входных данных, на которых функция обычно не определена (например, для деления); добавление еще одного аргумента, чтобы указать результат для этих входов; или исключение их с помощью функций системы типов, таких как типы уточнения . [2]
Эти ограничения означают, что полное функциональное программирование не является полным по Тьюрингу . Однако набор алгоритмов, которые можно использовать, по-прежнему огромен. Например, любой алгоритм, для которого может быть вычислена асимптотическая верхняя граница (с помощью программы, которая сама использует только рекурсию Вальтера), можно тривиально преобразовать в доказуемо завершающую функцию, используя верхнюю границу в качестве дополнительного аргумента, уменьшающегося на каждой итерации или рекурсии. .
Например, нетривиально показано , что быстрая сортировка является субструктурной рекурсивной, но она повторяется только до максимальной глубины длины вектора (временная сложность наихудшего случая O ( n 2 )). Реализация быстрой сортировки в списках (которая будет отклонена субструктурной рекурсивной проверкой) с использованием Haskell :
импорт Data.List ( раздел )qsort [] = [] qsort [ a ] = [ a ] qsort ( a : as ) = let ( меньше , больше ) = раздел ( < a ) как в qsort меньше ++ [ a ] ++ qsort больше
Чтобы сделать его субструктурной рекурсивной, используя длину вектора в качестве предела, мы могли бы сделать:
импорт Data.List ( раздел )qsort x = qsortSub x x - минимальный случай qsortSub [] as = as - показывает завершение - стандартные случаи qsort qsortSub ( l : ls ) [] = [] - нерекурсивный, поэтому принят qsortSub ( l : ls ) [ a ] = [ a ] - нерекурсивный, поэтому принято qsortSub ( l : ls ) ( a : as ) = let ( меньше , больше ) = partition ( < a ) as - рекурсивно, но повторяется на ls, который является подструктурой - его первый вход. в qsortSub ls меньше ++ [ a ] ++ qsortSub ls больше
Некоторые классы алгоритмов не имеют теоретической верхней границы, но имеют практическую верхнюю границу (например, некоторые алгоритмы на основе эвристики могут быть запрограммированы так, чтобы «сдаваться» после стольких рекурсий, также обеспечивая завершение).
Другой результат тотального функционального программирования состоит в том, что как строгая оценка, так и ленивая оценка в принципе приводят к одному и тому же поведению; тем не менее, тот или иной вариант может быть предпочтительным (или даже обязательным) по соображениям производительности. [4]
В общем функциональном программировании, проводится различие между данными и КОДАТОМ -The бывшим является финитарным , в то время как последний является потенциально бесконечным. Такие потенциально бесконечные структуры данных используются для таких приложений, как ввод-вывод . Использование codata влечет за собой использование таких операций, как corecursion . Однако можно выполнять ввод-вывод на полном языке функционального программирования (с зависимыми типами ) также без кодовых данных. [5]
И Epigram, и Charity можно считать полностью функциональными языками программирования, хотя они не работают так, как указывает Тернер в своей статье. То же самое можно сказать и о программировании непосредственно в простой Системе F , в теории типов Мартина-Лёфа или в исчислении конструкций .
Рекомендации
- ↑ Этот термин принадлежит: Turner, DA (декабрь 1995 г.). Элементарное сильное функциональное программирование . Первый международный симпозиум по языкам функционального программирования в образовании. Springer LNCS. 1022 . С. 1–13..
- ^ а б Тернер, Д. А. (2004-07-28), "Общая Функциональное программирование" , журнал Юниверсал Computer Science , 10 (7): 751-768, DOI : 10.3217 / jucs-010-07-0751
- ^ Тернер, Д. А. (2000-04-28), "Обеспечение Расторжение в ESFP" , журнал Юниверсал Computer Science , 6 (4): 474-488, DOI : 10.3217 / jucs-006-04-0474
- ^ Различия между ленивым и нетерпеливым оцениванием обсуждаются в: Гранстрем, Дж. Г. (2011). Трактат по интуиционистской теории типов . Логика, эпистемология и единство науки. 7 . ISBN 978-94-007-1735-0. См., В частности, стр. 86–91.
- ^ Granström, JG (май 2012), "Новая парадигма для компонентов на основе развития", журнал программного обеспечения , 7 (5): 1136-1148, DOI : 10,4304 / jsw.7.5.1136-1148[ мертвая ссылка ] Архивная копия