Total funktionale Programmierung - Total functional programming

Die vollständige funktionale Programmierung ( im Gegensatz zur normalen oder schwachen funktionalen Programmierung auch als starke funktionale Programmierung bezeichnet ) ist ein Programmierparadigma , das den Programmumfang auf diejenigen beschränkt, die nachweislich enden .

Beschränkungen

Die Kündigung wird durch folgende Einschränkungen garantiert:

  1. Eine eingeschränkte Form der Rekursion , die nur auf "reduzierte" Formen ihrer Argumente wie Walther-Rekursion , substrukturelle Rekursion oder "starke Normalisierung" angewendet wird , wie durch die abstrakte Interpretation von Code bewiesen wird .
  2. Jede Funktion muss eine Gesamtfunktion (im Gegensatz zu einer Teilfunktion ) sein. Das heißt, es muss eine Definition für alles in seiner Domäne haben.
    • Es gibt verschiedene Möglichkeiten, häufig verwendete Teilfunktionen wie die Division auf die Summe zu erweitern: Auswahl eines beliebigen Ergebnisses für Eingaben, für die die Funktion normalerweise nicht definiert ist (z. B. für die Division); Hinzufügen eines weiteren Arguments, um das Ergebnis für diese Eingaben anzugeben; oder Ausschluss durch Verwendung von Typsystemfunktionen wie Verfeinerungstypen .

Diese Einschränkungen führen dazu, dass die gesamte funktionale Programmierung nicht vollständig ist . Die Menge der Algorithmen, die verwendet werden können, ist jedoch immer noch riesig. Beispielsweise kann jeder Algorithmus, für den eine asymptotische Obergrenze berechnet werden kann (durch ein Programm, das selbst nur die Walther-Rekursion verwendet), trivial in eine nachweislich terminierende Funktion umgewandelt werden, indem die Obergrenze als zusätzliches Argument verwendet wird, das bei jeder Iteration oder Rekursion dekrementiert wird .

Beispielsweise wird Quicksort nicht trivial als substrukturell rekursiv dargestellt, sondern nur bis zu einer maximalen Tiefe der Länge des Vektors (Zeitkomplexität O ( n 2 ) im ungünstigsten Fall ). Eine QuickSort-Implementierung für Listen (die von einem rekonstruktiven Substrukturprüfer abgelehnt würde) ist die Verwendung von Haskell : 

import Data.List (partition)

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

Um die Substruktur unter Verwendung der Länge des Vektors als Grenze rekursiv zu machen, können wir Folgendes tun: 

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

Einige Klassen von Algorithmen haben keine theoretische Obergrenze, aber eine praktische Obergrenze (zum Beispiel können einige heuristische Algorithmen so programmiert werden, dass sie nach so vielen Rekursionen "aufgeben" und auch die Beendigung sicherstellen).

Ein weiteres Ergebnis der vollständigen funktionalen Programmierung ist, dass sowohl eine strikte Bewertung als auch eine verzögerte Bewertung im Prinzip zu demselben Verhalten führen. Das eine oder andere kann jedoch aus Leistungsgründen immer noch vorzuziehen (oder sogar erforderlich sein).

Bei der gesamten funktionalen Programmierung wird zwischen Daten und Codaten unterschieden - die erstere ist endlich , während die letztere möglicherweise unendlich ist. Solche potenziell unendlichen Datenstrukturen werden für Anwendungen wie E / A verwendet . Die Verwendung von Codaten erfordert die Verwendung von Operationen wie Corecursion . Es ist jedoch möglich, E / A in einer voll funktionsfähigen Programmiersprache (mit abhängigen Typen ) auch ohne Codaten durchzuführen.

Sowohl Epigram als auch Charity könnten als voll funktionsfähige Programmiersprachen betrachtet werden, obwohl sie nicht so funktionieren, wie Turner es in seinem Artikel spezifiziert. So könnte man direkt im einfachen System F programmieren , in der Martin-Löf-Typentheorie oder in der Konstruktionsrechnung .

Verweise