Es ist nicht möglich, dass linear begrenzte Automaten prüfen, ob C ++ - Programme vorhanden sind, und es ist unwahrscheinlich, dass LBA prüfen kann, ob SML-Programme korrekt geschrieben sind. C ++ verfügt über ein Turing-complete-Typensystem, da Sie beliebige Programme als Template-Metaprogramme codieren können.
SML ist interessanter. Es gibt eine entscheidende Typprüfung, aber das Problem ist EXPTIME-vollständig. Daher ist es unwahrscheinlich, dass ein LBA dies überprüfen kann, es sei denn, die Komplexitätshierarchie ist sehr überraschend zusammengebrochen. Der Grund dafür ist, dass SML eine Typinferenz erfordert und es Programmfamilien gibt, deren Typ viel schneller wächst als die Größe des Programms. Betrachten Sie als Beispiel das folgende Programm:
fun delta x = (x, x) (* this has type 'a -> ('a * 'a), so its return value
has a type double the size of its argument *)
fun f1 x = delta (delta x) (* Now we use functions to iterate this process *)
fun f2 x = f1 (f1 x)
fun f3 x = f2 (f2 x) (* This function has a HUGE type *)
Für einfachere Typsysteme wie C oder Pascal glaube ich, dass es einem LBA möglich ist, dies zu überprüfen.
In den Anfängen der Programmiersprachenforschung verwendeten die Leute manchmal Van-Wingaarden-Grammatiken (auch bekannt als zweistufige Grammatiken), um Typsysteme für Programmiersprachen zu spezifizieren. Ich glaube, Algol 68 wurde auf diese Weise spezifiziert. Mir wurde jedoch gesagt, dass diese Technik aus im Wesentlichen pragmatischen Gründen aufgegeben wurde: Es stellte sich heraus, dass es für die Leute ziemlich schwierig war, Grammatiken zu schreiben, die genau angaben, was sie für spezifiziert hielten! (In der Regel haben die Grammatiken, die die Leute geschrieben haben, größere Sprachen erzeugt, als sie beabsichtigt hatten.)
Heutzutage verwenden die Leute schematische Inferenzregeln, um Typsysteme zu spezifizieren. Dies ist im Wesentlichen eine Möglichkeit, Prädikate als den am wenigsten festgelegten Punkt einer Sammlung von Horn-Klauseln zu spezifizieren. Die Befriedigung von Horn-Theorien erster Ordnung ist im Allgemeinen unentscheidbar. Wenn Sie also alles erfassen möchten, was Typentheoretiker tun, ist der von Ihnen gewählte grammatikalische Formalismus strenger als wirklich zweckmäßig.
Ich weiß, dass einige Arbeiten an der Verwendung von Attributgrammatiken zur Implementierung von Typsystemen durchgeführt wurden. Sie behaupten, dass diese Wahl einige Vorteile für das Software-Engineering mit sich bringt: Attributgrammatiken kontrollieren den Informationsfluss sehr genau, und mir wird gesagt, dass dies das Programmverständnis erleichtert.
