Całkowite programowanie funkcyjne
Całkowite programowanie funkcjonalne (znane również jako silne programowanie funkcjonalne , w przeciwieństwie do zwykłego lub słabego programowania funkcjonalnego ) to paradygmat programowania , który ogranicza zakres programów do tych, które można udowodnić .
Ograniczenia
Wypowiedzenie jest gwarantowane przez następujące ograniczenia:
- Ograniczona forma rekurencji , która działa tylko na „zredukowanych” formach swoich argumentów, takich jak rekurencja Walthera , rekurencja podstrukturalna lub „silnie normalizująca”, czego dowodzi abstrakcyjna interpretacja kodu.
- Każda funkcja musi być funkcją całkowitą (w przeciwieństwie do częściowej ). Oznacza to, że musi mieć definicję wszystkiego w swojej domenie.
- Istnieje kilka możliwych sposobów rozszerzenia często używanych funkcji częściowych, takich jak dzielenie, na całkowite: wybranie dowolnego wyniku dla danych wejściowych, dla których funkcja jest normalnie niezdefiniowana (na przykład ∀ x dla dzielenia); dodanie kolejnego argumentu, aby określić wynik dla tych danych wejściowych; lub wykluczając je za pomocą funkcji systemu typu, takich jak typy uszlachetniania .
Te ograniczenia oznaczają, że całkowite programowanie funkcjonalne nie jest kompletne w sensie Turinga . Jednak zestaw algorytmów, które można wykorzystać, jest wciąż ogromny. Na przykład dowolny algorytm, dla którego asymptotyczną górną granicę (za pomocą programu, który sam używa tylko rekurencji Walthera) można w prosty sposób przekształcić w funkcję kończącą się w sposób dający się udowodnić, używając górnej granicy jako dodatkowego argumentu zmniejszanego przy każdej iteracji lub rekursji .
Na przykład szybkie sortowanie nie jest banalnie pokazane jako substrukturalne rekurencyjne, ale powtarza się tylko do maksymalnej głębokości długości wektora (w najgorszym przypadku złożoność czasowa O ( n 2 )). Implementacją szybkiego sortowania na listach (która zostałaby odrzucona przez podstrukturalny rekurencyjny kontroler) jest użycie Haskella :
import Data.List ( partycja ) qsort [] = [] qsort [ a ] = [ a ] qsort ( a : as ) = niech ( mniejszy , większy ) = partycja ( < a ) jak w qsort mniejszy ++ [ a ] + + qsort większy
Aby uczynić go substrukturalnym rekurencyjnym, używając długości wektora jako granicy, moglibyśmy zrobić:
import Data.List ( partition ) qsort x = qsortSub x x -- minimalny przypadek qsortSub [] as = as -- pokazuje zakończenie -- standardowe przypadki qsort qsortSub ( l : ls ) [] = [] -- nierekurencyjne, więc akceptowane qsortSub ( l : ls ) [ za ] = [ za ]
-- nierekurencyjny, więc akceptowany qsortSub ( l : ls ) ( a : as ) = let ( lesser , większy ) = partition ( < a ) as -- rekurencyjny, ale rekurencyjny na ls, który jest podstrukturą -- jego pierwszego wejścia . in qsortSub ls mniejszy ++ [ a ] ++ qsortSub ls większy
Niektóre klasy algorytmów nie mają teoretycznej górnej granicy, ale mają praktyczną górną granicę (na przykład niektóre algorytmy oparte na heurystyce można zaprogramować tak, aby „poddawały się” po tak wielu rekurencjach, zapewniając również zakończenie).
Innym wynikiem całkowitego programowania funkcjonalnego jest to, że zarówno ścisła ocena , jak i leniwa ocena skutkują w zasadzie tym samym zachowaniem; jednak jeden lub drugi może być nadal preferowany (lub nawet wymagany) ze względu na wydajność.
W całkowitym programowaniu funkcjonalnym rozróżnia się dane i kody — pierwsze są skończone , a drugie potencjalnie nieskończone. Takie potencjalnie nieskończone struktury danych są wykorzystywane w aplikacjach takich jak I/O . Korzystanie z codata pociąga za sobą stosowanie takich operacji jak corecursion . Jednak możliwe jest wykonanie I/O w całkowicie funkcjonalnym języku programowania (z typami zależnymi ) również bez kodowania.
Zarówno Epigram , jak i Charity można uznać za w pełni funkcjonalne języki programowania, mimo że nie działają one w sposób określony przez Turnera w jego artykule. Podobnie programowanie bezpośrednio w zwykłym Systemie F , w teorii typów Martina-Löfa lub rachunku konstrukcji .