Wie kann gezeigt werden, dass ein Typ in einem System mit abhängigen Typen nicht bewohnt ist (dh die Formel ist nicht nachweisbar)?

Für Systeme ohne abhängige Typen, wie das Hindley-Milner-Typensystem, entsprechen die Typen Formeln der intuitionistischen Logik. Dort wissen wir, dass es sich bei den Modellen um Heyting-Algebren handelt. Um eine Formel zu widerlegen, können wir uns auf eine Heyting-Algebra beschränken, bei der jede Formel durch eine offene Teilmenge von .$\mathbb{R}$

Zum Beispiel, wenn wir zeigen wollen, dass ist nicht besiedelt, wir konstruieren ein Mapping von Formeln zu offenen Teilmengen von indem wir definieren: Dann Dies zeigt, dass die ursprüngliche Formel nicht beweisbar sein kann, da wir ein Modell haben, bei dem es nicht wahr ist, oder der Typ (gemäß Curry-Howard-Isomorphismus) nicht bewohnt werden kann.$\forall\alpha.\alpha\lor(\alpha\rightarrow\bot)$$\phi$$\mathbb{R}$

Eine andere Möglichkeit wäre die Verwendung von Kriepke-Rahmen .

Gibt es ähnliche Methoden für Systeme mit abhängigen Typen? Wie eine Verallgemeinerung von Heyting-Algebren oder Kripke-Frames?

Hinweis: Ich bitte nicht um ein Entscheidungsverfahren, ich weiß, dass es keines geben kann. Ich bitte nur um einen Mechanismus, der es erlaubt, die Unbeweisbarkeit einer Formel zu bezeugen - um jemanden davon zu überzeugen, dass sie unbeweisbar ist.

Dass eine Formel nicht beweisbar ist, kann im Wesentlichen auf zwei Arten geschehen. Mit etwas Glück können wir in der Typentheorie zeigen, dass die Formel eine impliziert, von der bereits bekannt ist, dass sie nicht beweisbar ist. Die andere Möglichkeit besteht darin, ein Modell zu finden, in dem die Formel ungültig ist. Dies kann sehr schwierig sein. Es hat zum Beispiel sehr lange gedauert , das gruppenoidale Modell der abhängigen Typentheorie zu finden, das als erstes die Eindeutigkeit von Identitätsnachweisen für ungültig erklärt hat .

Die Frage "Was ist ein Modell der abhängigen Typentheorie?" hat eine etwas komplizierte Antwort. Wenn Sie bestimmte Substitutionseigenschaften ignorieren, ist ein Modell eine lokal kartesisch geschlossene Kategorie. Dies ist möglicherweise die einfachste Antwort. Wenn Sie ein "reales" Modell möchten, gibt es mehrere Optionen. Weitere Informationen finden Sie auf der Seite nLab über kategoriale Modelle der Theorie abhängiger Typen . In jedem Fall ist die Antwort etwas kompliziert, da die Theorie der abhängigen Typen ein ziemlich komplexes formales System ist.

Wenn ich nur einen Artikel zu diesem Thema vorschlagen würde, würde ich wahrscheinlich das Originalpapier von Robert Seely empfehlen: "Lokal kartesische geschlossene Kategorien und Typentheorie" . Wenn ich einen anderen vorschlagen würde, wäre es wahrscheinlich einer, der erklärt, was in Seelys Aufsatz korrigiert werden muss, z. B. Martin Hoffmans "Über die Interpretation der Typentheorie in lokal kartesischen geschlossenen Kategorien" .

Ein neuer wichtiger Fortschritt auf diesem Gebiet ist die Erkenntnis, dass homotopietheoretische Modelle auch Modelle der abhängigen Typentheorie sind, siehe homotopytypetheory.org Referenzen . Dies bietet eine Fülle von Möglichkeiten, aber man muss jetzt die Homotopietheorie erlernen, um an die Modelle heranzukommen.