Prooftechniken im Zusammenhang mit der Curry-Howard-Korrespondenz

Ich suche nach Quellen zum formalisierten Begriff von Programmen. Dies scheint eng mit der Curry-Howard-Korrespondenz verbunden zu sein, aber man könnte dies auch auf Universal Turing Machines und seine Fähigkeit zurückführen, die Beschreibung und Eingabe eines TM zu lesen.

Wenn ich über Curry-Howard-Korrespondenz lese, habe ich das Gefühl, dass die Ursprünglichkeit von UTMs der Forschung an Programmen schaden kann, mit der einzigartigen Schlussfolgerung, dass jedes Programm auf Symbole, Zustände und Regeln reduziert werden kann. Gibt es den umgekehrten Ansatz, bei dem übergeordnete Rechensysteme definiert und untersucht werden? Was sind gute Ressourcen daran?

Was Sie wollen, existiert und ist ein enormes Forschungsgebiet: Es ist die gesamte Theorie der Programmiersprachen.

Sie können die Berechnung auf zwei Arten anzeigen. Sie können an Maschinen denken , oder Sie können an Sprachen denken .

Eine Maschine ist im Grunde eine Art endliche Kontrolle, die durch einen (möglicherweise unbegrenzten) Speicher erweitert wird. Aus diesem Grund wechseln einführende TOC-Klassen von endlichen Automaten zu Pushdown-Automaten zu Turing-Maschinen. Jede Klasse übernimmt eine endliche Kontrolle und fügt ihr etwas mehr Speicher hinzu. (Heutzutage ist die endliche Kontrolle oft noch stärker eingeschränkt, wie bei Schaltungsmodellen.) Das Wesentliche ist, dass die endliche Kontrolle von vornherein auf einmal gegeben wird.

Eine Sprache ist eine Möglichkeit, eine ganze Familie von Steuerelementen kompositorisch zu spezifizieren. Sie haben primitive Formulare für grundlegende Steuerelemente und Operatoren zum Erstellen größerer Steuerelemente aus kleineren. Die ursprüngliche Sprache, der Lambda-Kalkül, spezifiziert tatsächlich nichts als Kontrolle - die einzigen Dinge, die Sie definieren können, sind Funktionsabstraktionen, Anwendungen und Variablenreferenzen.

$snm$

Forscher in Bezug auf Komplexität und Algorithmen betrachten Maschinen normalerweise als grundlegend, da sie an Kosten und Machbarkeitsergebnissen interessiert sind . Um ein bisschen zu übertreiben, ist die grundlegende Forschungsfrage, die sie haben:

Was ist die am wenigsten leistungsstarke Maschine, die eine bestimmte Art von Problem lösen kann ?

Sprachforscher betrachten Sprachen als grundlegend, weil wir an Ausdruckskraft und Unmöglichkeitsergebnissen interessiert sind . Mit einer ähnlichen Übertreibung lautet unsere grundlegende Forschungsfrage:

Was ist die ausdrucksstärkste Sprache, die eine bestimmte Art von schlechtem Verhalten ausschließt?

Beachten Sie nebenbei, wie die beiden Güter jeder Art von theoretischen Werten direkt in Konflikt stehen! Durch gute Arbeit mit Algorithmen und Komplexität können Sie ein schwierigeres Problem mit weniger Ressourcen lösen. Gute Arbeit in Sprachen ermöglicht es Programmierern, mehr Dinge zu tun und gleichzeitig mehr schlechtes Verhalten zu verbieten. (Dieser Konflikt ist im Grunde der Grund, warum Forschung schwierig ist.)

Nun fragen Sie sich vielleicht, warum mehr Theorie-A-Typen keine Sprachen verwenden oder warum mehr Theorie-B-Forscher keine Maschinen verwenden. Der Grund ergibt sich aus der Form der Grundlagenforschungsfrage.

Beachten Sie, dass die stilisierte Grundlagenforschungsfrage in Bezug auf Algorithmen / Komplexität eine Untergrenze ist. Sie möchten wissen, dass Sie die beste Lösung haben und dass es keinen Weg gibt, es besser zu machen, egal wie klug Sie sind. Eine Sprachdefinition legt die Mittel für die Programmzusammensetzung fest. Wenn Sie also nachweisen, dass eine Untergrenze mit einem Sprachmodell übereinstimmt, bleibt möglicherweise die Frage offen, ob es möglicherweise nicht möglich ist, bessere Ergebnisse zu erzielen, wenn Sie Ihre Sprache um einige erweitern neue Funktion. Mit einem Maschinenmodell haben Sie die gesamte Kontrolle auf einmal, sodass Sie von Anfang an alles wissen, was die Maschine möglicherweise kann.

Aber Maschinenspezifikationen sind genau das Falsche, um interessante Dinge über das Blockieren von schlechtem Verhalten zu sagen. Eine Maschine gibt Ihnen eine vollständige Kontrolle im Voraus, aber zu wissen, dass ein bestimmtes Programm in Ordnung oder schlecht ist, hilft Ihnen nicht, wenn Sie es erweitern oder als Unterprogramm verwenden möchten - wie Perlis 'Epigramm sagt: "Jedes Programm ist ein Teil eines anderen Programms und passt selten. " Da Sprachforscher daran interessiert sind, Dinge über ganze Klassen von Programmen zu sagen , sind Sprachen für den Zweck viel besser geeignet.