Logischer Rahmen gegen Typentheorie

Was ist der Unterschied zwischen logischem Rahmen und Typentheorie? Beide haben Typen, Begriffe und basieren auf abhängig typisierten Lambda-Berechnungen.

Wir haben Edinburg LF, das auf Lambda-Pi-Kalkül basiert, aber es scheint mir, dass es dort einen subtilen Unterschied gibt.

Zusammenfassung. Ein logischer Rahmen ist eine Metasprache für die Formalisierung deduktiver Systeme, in der Deduktionen zu syntaktischen Objekten werden.

Natürlich ist das, was als Metasprache zählt, ziemlich vage, und es ist hilfreich, die historische Entwicklung logischer Rahmenbedingungen zu verstehen. Der erste logische Rahmen war de Bruijns Automath (1), der auf -calculus basiert. Viele der Ideen aus der Automath-Sprachfamilie haben ihren Weg in moderne logische Rahmenbedingungen gefunden. Martin-Löfs Arbeit an konstruktiven Typentheorien, die ebenfalls auf -calculi basieren, war ebenfalls einflussreich.$\lambda$$\lambda$

Edinburghs LF (2) ist ein sehr einflussreicher logischer Rahmen. Edinburgh LF erhalten Sie, wenn Sie den einfach eingegebenen Kalkül mit Typabhängigkeit anreichern . Das ist alles. Um die Typabhängigkeit präzise zu machen, muss der Funktionsraumoperator für Typen durch Typabstraktion ersetzt werden, die normalerweise , und führen Sie die Art der Typen sowie die Art der Abstraktion ein. In Bezug auf Regeln befindet sich der Schlüssel in der Eliminierungsregel für bzw. :A → B Π x A . B A → B Π x A . $\lambda$$A \rightarrow B$$\Pi x^A. B$$A \rightarrow B$$\Pi x^A. B$

Links haben wir die Regel für den einfach eingegebenen Kalkül, rechts die Regel, die die linke Seite mit Typabhängigkeit verallgemeinert. Wir sehen, dass in der Schlussfolgerung rechts ein Wert in den Typ 'fließt'.$\lambda$

Ich denke, die interaktive Proof-Assistentin Isabelle verwendet eine intuitionistische Logik zweiter Ordnung, die auf -calculus basiert, ohne Zahlen oder rekursive Datentypen als logisches Framework. Verschiedene andere wurden vorgeschlagen.$\lambda$

Ein Vorteil der Verwendung von -calculi als logisches Framework besteht darin, dass Bindungskonstrukte wie universelle Quantifizierer mit dem Binder des Frameworks implementiert werden können. Beachten Sie, dass die meisten logischen Frameworks ausdrücklich schwach sind: Die Frameworks unterstützen das Denken auf Objektebene, reichen jedoch nicht aus, um viel metatheoretisches Denken durchzuführen, das über die Tatsache hinausgeht, dass eine bestimmte Anweisung auf Objektebene ein Theorem ist. Tatsächlich ist die Metalllogik normalerweise so schwach, dass es unmöglich ist, den Abzugssatz für eine Objektlogik im Hilbert-Stil zu beweisen. Natürlich hindert Sie nichts daran, leistungsfähigere Typentheorien als logischen Rahmen zu verwenden.$\lambda$$\lambda$

Aus diesen praktischen und historischen Gründen sind die meisten heute verwendeten logischen Rahmen typisierte -calculi, dh Typ-Theorien. In (3, 4) finden Sie ausführlichere Erläuterungen zu logischen Frameworks.$\lambda$

1. N. de Bruijn: Die mathematische Sprache AUTOMATH, ihre Verwendung und einige ihrer Erweiterungen.

2. RF Harper, F. Honsell, G. Plotkin: Ein Rahmen für die Definition von Logik .

3. F. Pfenning: Logische Rahmenbedingungen.

4. F. Pfenning: Logische Rahmenbedingungen - Eine kurze Einführung .