Programmiersprachen für eine effiziente Berechnung

32

Es ist unmöglich, eine Programmiersprache zu schreiben, die alle Maschinen zulässt, die an allen Eingaben anhalten, und keine anderen. Es scheint jedoch einfach zu sein, eine solche Programmiersprache für jede Standardkomplexitätsklasse zu definieren. Insbesondere können wir eine Sprache definieren, in der wir alle effizienten Berechnungen und nur effiziente Berechnungen ausdrücken können.

Zum Beispiel für etwas wie : Nehmen Sie Ihre bevorzugte Programmiersprache und fügen Sie nach dem Schreiben Ihres Programms (entsprechend Turing Machine ) dem Header drei Werte hinzu: eine Ganzzahl und eine Ganzzahl sowie eine Standardausgabe . Wenn das Programm kompiliert wird, ein Ausgang Turing Maschine , dass die Eingabe gegeben der Größe läuft auf für cn ^ k Schritten. Wenn M ' nicht anhält, bevor die cn ^ k- Schritte abgelaufen sind, geben Sie den Standardausgang d ausM ' c k d M x n M 'PMckdMxnMxcnkMcnkd. Wenn ich mich nicht irre, können wir mit diesen Programmiersprachen alle Berechnungen in und nicht mehr ausdrücken . Diese vorgeschlagene Sprache ist jedoch von Natur aus nicht interessant.P

Meine Frage: Gibt es Programmiersprachen, die Teilmengen von berechenbaren Funktionen (z. B. alle effizient berechenbaren Funktionen) auf nicht triviale Weise erfassen? Wenn nicht, gibt es einen Grund dafür?

Artem Kaznatcheev
quelle
7
Einige einfache Beispiele für Programmiersprachen, die Teilmengen berechenbarer Funktionen erfassen: reguläre Ausdrücke und kontextfreie Grammatiken.
Jukka Suomela
2
Tatsächlich sind die Sprachen, die die Komplexitätsklasse wie (die auf ähnliche Weise wie primitive rekursive Funktionen definiert wird, bei denen die Rekursion durch die beschränkte Rekursion ersetzt wird), (zumindest aus theoretischer Sicht) sehr interessant. :)P VPPV
Kaveh
Die lineare und die ganzzahlige Programmierung erfassen interessante Teilmengen berechenbarer Funktionen.
Diego de Estrada
Datalog kann nur polynomielle Zeitalgorithmen ausdrücken, aber ich weiß nicht, ob es alle polynomiellen Zeitalgorithmen ausdrücken kann.
Jules
Die bekannte Veröffentlichung "Total Functional Programming" argumentiert, dass Programmiersprachen, die kein unentscheidbares Halteproblem haben, tatsächlich praktisch und nützlich sind. jucs.org/jucs_10_7/total_functional_programming
none

Antworten:

32

Eine Sprache, die versucht, nur polynomielle Zeitberechnungen auszudrücken, ist der weiche Lambda-Kalkül . Das Typensystem basiert auf linearer Logik. Eine aktuelle Arbeit befasst sich mit Polynomzeitkalkülen und bietet eine gute Zusammenfassung der jüngsten Entwicklungen, die auf diesem Ansatz basieren. Martin Hofmann beschäftigt sich schon länger mit dem Thema. Eine ältere Liste relevanter Artikel finden Sie hier ; Viele seiner Arbeiten gehen in diese Richtung.

Bei anderen Arbeiten wird mithilfe abhängiger Typen oder typisierter Assemblersprachen überprüft, ob das Programm eine bestimmte Menge an Ressourcen verwendet .

Noch andere Ansätze basieren auf ressourcengebundenen formalen Kalkülen , wie z. B. Varianten der Umgebungskalkulation.

Diese Ansätze haben die Eigenschaft, dass gut typisierte Programme einige vordefinierte Ressourcengrenzen erfüllen. Die gebundene Ressource kann zeitlich oder räumlich sein und im Allgemeinen von der Größe der Eingaben abhängen.

Frühe Arbeiten in diesem Bereich befassen sich mit stark normalisierenden Kalkülen, was bedeutet, dass alle gut typisierten Programme anhalten. System F , auch bekannt als polymorpher Lambda-Kalkül, normalisiert sich stark. Es gibt keinen Festkommaoperator, aber es ist trotzdem sehr aussagekräftig, obwohl ich nicht glaube, dass es bekannt ist, welcher Komplexitätsklasse es entspricht. Definitionsgemäß drückt jeder stark normalisierende Kalkül eine Klasse von Abschlussberechnungen aus.

Die Programmiersprache Charity ist eine recht ausdrucksstarke Funktionssprache, die bei allen Eingaben anhält. Ich weiß nicht, welche Komplexitätsklasse es ausdrücken kann, aber die Ackermann-Funktion kann in Charity geschrieben werden.

Dave Clarke
quelle
Was meinst du mit "zumindest" hier?
nponeccop
"Zumindest" bedeutet hier "einige". Ich werde meine Antwort ändern, um sie etwas präziser zu gestalten.
Dave Clarke
Ich bin mir ziemlich sicher, dass die Komplexität der in System F definierbaren Funktionen die Klasse von Funktionen ist, die mit der Zeit "eine nachweislich Gesamtfunktion der Arithmetik 2. Ordnung" der Eingabe abschließen. Keine sehr konventionelle Komplexitätsklasse, aber dennoch ...
cody
cody: Nach Wadlers "Theorems for free" kann System F "jede rekursive Funktion ausdrücken, die sich in Peano-Arithmetik zweiter Ordnung als vollständig beweisen lässt", und zwar "einschließlich [...] Ackermanns Funktion". Ich bin mir nicht sicher, ob das dasselbe ist, das Sie beschreiben. Das Hauptmerkmal von Charity ist die Unterstützung von Codata, während ich denke, dass die Terminierungsprüfung von Agda mehr Expressivität als Coq und System F ermöglicht und gleichzeitig die Terminierung garantiert.
Blaisorblade
8

Als Ansatz möchte ich auch die implizite Komplexitätstheorie erwähnen, da ich sie in einigen Fragen gesehen habe, die etwas miteinander zu tun haben. Um diese Antwort von Neel Krishnaswami zu zitieren :

Die grundlegende Technik besteht darin, Komplexitätsklassen mit Subsystemen der linearen Logik (der sogenannten "leichten linearen Logik") in Beziehung zu setzen, mit der Idee, dass die Schnitteliminierung für das logische System für die gegebene Komplexitätsklasse vollständig sein sollte (wie LOGSPACE, PTIME usw.). Über Curry-Howard erhält man dann eine Programmiersprache, in der genau die Programme der jeweiligen Klasse zum Ausdruck kommen.

Chris Pressey
quelle
5

Ich bin überrascht, dass niemand die primitive Rekursion erwähnt hat. Durch Beschränkung auf begrenzte Schleifen (dh die Anzahl der Iterationen für jede Schleife muss berechnet werden, bevor die Schleife beginnt) ist das resultierende Programm primitiv rekursiv und daher total. Douglas Hofstadter schlug eine Programmiersprache vor, BLOOP, die alle und nur primitive rekursive Funktionen zuließ.

David Harris
quelle
1
Es ist eine ordentliche Unterklasse aller Funktionen, aber es als Klasse "effizienter" Funktionen zu bezeichnen, kann ein bisschen schwierig sein.
Raphael,
PP
Andere erwähnten System F und andere stark normalisierende Sprachen, die gewissermaßen nur "primitive Rekursion" unterstützen. Da sie jedoch erstklassige Funktionen unterstützen, können Sie mehr Programme schreiben (wie die Ackermann-Funktion).
Blaisorblade