Полное функциональное программирование

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

Ограничения

Прекращение действия гарантируется следующими ограничениями:

1. Ограниченная форма рекурсии , которая работает только с «сокращенными» формами своих аргументов, такими как рекурсия Вальтера , субструктурная рекурсия или «сильная нормализация», что доказано абстрактной интерпретацией кода.
2. Каждая функция должна быть полной (а не частичной ) функцией. То есть у него должно быть определение всего, что находится в его области.
   • Существует несколько возможных способов расширить часто используемые частичные функции, такие как деление, до суммы: выбор произвольного результата для входных данных, на которых функция обычно не определена (например, $\forall x\in \mathbb {N} .x\div 0=0$ для деления); добавление еще одного аргумента для указания результата для этих входных данных; или исключить их с помощью функций системы типов, таких как уточненные типы .

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

Например, быстрая сортировка не является тривиально субструктурно-рекурсивной, но она рекурсивна только до максимальной глубины длины вектора (временная сложность в худшем случае O ( n ² )). Реализация быстрой сортировки в списках (которая будет отклонена субструктурной рекурсивной проверкой) с использованием Haskell :

import Data.List (partition)

qsort []       = []
qsort [a]      = [a]
qsort (a:as)   = let (lesser, greater) = partition (<a) as
                 in qsort lesser ++ [a] ++ qsort greater

Чтобы сделать его субструктурно-рекурсивным, используя длину вектора в качестве ограничения, мы могли бы сделать:

import Data.List (partition)

qsort x = qsortSub x x
-- minimum case
qsortSub []     as     = as -- shows termination
-- standard qsort cases
qsortSub (l:ls) []     = [] -- nonrecursive, so accepted
qsortSub (l:ls) [a]    = [a] -- nonrecursive, so accepted
qsortSub (l:ls) (a:as) = let (lesser, greater) = partition (<a) as
                            -- recursive, but recurs on ls, which is a substructure of
                            -- its first input.
                         in qsortSub ls lesser ++ [a] ++ qsortSub ls greater

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

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

В тотальном функциональном программировании различают данные и кодаты : первые являются финитными , а вторые потенциально бесконечны. Такие потенциально бесконечные структуры данных используются для таких приложений, как ввод-вывод . Использование кодатов влечет за собой использование таких операций, как corecursion . Однако можно выполнять ввод-вывод на функциональном языке программирования (с зависимыми типами ) и без кодовых данных.

И Epigram , и Charity можно считать полностью функциональными языками программирования, хотя они и не работают так, как указывает Тернер в своей статье. То же самое можно сделать и с программированием непосредственно в простой системе F , в теории типов Мартина-Лёфа или в исчислении конструкций .

См. также

• Анализ завершения