Primitive rekursive Funktionen für Programmierer in der Praxis

 (matklad.github.io)
2 Punkte von GN⁺ 2024-08-05 | 1 Kommentare | Auf WhatsApp teilen
  • Diskussionen nach dem Muster „Wenn es nicht Turing-vollständig ist, ist es sicher“ verfehlen die mathematische Bedeutung, und Nicht-Turing-Vollständigkeit hat mit praktischen Eigenschaften wie Terminierung, Determinismus oder Sandboxing meist nur wenig zu tun
  • Berechnungen einer Turing-Maschine, deren Laufzeit durch eine primitive rekursive Funktion der Eingabe beschränkt ist, lassen sich auch wieder als primitive rekursive Funktionen ausdrücken
  • Primitive rekursive Funktionen terminieren immer, können aber trotzdem extrem schnell wachsende Funktionen wie 2^(2^N) bilden; eine garantierte Terminierung bedeutet also nicht automatisch praktikable Laufzeit
  • In der Praxis verursachen Programme, die nie anhalten, und Programme, die erst in Milliarden mal Milliarden Jahren fertig werden, fast das gleiche Problem, und auch Turing-vollständige Sprachen lassen sich mit einem Schrittzähler zwangsweise abbrechen
  • Die Qualität einer Konfigurationssprache hängt stärker von Determinismus, klarer Semantik, Reinheit, Sicherheit und Sandboxing, Laufzeitkontrolle und Einfachheit ab als von der Frage, ob sie Turing-vollständig ist

Der zentrale Irrtum in Debatten über Turing-Vollständigkeit

  • Im Internet sprechen Programmierer in bestimmten Domänen oft davon, dass „nicht Turing-vollständig“ ein Vorteil oder sogar eine Anforderung sei
  • Turing-Vollständigkeit ist jedoch ein konkreter Begriff aus der Mathematik; verwendet man ihn als Stellvertreter für allerlei gewünschte Praxiseigenschaften, verwässert seine Bedeutung
  • Tatsächlich gebraucht werden Eigenschaften wie garantierte Terminierung, schnelle Ausführung, deterministisches Verhalten, Sandboxing oder eine einfache Konfigurationssprache, und diese stehen zur Turing-Vollständigkeit größtenteils orthogonal
  • Um diesen Unterschied zu verstehen, braucht man ein einfaches theoretisches Resultat zu primitiv rekursiven Funktionen (Primitive Recursive Functions, PRF)

Hinreichend schnelle Turing-Maschinen lassen sich in PRF umschreiben

  • Selbst wenn ein Programm in einer Turing-vollständigen Sprache geschrieben ist, kann derselbe Algorithmus auch in einer nicht Turing-vollständigen Sprache implementiert werden, sofern bekannt ist, dass seine Laufzeit schneller als O(2^(2^N)) ist
  • Die meisten praktischen Probleme liegen in einem Bereich, der schneller als 2^(2^N) endet
  • Deshalb beschränken nicht Turing-vollständige Sprachen die praktische Rechenfähigkeit nicht sinnvoll und verleihen auch nicht automatisch besondere Fähigkeiten zur Kontrolle von Berechnungen
  • Aus praktischer Sicht verursachen die folgenden beiden Programme faktisch dasselbe Problem
    • Ein Programm, das nicht terminiert
    • Ein Programm, das erst nach einer Schrittzahl wie einer Milliarde mal einer Milliarde terminiert
  • Auch in Turing-vollständigen Sprachen kann man das Nichtterminierungsproblem auf Implementierungsebene einfach verhindern, indem man Schritte zählt und nach einem festen Limit mit einem Fehler abbricht

FSM: terminiert immer, aber mit begrenzter Ausdruckskraft

  • Eine Finite State Machine (FSM) ist ein Erkenner, der einen String als Eingabe nimmt und „yes“ oder „no“ zurückgibt
  • Eine FSM besteht aus einer endlichen Zustandsmenge, einem Startzustand, einer Menge von Yes-Zuständen und einer Übergangsfunktion
  • Auf jedes Eingabesymbol wird die Übergangsfunktion wiederholt angewendet; das Ergebnis hängt dann davon ab, ob der Endzustand ein Yes-Zustand ist
  • Die Ausdruckskraft von FSM ist äquivalent zu regulären Ausdrücken (regular expression)
  • Eine FSM arbeitet linear in der Eingabelänge und terminiert immer, kann aber nicht jede Menge von Strings erkennen
    • Zum Beispiel kann sie die Menge von Strings wie 1, 010, 00100, 0001000 nicht erkennen, bei denen auf beiden Seiten der 1 gleich viele 0 stehen
    • Bei hinreichend langen Eingaben wiederholen sich Zustände, wodurch ein Zyklus entsteht; dupliziert man diesen Zyklusbereich, erreicht die FSM weiterhin einen Yes-Zustand, obwohl die Bedingung des Strings verletzt ist

Turing-Maschine: ein FSM-Modell mit veränderlichem Band

  • Eine Turing-Maschine (TM) besitzt wie eine FSM Zustände und eine Übergangsfunktion, arbeitet aber nicht auf unveränderlicher Eingabe, sondern auf einem veränderlichen Band
  • In jedem Schritt liest die TM das aktuelle Bandsymbol und führt dann Folgendes aus
    • Sie ersetzt das aktuelle Symbol durch ein neues Symbol
    • Sie ändert ihren internen Zustand
    • Sie bewegt den Kopf um ein Feld nach links oder rechts
  • Erreicht die TM einen Halt-Zustand, stoppt sie, und der Bandinhalt zu diesem Zeitpunkt ist das Ergebnis
  • Während eine FSM ein binärer Erkenner ist, ist die TM ein Gerät zur Berechnung von Funktionen
  • Eine TM muss nicht anhalten; sie kann über das Band laufen und Zustände ändern, ohne je einen Endzustand zu erreichen

Universal Turing Machine und Rechenfähigkeit

  • Das Programm einer TM wird nicht als Benutzereingabe in Form von Code gegeben, sondern ist in der Übergangsfunktion selbst fest verdrahtet
  • Man kann jedoch eine beliebige TM und ihre Eingabe als Textdatei kodieren und eine „Interpreter“-TM bauen, die diese Darstellung auswertet
  • Eine solche TM ist eine Universal Turing Machine und simuliert andere TMs, die ihr als Eingabe gegeben werden
  • Man kann einen TM-Interpreter in Python schreiben, und umgekehrt auch einen Python-Interpreter als TM implementieren; daher kann man beide hinsichtlich ihrer Rechenfähigkeit als gleichwertig ansehen
  • Eine FSM ist schwächer als eine TM
    • Eine TM kann eine FSM simulieren
    • Eine TM kann per Bandmanipulation entscheiden, ob ein String auf beiden Seiten gleich viele 0 und in der Mitte eine 1 hat
    • Eine FSM kann dasselbe Problem nicht lösen

Das Band lässt sich als zwei Stapel auffassen

  • Das Band einer TM ist eine Abstraktion, die sich in gewöhnlichen Programmiersprachen nicht besonders bequem direkt implementieren lässt
  • Band und Kopfposition lassen sich durch zwei Stapel darstellen
    • Der Inhalt links vom Kopf ist der linke Stapel
    • Der Inhalt rechts vom Kopf ist in umgekehrter Reihenfolge der rechte Stapel
  • Das Bewegen des Kopfes nach links oder rechts wird dadurch zu einem Pop auf dem einen und einem Push auf dem anderen Stapel
  • Damit ist eine TM rechnerisch äquivalent zu „einer FSM mit zwei Stapeln“
  • Wenn die Symbole des Stapels nur 0 und 1 sind, lässt sich der Stapel selbst sogar durch eine einzige natürliche Zahl darstellen
    • Top prüfen: stack % 2
    • pop: stack / 2
    • push x: stack * 2 + x

Grenzen der Turing-Maschine: Halteproblem und Resultate vom Rice-Typ

  • Da sich jede TM als Text kodieren lässt, kann man alle möglichen TMs in eine unendliche Liste bringen
  • Mit einem Diagonalisierungsargument lässt sich zeigen, dass es Funktionen gibt, die von keiner TM berechnet werden können
  • Ein konkreteres Beispiel ist das Halteproblem
    • Gegeben sind der Quellcode einer TM und eine Eingabe; gefragt ist, ob diese TM irgendwann anhält
  • Nimmt man an, dass halts(program, input) immer korrekt terminiert, entsteht mit einem weird-Programm, das seinen eigenen Quellcode als Eingabe erhält, ein Widerspruch
    • Wenn vorhergesagt wird, dass es anhält, läuft es in eine Endlosschleife und hält nicht an
    • Wenn vorhergesagt wird, dass es nicht anhält, beendet es sich sofort
  • Daher muss halts in manchen Fällen falsch liegen oder in manchen Fällen selbst nicht terminieren
  • Allgemeiner gilt: Für eine beliebige TM kann man nichttriviale, verhaltenserhaltende Eigenschaften nicht algorithmisch entscheiden
    • Syntaktische Eigenschaften sind prüfbar, aber Verhaltenseigenschaften, die auch nach Refactoring erhalten bleiben, sind im Allgemeinen nicht entscheidbar

Primitive rekursive Funktionen: ein Rechenmodell, das immer terminiert

  • Eine primitive rekursive Funktion (PRF) ist als Funktion definiert, die ein Tupel natürlicher Zahlen annimmt und eine natürliche Zahl zurückgibt
  • Die Grundfunktionen sind zero und succ
    • zero = 0
    • succ(x) = x + 1
  • Durch Funktionskomposition lassen sich Konstanten bilden
    • succ(zero) = 1
    • succ(succ(zero)) = 2
  • Allgemeine Rekursion ist nicht erlaubt, aber eine eingeschränkte Schleife mit vorab festgelegter Wiederholungszahl LOOP(init, f, n) ist zulässig
    • LOOP(init, f, 0) = init
    • LOOP(init, f, 1) = f(init)
    • LOOP(init, f, 2) = f(f(init))
  • Die zentrale Einschränkung ist, dass die Wiederholungszahl n vor dem Start der Schleife feststeht und der Schleifenzähler im Schleifenkörper nicht verändert werden kann

Grundlegende Programmierbausteine mit PRF aufbauen

  • Addition lässt sich als add(x, y) = LOOP(x, succ, y) definieren
  • Multiplikation lässt sich als mul(x, y) = LOOP(0, add x, y) definieren
  • Potenzierung lässt sich als pow(x, y) = LOOP(1, mul x, y) definieren
  • Damit lassen sich auch schnell wachsende Funktionen konstruieren
    • pow_2(n) = pow(2, n)
    • pow_2_2(n) = pow_2(pow_2(n))
  • Fügt man pred zu den Grundfunktionen hinzu, lassen sich saturierende Subtraktion und boolesche Operationen bilden
    • sub(x, y) = LOOP(x, pred, y)
    • and(x, y) = mul(x, y)
    • not(x) = sub(1, x)
    • Auch if(cond, a, b) lässt sich als arithmetischer Ausdruck formulieren
  • Vergleichsoperatoren, Rest und Division lassen sich ebenfalls mit begrenzter Wiederholung und Bedingungen implementieren

Datenstrukturen in PRF und Simulation von TMs

  • Eine PRF kann mehrere Argumente annehmen, liefert aber nur eine natürliche Zahl zurück; Datenstrukturen müssen daher als natürliche Zahl kodiert werden
  • Ein Paar (a, b) kann als 2^a * 3^b dargestellt werden
  • Um die Bestandteile wieder zu extrahieren, sucht man den maximalen Exponenten einer bestimmten Primzahl
    • fst(p) ist der Exponent der größten Zweierpotenz, die p teilt
    • snd(p) ist der Exponent der größten Dreierpotenz, die p teilt
  • Nach demselben Prinzip lassen sich auch drei Werte (S, stack1, stack2) in eine einzige natürliche Zahl packen
  • Die Konfiguration einer TM kann durch die folgenden drei Elemente beschrieben werden
    • aktueller Zustand S
    • linker Band-Stapel
    • rechter Band-Stapel
  • Da sich Stapeloperationen mit Rest, Multiplikation und Division implementieren lassen, kann man auch einen einzelnen Schritt einer TM als PRF kodieren
  • Mit LOOP(initial_config, single_step, n) lässt sich eine TM exakt n Schritte lang simulieren
  • Das Problem ist, dass man ein hinreichendes n normalerweise nicht kennt; ist die Laufzeit jedoch durch irgendeine PRF beschränkt, kann man genau so oft iterieren
  • Am Ende gilt also: TM-Berechnungen, deren Laufzeit durch eine primitive rekursive Funktion beschränkt ist, lassen sich durch PRF ersetzen

Grenzen von PRF: immer terminierend, aber nicht so stark wie TM

  • PRF terminieren immer, können aber nicht alle terminierenden Funktionen ausdrücken
  • Es gibt Funktionen, die von einer TM berechnet werden können, aber nicht durch PRF
  • Um das zu zeigen, setzt man eine Obergrenze für die Wachstumsrate anhand der Tiefe des PRF-Syntaxbaums
  • Für PRF mit Tiefe höchstens d lässt sich eine Schranke angeben, sodass sie nicht schneller wachsen können als eine bestimmte unäre Funktion A_d
  • A(d, x) ist wie folgt definiert
    • A(1, x) = x + 1
    • A(d + 1, 0) = A(d, A(d, 0))
    • A(d + 1, x) = A(d, A(d + 1, x - 1))
  • Diese Definition terminiert bei Berechnung auf einer TM, weil sich bei jedem Rekursionsaufruf (d, x) lexikographisch verkleinert
  • a(x) = A(x, x) wächst schneller als jede PRF; sie ist auf einer TM berechenbar, aber nicht als PRF ausdrückbar

Zurück zur Praxis: Nicht-Turing-Vollständigkeit allein reicht nicht

  • Eine Turing-Maschine kann möglicherweise nie anhalten
  • Auch Modelle wie FSM und PRF, die immer terminieren, garantieren nicht automatisch kurze Laufzeiten
  • PRF kann große Funktionen wie 2^(2^N) berechnen; eine Terminierungsgarantie allein garantiert also keine praktikable Ausführungszeit
  • Viele reale Algorithmen haben eine durch PRF beschränkte Laufzeit und lassen sich deshalb auch in nicht Turing-vollständigen Modellen ausdrücken
  • Eine allgemeine Methode, Turing-vollständige Berechnungen PRF-artig zu machen, besteht darin, einen Wiederholungszähler hinzuzufügen und bei zu großem Zählerstand zwangsweise abzubrechen

Welche Eigenschaften Konfigurationssprachen tatsächlich brauchen

  • Häufig wird bei Konfigurationssprachen „nicht Turing-vollständig“ als Designziel genannt, tatsächlich braucht man aber mehrere stärkere Eigenschaften

  • Determinismus

    • Eine Konfigurationssprache sollte deterministisch sein
    • Verhalten wie bei id([]) in Python, das je nach Ausführung unterschiedliche Werte liefert, mag in allgemeiner Programmierung akzeptabel sein, ist für Konfiguration aber ungeeignet
    • Konfigurationen dienen oft als Schlüssel für inkrementelle Builds oder Caching-Systeme; Nichtdeterminismus bringt dann das Cache-Verhalten durcheinander

  • Klare Semantik

    • Das Verhalten der Sprache sollte durch eine referenzierbare Norm eindeutig festgelegt sein
    • Man könnte id([]) in Python deterministisch machen, indem man ASLR deaktiviert und einen bestimmten Allocator verwendet, aber damit wäre das Ergebnis noch nicht vorhersagbar oder zwischen Implementierungen konsistent
    • Soll dasselbe Verhalten auch über verschiedene Implementierungen oder Python-Versionen hinweg garantiert sein, braucht es eine klare Semantik

  • Reinheit

    • Wenn Konfigurationen Umgebungsvariablen oder Dateien auf der Festplatte lesen können, hängt ihre Bedeutung von der Auswertungsumgebung ab
    • Damit Caching korrekt funktioniert, sollte die Konfigurationssprache rein sein

  • Sicherheit und Sandboxing

    • Sowohl Reinheit als auch Sicherheit lassen sich erreichen, indem man allgemeines IO nicht freigibt
    • Beide Eigenschaften verfolgen jedoch unterschiedliche Ziele
    • Reinheit soll verhindern, dass Ergebnisse nichtdeterministisch werden
    • Sicherheit soll verhindern, dass Angreifer Zugriff auf Ressourcen wie Zugriffstoken erhalten

  • Laufzeitkontrolle

    • Auch wenn IO kontrolliert wird, kann bösartige Konfiguration immer noch eine Denial-of-Service-Attacke verursachen und CPU verbrennen
    • Um Laufzeit zu garantieren, gibt es zwei Ansätze
    • Man beschränkt die Sprache so, dass Verarbeitung offensichtlich linear zur Eingabegröße bleibt
    • Oder man nutzt metered execution, bei der bei jedem atomaren Schritt ein Zähler dekrementiert wird und die Ausführung stoppt, sobald der Zähler 0 erreicht

  • Einfachheit

    • Eine Konfigurationssprache sollte Benutzer zu einfachen Programmen anleiten
    • Das Verbot von Rekursion und Endlosschleifen kann als Bremsschwelle dienen, die Einfachheit fördert
    • Wie das PRF-Beispiel zeigt, verhindert ein solches Verbot aber nicht vollständig das Schreiben beliebiger rekursiver Programme; es erzwingt nur umständlichere Umgehungen
    • Ein verwandtes Beispiel ist some roundabout code

Schlussfolgerung

  • Ein Turing-Maschinen-Algorithmus, dessen Laufzeit auf der Eingabe durch irgendeine primitive rekursive Funktion beschränkt ist, lässt sich auch als primitive rekursive Funktion implementieren
  • Nicht-Turing-Vollständigkeit kann die eine Eigenschaft garantierter Terminierung liefern, garantiert aber weder automatisch sinnvolle Laufzeitgrenzen noch die Qualität einer Konfigurationssprache in der Praxis
  • Für das Design von Konfigurationssprachen sind Determinismus, klare Semantik, Reinheit, Sandboxing, Laufzeitmessung und Einfachheit wichtiger als Turing-Vollständigkeit selbst

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-08-05
Kommentare auf Hacker News

  • Eigenwerbung: https://www.nayuki.io/page/primitive-recursive-functions

    • Deutlich besser als der Originalartikel, aber heutzutage scheinen alle eher ELI5-artige einfache Erklärungen zu bevorzugen

  • Im Fazit des Artikels gibt es ziemlich gute Kriterien in Bezug auf Konfigurationssprachen; ich frage mich, ob es unter den aktuellen Sprachen welche gibt, die alle oder die meisten davon erfüllen

    • Beispiele, die diese Kriterien erfüllen, sind Dhall [1] und Cue [2], aber in gewisser Weise sind das keine interessanten Beispiele
      Dhall ist absichtlich eine totale funktionale Sprache und geht daher in Richtung „nicht Turing-vollständig“, und Cue hat keine Funktionen, also gibt es auch nichts, das rekursiv sein könnte
      RCL [3] würde ich als kriterientreu ansehen. Es ist deterministisch und rein, bietet gemessene Ausführung und behandelt Dateisystemzugriffe in einer Sandbox. Wenn die Sandbox-Policy es erlaubt, kann es Dateien lesen, aber solche Dateien gelten als Teil des Quellcodes und verhalten sich genauso wie ein Import
      Bei RCL wollten wir aus den vom Autor genannten Gründen nicht in Richtung „nicht Turing-vollständig“ gehen. Die Tatsache, dass ein Programm letztlich terminiert, ist in der Praxis keine besonders nützliche Eigenschaft; umgekehrt kann man selbst in totalen funktionalen Sprachen wie Agda sehr komplexe Programme schreiben, sodass Nicht-Turing-Vollständigkeit keine einfachen Programme/Konfigurationen garantiert
      In RCL sind alle Schleifen begrenzt, aber weil es Funktionen gibt, ist auch Rekursion möglich. Tail Calls gibt es nicht, daher hatten wir anfangs eine Begrenzung der Rekursionstiefe eingebaut, um native Stack Overflows zu verhindern; der Fuzzer fand jedoch eine Funktion, die mit konstantem Stack-Speicher läuft und trotzdem nicht anhält, und ich verstehe sie immer noch nicht vollständig: let f = g => g(g(h => k => g(g(h)))); f(f)
      Letztlich ist es in der Praxis kein Problem, dass sich solche pathologischen Funktionen ausdrücken lassen. Man setzt einfach eine Begrenzung der Ausführungsschritte, also ein „Gas Limit“, oder die vom Autor genannte „gemessene Ausführung“. Dass die eingebauten Iterationskonstrukte begrenzt sind und Rekursion unbequem ist, ist ein guter Lenkungsmechanismus, um Code einfach zu halten; am Ende sind die wertvollsten Werkzeuge aber Code Reviews und gutes Urteilsvermögen
      [1]: https://dhall-lang.org/
      [2]: https://cuelang.org/
      [3]: https://rcl-lang.org/
    • Obwohl es imperativ und auch nicht „rein“ ist, wurde sogar C in eine Richtung entworfen, in der man vor Eintritt in jede Schleife eine obere Grenze für die Anzahl der Iterationen kennen können sollte, und ist daher primitiv rekursiv
      Dennis Ritchies Forschung am MIT konzentrierte sich auf ein Thema, das er Loop Programming nannte
      The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
      https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
      Strukturierte Programmierung, der fast alle modernen Programmierer standardmäßig folgen, ist im Grunde ein Paradigma, das einen in Richtung primitiver rekursiver Funktionen drängt. Weil strukturierte Programmierung im Vergleich zu den beiden anderen Typen wie pop und funktional nahezu universell akzeptiert wurde, scheint Dijkstras Aufsatz „goto considered harmful“ oft missverstanden zu werden
      Primitive rekursive Funktionen umfassen zwar nicht alle berechenbaren Funktionen, aber fast alle intuitiven Funktionen, deren Terminierung garantiert ist. Natürlich gibt es Fälle, in denen man tatsächlich Schleifen braucht, bei denen man beim Eintritt in die Schleife die Anzahl der Iterationen nicht kennt; aber wenn man sie nur dann verwendet, wenn sie wirklich nötig sind, sind sie ein vermeidbarer Fußschuss
      Sogar COBOL wurde modernisiert, indem unbegrenztes goto in die ALTER-Anweisung verschoben wurde. Mir fällt keine moderne, nützliche Sprache ein, die PR-Funktionen nicht erlaubt
      Auch in C kann man, wenn man while vermeidet und Fall-through explizit vermeidet, fast immer totalen Funktionscode schreiben, der sicher terminiert
      Es gibt auch pathologische Fälle wie die Typinferenz von ML. Sie ist gemessen an ihrer Komplexitätsklasse in der Praxis deutlich billiger, sodass es sich lohnt, sie in Kauf zu nehmen, auch wenn es der Sprache schwerfällt, eine solche Nutzung zu beschränken, ohne total funktional zu sein
      Praktisch gesehen bieten alle Sprachen im Großen und Ganzen Defaults, die die meisten dieser Kriterien unterstützen; Einschränkungen, die sie erzwingen, würden die Nützlichkeit einer Sprache jedoch stark begrenzen. Selbst die vielgescholtenen SOLID- und Clean-Frameworks drängen meiner Ansicht nach in Richtung dieses Modells
      Strukturierte Programmierung ist so allgegenwärtig geworden, dass man diesen Punkt leicht vergisst und ihn manchmal nicht einmal mehr lehrt. Aus Sicht eines alten bärtigen Kerls erinnere ich mich daran, die Gefahren von WHILE und Ähnlichem gelernt zu haben
    • Man könnte Dhall nehmen und prüfen, an welchen Kriterien es scheitert. Es scheint am nächsten dran zu sein

  • Die Aussage, dass es schneller läuft als O(2^(2^N)), war vermutlich als Vereinfachung gemeint, aber der Teil mit der „sehr großen Zahl“ mindert die Glaubwürdigkeit ein wenig
    Genauer müsste man wohl von einer „sehr schnell wachsenden Funktion“ sprechen. Oder es klingt so, als sei gemeint, dass das Programm in weniger als O(2^(2^N)) Schritten endet

  • Wenn man nur den ersten Teil betrachtet, dass eine eingeschränkte Sprache für manche Anwendungen besser ist, scheint mir der Vorteil darin zu liegen, dass man die Obergrenze der benötigten Anzahl von Schritten statisch berechnen kann.
    Dann könnte man für jede Eingabe Berechnungen ablehnen, die die Grenze verletzen, und einen sinnvollen Fehler zurückgeben.
    Bei einer turing-vollständigen Sprache mit Laufzeitlimit kann man das Limit dagegen für manche interessanten Eingaben zu niedrig ansetzen. Das weiß man erst, wenn man es ausführt und ins Limit läuft. Bei C++-Template-Rekursion sieht man so etwas gelegentlich.
    Vielleicht bin ich auch völlig auf dem Holzweg; wäre gut, wenn jemand mit mehr Ahnung das erklären könnte.

    • Ein früherer Kollege hatte einmal einen Wert von fast dem Dreifachen angesetzt, und nachdem ein paar Jahre später die reale Arbeitslast in dieses Limit lief, verwende ich nun ein 10-faches Limit einer vernünftigen Rechenmenge.
      Selbst wenn ein schlechter Workflow ein paarmal länger braucht, bis er fehlschlägt, reden wir immer noch von Millisekunden, also sehe ich darin keinen großen Schaden.
      Normalerweise stößt man auf dieses Problem, wenn jemand den Problembereich als gerichteten azyklischen Graphen behandelt, aber das „azyklisch“ nicht erzwingen konnte. Ein Problem als gerichteten azyklischen Graphen zu modellieren ist wie Dark Galadriel, die überlegt, ob sie den Ring von Frodo annimmt. „Alle werden mich lieben und verzweifeln.“ Leute, die so etwas bauen, sind immer viel stolzer darauf, als sie es verdient hätten.
      Am Ende geht den Kunden, die in teure und komplexe Lösungen hineingezogen wurden, das Geld aus, und ihr eigenes Problem beginnt ihnen viel kleiner vorzukommen. Dann bleibt buchstäblich nur eine App übrig, deren Kosten pro Aufgabe nicht weit genug gesenkt werden können, um das Geschäft des Kunden am Leben zu halten.
    • Den Fuel-Verbrauch von Blockchain-Berechnungen exakt vorherzusagen mag für andere interessant sein, für mich aber nicht.
      Mich interessiert eher, es als einen weiteren Hammer im Werkzeugkasten zu verwenden, um Bugs zu finden, die an den vorherigen Hämmern wie statischer Typprüfung, keinem null und keiner Veränderlichkeit vorbeigekommen sind.
      Die Tatsache, dass etwas in endlicher Zeit terminiert, beweist nicht seine Korrektheit; aber wenn ich erkläre, dass mein Code in endlicher Zeit terminiert, und der Compiler nicht zustimmt, dann werde ich glauben, dass dieser Code falsch ist.
    • Eine statisch bestimmte Obergrenze kann die tatsächliche Laufzeitkomplexität im häufigen Fall stark überschätzen. Denn im Allgemeinen lässt sich nicht vorhersagen, wie Bedingungen ausgewertet werden, die bei Rekursion zu einem frühen Abbruch führen.
      Damit ein früher Abbruch die Laufzeit beeinflusst, muss man Lazy Evaluation oder kurzschließende Bedingungen annehmen; eine praktische Sprache wird so etwas aber normalerweise haben.
    • Was, wenn diese Obergrenze extrem locker ist? Deterministisches Quicksort ist zum Beispiel normalerweise n log n, hat aber in Bezug auf die Eingabegröße eine quadratische Obergrenze.
      Würde man dann Quicksort-Berechnungen ablehnen? Noch extremer: Der Hindley-Milner-Algorithmus hat eine exponentielle Zeitobergrenze, läuft in der Praxis aber oft in linearer Zeit.
    • Ich weiß nicht, ob sie „statisch berechnet“ wird, aber der einzige Vorteil einer stark eingeschränkten Sprachmächtigkeit besteht meiner Ansicht nach darin, eine Berechnungsgrenze setzen zu können, die nicht von den Daten abhängt.
      Allerdings fällt mir keine einzige Situation ein, in der das wirklich eine harte Anforderung wäre. Wie viele Systeme gibt es, die keinen Fehler „Die Abfrage hat zu lange gedauert“ ausgeben können?

  • Ich wollte einmal eine Backend-Web-Programmiersprache ausprobieren, die auf dem Prinzip terminiert nicht / ist beschränkt basiert.
    Die Idee war, dass der Compiler für jede Funktion nachweist, dass ihre Ausführung für einen gegebenen Zustand und gegebene Argumente innerhalb von Grenzen liegt, und zeigen kann, dass X die Untergrenze und Y die Obergrenze ist. Diese Information wird bis zu den Einstiegspunkten weitergereicht.
    Ich stimme dem Autor zu, dass stärkere Semantik nötig ist, und deshalb habe ich über diese Sprache nachgedacht. Oft will man Garantien über die Laufzeit eines Programms.
    Im Kern würde sie auf primitiv rekursiven Funktionen basieren, könnte in der Praxis aber turing-vollständig sein. So wie Rust fehlerhafte Borrows ablehnt, aber für rohe Pointer unsafe bereitstellt, würde diese Sprache auf einfachen primitiven Iterationsfunktionen die Obergrenze berechnen oder einen unsafe-Operator verwenden und eine alternative Formel für die Grenzen bereitstellen.

  • Der kurze Beschwerde-/Motivationsteil des Artikels ist für mich nicht gut nachvollziehbar.
    Gemeint ist die Stelle: „Normalerweise wird in bestimmten Bereichen die Tatsache, nicht turing-vollständig zu sein, als Vorteil oder Anforderung gepriesen. Ich halte die meisten dieser Diskussionen für fehlgeleitet — nicht turing-vollständig zu sein bedeutet nicht das, was die Leute erwarten.“
    Warum sollen solche Diskussionen fehlgeleitet sein? Die meisten Werkzeuge für formale Analyse, etwa Coq, Isabelle und Agda, verlangen üblicherweise einen Beweis dafür, dass eine Funktion terminiert. Das ist doch gleichbedeutend mit dem Beweis, dass die Funktion total ist, und bedeutet damit, dass sie primitiv rekursiv ist, oder nicht?

    • Ich habe nicht bis zum Ende gelesen, aber dieser Artikel scheint daher zu kommen, dass einige Konfigurationssprachen „nicht turing-vollständig“ als Feature anpreisen. Was sie eigentlich bewerben wollen, ist wohl eine vernünftig begrenzte Laufzeit.
      Das kam auch kürzlich in einer Diskussion zu CEL auf:
      https://news.ycombinator.com/item?id=40954652
    • Wenn es um formale Beweise geht: Im allgemeinen Fall zu beweisen, dass eine Funktion total ist, ist kein wissenschaftliches Gegenbeispiel aus moderner Programmierung, sondern ein NP-vollständiges Suchproblem.
      Wenn ich mich richtig erinnere, entspricht das NP mit einem co-NP-Orakel oder der zweiten Ebene der polynomiellen Hierarchie. Selbst wenn es bei kleinen Problemen möglich ist, ist es teuer.
      Solche Werkzeuge funktionieren am besten, wenn man Programme so strukturiert, dass sie total werden. In der strukturierten Programmierung ist die häufigste Methode dafür, nur FOR zu verwenden oder WHILE/Rekursion auf eine begrenzte Anzahl von Iterationen zu beschränken.
      Auch wenn es nur mit SAT zu tun hat: Die handhabbaren Formen aus Schaefers Dichotomiesatz sind die zugänglichste Perspektive, die mir dazu einfällt.
    • Wie der Artikel zeigt, gibt es terminierende Funktionen, die nicht primitiv rekursiv sind; daher bedeutet ein Beweis der Totalität nicht, dass etwas primitiv rekursiv ist.
      Agda und vermutlich auch andere Werkzeuge können für manche terminierenden, nicht primitiv rekursiven Funktionen die Terminierung beweisen. Natürlich nicht für alle.
      Das Missverständnis, über das sich der Artikel beschwert, scheint ungefähr dieses zu sein: „Turing-Vollständigkeit bedeutet, dass man Berechnungen durchführen kann, und Nicht-Turing-Vollständigkeit bedeutet, dass man keine Berechnungen durchführen kann und gute Eigenschaften für Konfigurationssprachen erhält.“
      Der Punkt des Artikels ist, dass man auch ohne Turing-Vollständigkeit viele rechenintensive oder schwierige Dinge tun kann und dass eine Konfigurationssprache deutlich strengere Beschränkungen braucht als bloß Nicht-Turing-Vollständigkeit.
    • Es kann außer totalen Funktionen, die sauber terminieren, noch andere Wege geben, nicht turing-vollständig zu werden. Eine Endlosschleife zum Beispiel kann weder universell berechnen noch terminieren.

  • Ich bin CUE-Entwickler. CUE ist primitiv-rekursiv und erfüllt auch die Kriterien, die man sich von einer „guten“ Konfigurationssprache wünscht.