Was kann Idris nicht tun, indem es auf Vollständigkeit verzichtet?

Ich weiß, dass Idris abhängige Typen hat, aber nicht vollständig ist. Was kann es nicht tun, wenn es auf Vollständigkeit verzichtet, und hängt dies damit zusammen, dass es abhängige Typen gibt?

Ich denke, das ist eine ziemlich spezifische Frage, aber ich weiß nicht viel über abhängige Typen und verwandte Typsysteme.

Idris ist Turing Complete! Es prüft auf Vollständigkeit (Abbruch beim Programmieren mit Daten, Produktivität beim Programmieren mit Codaten), setzt jedoch nicht voraus, dass alles vollständig ist.

Interessanterweise reichen Daten und Codaten aus, um die Vollständigkeit von Turing zu modellieren, da Sie eine Monade für Teilfunktionen schreiben können. Ich habe das vor Jahren in Coq gemacht - es ist wahrscheinlich mittlerweile bitrot, aber hier ist es trotzdem: http://eb.host.cs.st-andrews.ac.uk/Partial/partial.v .

Sie brauchen eine Flucht, um solche Dinge tatsächlich auszuführen, aber Idris ermöglicht es Ihnen, dies zu tun.

Idris reduziert Teilfunktionen auf der Typebene nicht, um die Typprüfung entscheidbar zu machen. Auch können nur Gesamtprogramme als Beweise angesehen werden.

Ich gehe davon aus, dass Sie bereits von der Church-Turing-These gehört haben , wonach alles, was wir als „Berechnung“ bezeichnen, mit einer Turing-Maschine (oder einem der vielen anderen äquivalenten Modelle) durchgeführt werden kann. Eine Turing-vollständige Sprache ist also eine Sprache, in der jede Berechnung ausgedrückt werden kann. Umgekehrt ist eine Turing-unvollständige Sprache eine Sprache, in der es einige Berechnungen gibt, die nicht ausgedrückt werden können.

Ok, das war nicht sehr informativ. Lassen Sie mich ein Beispiel geben. In einer unvollständigen Turing-Sprache können Sie nichts tun: Sie können keinen Turing-Maschinensimulator schreiben (andernfalls könnten Sie eine Berechnung auf der simulierten Turing-Maschine codieren).

Ok, das war noch nicht sehr informativ. Die eigentliche Frage ist, welches nützliche Programm kann nicht in einer Turing-unvollständigen Sprache geschrieben werden? Nun, niemand hat sich eine Definition von „nützlichem Programm“ ausgedacht, die alle Programme enthält, die irgendwo für einen nützlichen Zweck geschrieben wurden, und die nicht alle Turing-Maschinenberechnungen enthält. Das Entwerfen einer Turing-unvollständigen Sprache, in der Sie alle nützlichen Programme schreiben können, ist daher immer noch ein sehr langfristiges Forschungsziel.

Nun gibt es einige sehr unterschiedliche Arten von Turing-unvollständigen Sprachen, und sie unterscheiden sich darin, was sie nicht können. Es gibt jedoch ein gemeinsames Thema: Turing-complete-Sprachen müssen eine Möglichkeit zum bedingten Beenden oder Fortfahren für eine Zeit enthalten, die nicht durch die Programmgröße begrenzt ist, und eine Möglichkeit, mit der das Programm eine von der Eingabe abhängige Speichermenge verwendet . Konkret bieten die meisten imperativen Programmiersprachen diese Fähigkeiten durch while-Schleifen bzw. dynamische Speicherzuweisung. Die meisten funktionalen Programmiersprachen bieten diese Fähigkeiten durch Rekursion und Verschachtelung von Datenstrukturen.

Idris ist stark von Agda inspiriert . Agda ist eine Sprache zum Beweisen von Theoremen . Jetzt Theoreme beweisen und Programme ausgeführt werden , sehr eng miteinander verbunden , so dass Sie Programme in Agda schreiben können wie Sie einen Satz beweisen. Intuitiv ist ein Beweis des Theorems „A impliziert B“ eine Funktion, die einen Beweis von Theorem A als Argument nimmt und einen Beweis von Theorem B zurückgibt.

Da es das Ziel des Systems ist, Theoreme zu beweisen, können Sie den Programmierer nicht beliebige Funktionen schreiben lassen. Stellen Sie sich vor, Sie könnten mit der Sprache eine blöde rekursive Funktion schreiben, die sich gerade selbst nannte:

oops : A -> B
oops x = oops x

Sie können sich von der Existenz einer solchen Funktion nicht überzeugen lassen, dass A B impliziert, sonst könnten Sie alles und nicht nur wahre Theoreme beweisen! Also verbietet Agda (und ähnliche Theorembeweiser) willkürliche Rekursionen. Wenn Sie eine rekursive Funktion schreiben, müssen Sie nachweisen, dass sie immer terminiert , sodass Sie immer dann, wenn Sie sie mit einem Beweis von Satz A ausführen, wissen, dass ein Beweis von Satz B erstellt wird.

Die unmittelbare praktische Einschränkung von Agda besteht darin, dass Sie keine willkürlichen rekursiven Funktionen schreiben können. Da das System in der Lage sein muss, alle nicht terminierenden Funktionen abzulehnen, stellt die Unentscheidbarkeit des Halteproblems (oder allgemeiner der Satz von Rice ) sicher, dass es auch terminierende Funktionen gibt, die abgelehnt werden. Eine weitere praktische Schwierigkeit besteht darin, dass Sie dem System helfen müssen, zu beweisen, dass Ihre Funktion beendet ist.

Es wird viel darüber geforscht, Proofsysteme programmiersprachenähnlicher zu machen, ohne die Garantie zu gefährden, dass A bei einer Funktion von A nach B einen mathematischen Beweis liefert, der B impliziert. Erweitern des Systems, um mehr zu akzeptieren das Beenden von Funktionen ist eines der Forschungsthemen. Andere Erweiterungsrichtungen umfassen die Bewältigung von Problemen der „realen Welt“ wie Ein- / Ausgabe und Parallelität. Eine weitere Herausforderung besteht darin, diese Systeme für bloße Sterbliche zugänglich zu machen (oder vielleicht bloße Sterbliche davon zu überzeugen, dass sie tatsächlich zugänglich sind).

Idris kenne ich nicht. Es ist eine Übernahme der Herausforderungen, die ich gerade erwähnt habe. Soweit ich von einem flüchtigen Blick auf verstehen 2013 Preprint , Idris ist Turing-vollständig, sondern enthält eine Gesamtheit checker. Die Gesamtheitsprüfung überprüft, ob jede mit dem Schlüsselwort " totalterminate" versehene Funktion beendet ist. Das Sprachfragment, das nur Idris-Programme enthält, in denen jede Funktion total ist, hat eine ähnliche Ausdruckskraft wie Arda (wahrscheinlich keine exakte Übereinstimmung aufgrund von Unterschieden in der Typentheorie, aber nahe genug, dass Sie es nicht bemerken würden, wenn Sie es nicht absichtlich versucht hätten).

Weitere Beispiele für Sprachen, die auf unterschiedliche Weise nicht vollständig sind, finden Sie unter Was sind die praktischen Einschränkungen einer nicht vollständigen Sprache wie Coq? (Dem ist diese Antwort weitgehend entnommen).