Teljes funkcionális programozás - Total functional programming

A teljes funkcionális programozás (más néven erős funkcionális programozás , szemben a közönséges vagy gyenge funkcionális programozással ) egy olyan programozási paradigma, amely a programok körét azokra korlátozza, amelyek bizonyíthatóan befejeződnek .

Korlátozások

A felmondást a következő korlátozások garantálják:

1. A rekurzió korlátozott formája , amely csak argumentumainak „redukált” formáin működik, mint például Walther rekurzió , szubstrukturális rekurzió vagy "erősen normalizálás", amint azt a kód absztrakt értelmezése bizonyítja .
2. Minden függvénynek teljes (szemben a részleges ) funkcióval kell rendelkeznie. Vagyis meg kell határoznia mindent a tartományán belül.
   • Számos lehetséges mód van az általánosan használt részfunkciók kiterjesztésére, például az osztás teljes összegére: tetszőleges eredmény kiválasztása olyan bemenetekre, amelyeken a függvény általában nincs meghatározva (például osztás esetén); újabb argumentum hozzáadása az inputok eredményének megadásához; vagy kizárja őket a tipusú rendszerfunkciók, például a finomítási típusok használatával .${\ displaystyle \ forall x \ in \ mathbb {N} .x \ div 0 = 0}$

Ezek a korlátozások azt jelentik, hogy a teljes funkcionális programozás nem teljes Turing-ben . Az alkalmazható algoritmusok halmaza azonban továbbra is hatalmas. Például bármely algoritmust, amelynek aszimptotikus felső határa kiszámítható (egy olyan programmal, amely maga csak Walther rekurziót használ), triviálisan átalakíthatjuk bizonyíthatóan végződő függvényvé, ha a felső határt használjuk minden egyes iteráción vagy rekurzión csökkentett extra argumentumként. .

Például a quicksort triviálisan nem bizonyítottan szubsztrukturális rekurzív, de csak a vektor hosszának maximális mélységéig ismétlődik (legrosszabb esetben az idő bonyolultsága O ( n ² )). A listákon lévő quicksort megvalósítás (amelyet egy alstrukturális rekurzív ellenőr elutasít) a Haskell segítségével :

import Data.List (partition)

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

Annak érdekében, hogy szubstrukturális rekurzívvá tegye a vektor hosszát korlátként, megtehetnénk:

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

Néhány algoritmusosztálynak nincs elméleti felső határa, de van gyakorlati felső határa (például egyes heurisztikus alapú algoritmusok beprogramozhatók "lemondásra" ennyi rekurzió után, biztosítva a felmondást is).

A teljes funkcionális programozás másik eredménye, hogy a szigorú értékelés és a lusta értékelés elvileg ugyanazt a viselkedést eredményezi; azonban egyik vagy másik teljesítmény-okokból továbbra is előnyösebb (vagy akár szükséges is lehet).

Összességében a funkcionális programozás, különbséget kell tenni a adatok és codata -az előbbi finitary , míg az utóbbi potenciálisan végtelen. Az ilyen, potenciálisan végtelen adatstruktúrákat használunk olyan alkalmazásokhoz, mint az I / O . A kodata használata olyan műveletek használatát vonja maga után, mint corecursion . Lehetséges azonban az I / O teljes funkcionális programozási nyelven ( függő típusokkal ) kodata nélkül is.

Az Epigram és a Charity is funkcionális programozási nyelvnek tekinthető, annak ellenére, hogy nem úgy működnek, ahogy Turner az írásában meghatározza. Így lehetne programozni közvetlenül a sima F rendszerben , a Martin-Löf típusú elméletben vagy az Építések számításában .

Hivatkozások