Was macht die Typinferenz für abhängige Typen unentscheidbar?

Ich habe gesehen, dass abhängige Typsysteme nicht ableitbar, sondern überprüfbar sind. Ich habe mich gefragt, ob es eine einfache Erklärung dafür gibt, warum das so ist, und ob es eine Grenze der "Abhängigkeit" gibt, in der Typen durch Werte indiziert werden können, unterhalb derer eine Typinferenz möglich ist und oberhalb derer keine?

Für eine relativ einfache Version der Theorie abhängiger Typen gab Gilles Dowek einen Beweis für die Unentscheidbarkeit der Typisierbarkeit in einem nicht leeren Kontext:

Gilles Dowek, Die Unentscheidbarkeit der Typisierbarkeit im Kalkül$\lambda\Pi$

Welches finden Sie hier .

Lassen Sie mich zunächst klären, was in dieser Arbeit bewiesen ist: Er zeigt, dass es in einer abhängigen Rechnung ohne Anmerkungen zu den Abstraktionen unentscheidbar ist, die Typisierbarkeit eines Begriffs in einem nicht leeren Kontext zu zeigen . Beide Hypothesen sind notwendig: Im leeren Kontext reduziert sich die Typisierbarkeit auf die des einfach typisierten Kalküls (entscheidbar von Hindley-Milner), und bei den Anmerkungen zu den Abstraktionen gilt der übliche typgesteuerte Algorithmus.$\lambda$

Die Idee ist, ein Post-Korrespondenz-Problem als Typkonvertierungsproblem zu kodieren und dann sorgfältig einen Begriff zu konstruieren, der typisierbar ist, wenn die beiden spezifischen Typen konvertierbar sind. Dies nutzt die Kenntnis der Form normaler Formen, die immer in diesem Kalkül existieren. Der Artikel ist kurz und gut geschrieben, daher werde ich hier nicht näher darauf eingehen.

In polymorphen Kalkülen wie System-F wäre es nun schön, auf die Typabstraktionen und -anwendungen schließen zu können und die Anmerkungen zu s wie oben wegzulassen . Dies ist auch nicht zu entscheiden, aber der Beweis ist viel schwieriger und die Frage war für einige Zeit offen. Die Angelegenheit wurde von Wells gelöst:$\lambda$

JB Wells, Typisierbarkeit und Typprüfung in System F sind gleichwertig und unentscheidbar .

Dies kann hier gefunden werden . Alles, was ich darüber weiß, ist, dass es das Problem der Halb-Vereinheitlichung (die Unification-Modulo-Instanziierung von universellen Quantifizierern und unentscheidbar ist) auf die Typprüfung in System F reduziert.

Schließlich ist es ziemlich einfach zu zeigen, dass die Besiedlung abhängiger Familien unentscheidbar ist: Codieren Sie einfach ein Post-Problem in die Konstruktorindizes. Hier sind einige Folien von Nicolas Oury, die das Argument skizzieren.

Ob es eine "Grenze" gibt, hängt stark davon ab, was Sie mit Ihren abhängigen Typen zu tun versuchen, und es gibt viele Näherungswerte, die versuchen, entweder entscheidbar oder zumindest nahe genug zu sein, um verwendbar zu sein. Diese Fragen sind jedoch nach wie vor ein wesentlicher Bestandteil der aktiven Forschung.

Ein möglicher Weg ist das Feld "Verfeinerungstypen", in dem die Ausdruckssprache von Typabhängigkeiten eingeschränkt ist, um eine entscheidbare Überprüfung zu ermöglichen, siehe z . B. Flüssigkeitstypen . Es ist jedoch selten, dass eine vollständige Typinferenz selbst in diesen Systemen entscheidbar ist.