Samlet funktionel programmering - Total functional programming

Total funktionel programmering (også kendt som stærk funktionel programmering , der står i kontrast til almindelig eller svag funktionel programmering ) er et programmeringsparadigme, der begrænser rækkevidden af ​​programmer til dem, der sandsynligvis afsluttes .

Begrænsninger

Opsigelse garanteres af følgende begrænsninger:

1. En begrænset form for rekursion , der kun fungerer på 'reducerede' former for dens argumenter, såsom Walther-rekursion , substrukturel rekursion eller "stærk normalisering" som bevist ved abstrakt fortolkning af kode.
2. Hver funktion skal være en total (i modsætning til delvis ) funktion. Det vil sige, det skal have en definition for alt inden for sit domæne.
   • Der er flere mulige måder at udvide almindeligt anvendte delfunktioner såsom division til at være total: vælge et vilkårligt resultat for input, som funktionen normalt er udefineret (såsom for division); tilføje et andet argument for at specificere resultatet for disse input; eller ekskludere dem ved brug af typesystemfunktioner såsom forfiningstyper .${\ displaystyle \ forall x \ in \ mathbb {N} .x \ div 0 = 0}$

Disse begrænsninger betyder, at total funktionel programmering ikke er Turing-komplet . Det sæt algoritmer, der kan bruges, er dog stadig enormt. For eksempel kan enhver algoritme, for hvilken en asymptotisk øvre grænse kan beregnes (af et program, der i sig selv kun bruger Walther-rekursion), trivielt omdannes til en beviseligt afsluttende funktion ved at bruge den øvre grænse som et ekstra argument, der er reduceret for hver iteration eller rekursion .

For eksempel er quicksort ikke trivielt vist at være substrukturel rekursiv, men det gentager sig kun til en maksimal dybde af vektorens længde (worst-case tidskompleksitet O ( n ² )). En quicksort-implementering på lister (som ville blive afvist af en substrukturel rekursiv checker) bruger Haskell :

import Data.List (partition)

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

For at gøre det substrukturelt rekursivt ved hjælp af længden af ​​vektoren som en grænse, kunne vi gøre:

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

Nogle klasser af algoritmer har ingen teoretisk øvre grænse, men har en praktisk øvre grænse (for eksempel kan nogle heuristiske baserede algoritmer programmeres til at "give op" efter så mange rekursioner, hvilket også sikrer afslutning).

Et andet resultat af total funktionel programmering er, at både streng evaluering og doven evaluering i princippet resulterer i den samme adfærd; dog kan den ene eller den anden stadig foretrækkes (eller endda kræves) af præstationsmæssige årsager.

I total funktionel programmering skelnes der mellem data og codata - førstnævnte er endelig , mens sidstnævnte potentielt er uendelig. Sådanne potentielt uendelige datastrukturer anvendes til applikationer som I / O . Brug af codata medfører brug af sådanne operationer som corecursion . Det er dog muligt at udføre I / O på et samlet funktionelt programmeringssprog (med afhængige typer ) også uden kodata.

Både Epigram og Charity kunne betragtes som samlede funktionelle programmeringssprog, selvom de ikke fungerer på den måde, som Turner specificerer i sit papir. Så kunne programmering direkte i almindeligt system F , i Martin-Löf-typeteori eller konstruktionsberegning .

Referencer