Im dritten Kapitel der CPDT wird kurz erläutert, warum negative induktive Typen in Coq verboten sind. Wenn wir
hätten %Vor%Dann könnten wir einfach eine Funktion definieren
%Vor%, so dass der Ausdruck uhoh (Abs uhoh) nicht terminierend wäre, mit dem "wir jeden Satz beweisen könnten".
Ich verstehe den Nicht-Beendigungsteil, aber ich verstehe nicht, wie wir damit etwas beweisen können. Wie würde man False mit term wie oben definiert beweisen?
Durch das Lesen Ihrer Frage wurde mir klar, dass ich Adams Argument auch nicht ganz verstanden habe. Aber Inkonsistenz in diesem Fall ergibt sich recht leicht aus Cantors üblichem diagonalem Argument (einer endlosen Quelle von Paradoxen und Rätseln in Logik). Berücksichtigen Sie die folgenden Annahmen:
%Vor% Dies ist eine generische Entwicklung, die mit dem in CPDT definierten term -Typ instanziiert werden könnte: T wäre term , x und y wären zwei Elemente von term , die wir testen können unterscheiden zwischen (zB App (Abs id) (Abs id) und Abs id ). Der entscheidende Punkt ist die letzte Annahme: Wir nehmen an, dass wir eine invertierbare Funktion g : (T -> T) -> T haben, die in Ihrem Beispiel Abs wäre. Mit dieser Funktion spielen wir den üblichen Diagonalisierungstrick: Wir definieren eine Funktion kaboom , die sich durch Konstruktion von jeder Funktion T -> T unterscheidet, einschließlich sich selbst. Daraus ergibt sich der Widerspruch.
Tags und Links coq infinite-loop non-termination