System F - System F

System F , auch bekannt als polymorpher Lambda-Kalkül ( Girard-Reynolds ) oder Lambda-Kalkül zweiter Ordnung , ist ein typisierter Lambda-Kalkül , der sich vom einfach typisierten Lambda-Kalkül durch die Einführung eines Mechanismus der universellen Quantifizierung über Typen unterscheidet. System F formalisiert somit den Begriff des parametrischen Polymorphismus in Programmiersprachen und bildet eine theoretische Grundlage für Sprachen wie Haskell und ML . System F wurde unabhängig vom Logiker Jean-Yves Girard (1972) und Informatiker entdeckt John C. Reynolds (1974).

Während der einfach typisierte Lambda-Kalkül Variablen hat, die sich über Terme erstrecken, und Binder dafür, hat System F zusätzlich Variablen, die über Typen reichen , und Binder dafür. Als Beispiel würde die Tatsache, dass die Identitätsfunktion jeden Typ der Form A → A haben kann, im System F als Urteil

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha}.x:\forall \alpha .\alpha \to \alpha}$

wobei ist eine Typvariable . Der Großbuchstabe wird traditionell verwendet, um Funktionen auf Typebene zu bezeichnen, im Gegensatz zum Kleinbuchstaben, der für Funktionen auf Wertebene verwendet wird. (Das hochgestellte bedeutet, dass das gebundene x vom Typ ist ; der Ausdruck nach dem Doppelpunkt ist der Typ des Lambda-Ausdrucks davor.) ${\displaystyle\alpha}$${\displaystyle \Lambda}$${\displaystyle \lambda}$${\displaystyle\alpha}$${\displaystyle\alpha}$

Als System zum Umschreiben von Begriffen normalisiert sich System F stark . Der Typrückschluss in System F (ohne explizite Typanmerkungen) ist jedoch unentscheidbar. Unter dem Curry-Howard-Isomorphismus entspricht System F dem Fragment der intuitionistischen Logik zweiter Ordnung , das nur universelle Quantifizierung verwendet. System F kann als Teil des Lambda-Würfels gesehen werden , zusammen mit noch ausdrucksstärkeren typisierten Lambda-Kalkülen, einschließlich solcher mit abhängigen Typen .

Laut Girard wurde das "F" in System F zufällig ausgewählt.

Tippregeln

Die Typisierungsregeln von System F sind die des einfach typisierten Lambda-Kalküls mit dem folgenden Zusatz:

${\displaystyle {\frac {\Gamma\vdash M{\mathbin {:}}\forall \alpha .\sigma }{\Gamma \vdash M\tau {\mathbin {:}}\sigma [\tau /\alpha ]}}}$ (1)

${\displaystyle {\frac {\Gamma ,\alpha ~{\text{type}}\vdash M{\mathbin {:}}\sigma }{\Gamma\vdash\Lambda \alpha .M{\mathbin {:} }\forall \alpha .\sigma }}}$ (2)

wobei Typen sind, eine Typvariable ist und im Kontext angibt, dass gebunden ist. Die erste Regel ist die der Anwendung, die zweite die der Abstraktion. ${\displaystyle\sigma,\tau}$${\displaystyle\alpha}$${\displaystyle \alpha ~{\text{type}}}$${\displaystyle\alpha}$

Logik und Prädikate

Der Typ ist definiert als: , wobei eine Typvariable ist . Das bedeutet: ist die Art von Funktionen , die einen Typ α als Eingabe und zwei Ausdrücke vom Typ α, und produzieren als Ausgabe ein Ausdruck des Typs α (beachte , dass wir als sein rechtsassoziativ .) ${\displaystyle {\mathsf {Boolean}}}$${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle\alpha}$${\displaystyle {\mathsf {Boolean}}}$${\displaystyle \to}$

Die folgenden zwei Definitionen für die booleschen Werte und werden verwendet, um die Definition von Church-Booleschen zu erweitern : ${\displaystyle\mathbf{T}}$${\displaystyle\mathbf{F}}$

${\displaystyle \mathbf{T} =\Lambda\alpha{.}\lambda x^{\alpha}\lambda y^{\alpha}{.}x}$

${\displaystyle \mathbf{F} =\Lambda\alpha{.}\lambda x^{\alpha}\lambda y^{\alpha}{.}y}$

(Beachten Sie, dass die beiden obigen Funktionen drei – nicht zwei – Argumente erfordern . Die letzten beiden sollten Lambda-Ausdrücke sein, die erste jedoch ein Typ. Diese Tatsache spiegelt sich in der Tatsache wider, dass der Typ dieser Ausdrücke ; der universelle Quantor ist Bindung der α entspricht den Λ die alpha in dem Lambda - Ausdruck Bindung selbst. Beachten sie auch, dass eine bequeme Abkürzung für ist , aber es ist nicht ein Symbol für System F selbst, sondern ein „Meta-Symbol“. Ebenso und sind auch "Meta-Symbole", bequeme Abkürzungen, von System-F-"Assemblies" (im Bourbaki-Sinn ); andernfalls, wenn solche Funktionen (innerhalb von System F) benannt werden könnten, dann bräuchte es keinen Lambda-Ausdrucksapparat, der fähig ist Funktionen anonym und für den Festkomma-Kombinator zu definieren , der diese Einschränkung umgeht.) ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle {\mathsf {Boolean}}}$${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$${\displaystyle\mathbf{T}}$${\displaystyle\mathbf{F}}$

Dann können wir mit diesen beiden -Termen einige logische Operatoren (die vom Typ sind ) definieren: ${\displaystyle \lambda}$${\displaystyle {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}}$

${\displaystyle {\begin{ausgerichtet}\mathrm {AND} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean} }\,y\,\mathbf {F} \\\mathrm {ODER} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\ mathsf {Boolean}}\,\mathbf {T} \,y\\\mathrm {NICHT} &=\lambda x^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\, \mathbf{F}\,\mathbf{T} \end{ausgerichtet}}}$

Beachten Sie, dass in den obigen Definitionen ein Typargument für ist , das angibt, dass die anderen beiden Parameter, die an übergeben werden, vom Typ sind . Wie bei den Church-Kodierungen besteht keine Notwendigkeit für eine IFTHENELSE- Funktion, da man einfach roh typisierte Begriffe als Entscheidungsfunktionen verwenden kann. Wenn jedoch eine angefordert wird: ${\displaystyle {\mathsf {Boolean}}}$${\displaystyle x}$${\displaystyle x}$${\displaystyle {\mathsf {Boolean}}}$${\displaystyle {\mathsf {Boolean}}}$

${\displaystyle \mathrm {IFTHENELSE} =\Lambda\alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha}\lambda z^{\alpha}.x\alpha yz}$

Wird besorgt. Ein Prädikat ist eine Funktion, die einen -typisierten Wert zurückgibt. Das grundlegendste Prädikat ist ISZERO, das genau dann zurückgibt, wenn sein Argument die Kirchenzahl 0 ist : ${\displaystyle {\mathsf {Boolean}}}$${\displaystyle\mathbf{T}}$

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\ ,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

Strukturen des Systems F

System F erlaubt die natürliche Einbettung rekursiver Konstruktionen, ähnlich wie in der Typentheorie von Martin-Löf . Abstrakte Strukturen (S) werden mit Konstruktoren erstellt . Dies sind Funktionen, die wie folgt typisiert sind:

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow\dots\rightarrow S}$.

Rekursivität manifestiert sich, wenn sie selbst in einem der Typen auftritt . Wenn Sie über diese Konstruktoren verfügen , können Sie den Typ von wie folgt definieren : ${\displaystyle S}$${\displaystyle K_{i}}$${\displaystyle m}$${\displaystyle S}$

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S ]\rightarrow\dots\rightarrow\alpha)\rightarrow\alpha}$

Zum Beispiel können die natürlichen Zahlen mit Konstruktoren als induktiver Datentyp definiert werden${\displaystyle N}$

${\displaystyle {\mathit {null}}:\mathrm {N} }$

${\displaystyle {\mathit {succ}}:\mathrm{N} \rightarrow\mathrm{N}}$

Der dieser Struktur entsprechende System F-Typ ist . Die Begriffe dieser Art umfassen eine getippte Version der Kirchenziffern , von denen die ersten sind: ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$

{{{1}}}${\displaystyle \Lambda\alpha.\lambda x^{\alpha}.\lambda f^{\alpha\to\alpha}.x}$

{{{1}}}${\displaystyle \Lambda\alpha.\lambda x^{\alpha}.\lambda f^{\alpha\to\alpha}.fx}$

{{{1}}}${\displaystyle \Lambda\alpha.\lambda x^{\alpha}.\lambda f^{\alpha\to\alpha}.f(fx)}$

{{{1}}}${\displaystyle \Lambda\alpha.\lambda x^{\alpha}.\lambda f^{\alpha\to\alpha}.f(f(fx))}$

Wenn wir die Reihenfolge der Curry-Argumente umkehren ( dh ), dann ist die Church-Zahl für eine Funktion, die eine Funktion f als Argument nimmt und die ^te Potenz von f zurückgibt . Das heißt, eine Kirchenzahl ist eine Funktion höherer Ordnung – sie nimmt eine Funktion f mit einem einzigen Argument und gibt eine andere Funktion mit einem einzigen Argument zurück. ${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha}$${\displaystyle n}$${\displaystyle n}$

Verwendung in Programmiersprachen

Die in diesem Artikel verwendete Version von System F ist ein explizit typisierter oder Church-Style-Kalkül. Die in λ-terms enthaltenen Typisierungsinformationen machen die Typprüfung einfach. Joe Wells (1994) löste ein "peinliches offenes Problem", indem er bewies, dass die Typprüfung für eine Curry-Variante von System F, dh eine Variante ohne explizite Typisierungsanmerkungen, unentscheidbar ist.

Das Ergebnis von Wells impliziert, dass Typinferenz für System F unmöglich ist. Eine Einschränkung von System F, bekannt als " Hindley-Milner " oder einfach "HM", hat einen einfachen Typinferenzalgorithmus und wird für viele statisch typisierte funktionale Programmiersprachen wie Haskell 98 und die ML- Familie verwendet. Im Laufe der Zeit, als die Einschränkungen von Typsystemen im HM-Stil offensichtlich wurden, haben sich Sprachen stetig zu ausdrucksstärkeren Logiken für ihre Typsysteme bewegt. GHC, ein Haskell-Compiler, geht über HM hinaus (seit 2008) und verwendet System F, das mit nicht-syntaktischer Typgleichheit erweitert wurde; Nicht-HM-Merkmale im Typsystem von OCaml umfassen GADT .

Der Girard-Reynolds-Isomorphismus

In der intuitionistischen Logik zweiter Ordnung wurde der polymorphe Lambda-Kalkül zweiter Ordnung (F2) von Girard (1972) und unabhängig von Reynolds (1974) entdeckt. Girard hat den Darstellungssatz bewiesen : dass in der intuitionistischen Prädikatenlogik zweiter Ordnung (P2) Funktionen von den natürlichen Zahlen zu den total beweisbaren natürlichen Zahlen eine Projektion von P2 auf F2 bilden. Reynolds bewies den Abstraktionssatz : dass jeder Term in F2 eine logische Relation erfüllt, die in die logischen Relationen P2 eingebettet werden kann. Reynolds bewies, dass eine Girard-Projektion gefolgt von einer Reynolds-Einbettung die Identität bildet, dh den Girard-Reynolds-Isomorphismus .

System F _ω

Während System F der ersten Achse von Barendregts Lambda-Würfel entspricht , kombiniert System F _ω oder der polymorphe Lambda-Kalkül höherer Ordnung die erste Achse (Polymorphismus) mit der zweiten Achse ( Typoperatoren ); es ist ein anderes, komplexeres System.

System F _ω kann induktiv auf einer Systemfamilie definiert werden, wobei die Induktion auf den in jedem System zulässigen Arten basiert :

• ${\displaystyle F_{n}}$ erlaubt Arten:
  • ${\displaystyle \star}$ (die Art der Typen) und
  • ${\displaystyle J\Rightarrow K}$where und (die Art der Funktionen von Typen zu Typen, wobei der Argumenttyp von niedrigerer Ordnung ist)${\displaystyle J\in F_{n-1}}$${\displaystyle K\in F_{n}}$

Im Grenzfall können wir das System definieren als ${\displaystyle F_{\omega}}$

• ${\displaystyle F_{\omega}={\underset {1\leq i}{\bigcup}}F_{i}}$

Das heißt, F _ω ist das System, das Funktionen von Typen zu Typen zulässt, wobei das Argument (und das Ergebnis) von beliebiger Reihenfolge sein können.

Beachten Sie, dass F _{ω zwar} die Reihenfolge der Argumente in diesen Zuordnungen nicht einschränkt, aber das Universum der Argumente für diese Zuordnungen einschränkt : Es müssen Typen und keine Werte sein. System F _ω erlaubt keine Abbildungen von Werten auf Typen ( abhängige Typen ), aber Abbildungen von Werten auf Werte ( Abstraktion), Abbildungen von Typen auf Werte ( Abstraktion) und Abbildungen von Typen auf Typen ( Abstraktion auf der Ebene der Typen). ) ${\displaystyle \lambda}$${\displaystyle \Lambda}$${\displaystyle \lambda}$

Siehe auch

• Existenzielle Typen – die existentiell quantifizierten Gegenstücke zu universellen Typen
• System F _<: — erweitert System F mit Subtyping
• System U

Anmerkungen

Verweise

Weiterlesen

• Pierce, Benjamin (2002). "V Polymorphism Ch. 23. Universal Types, Ch. 25. Eine ML-Implementierung von System F" . Typen und Programmiersprachen . MIT-Presse. S. 339–362, 381–388. ISBN 0-262-16209-1.

Externe Links

• Zusammenfassung von System F von Franck Binard.
• System F _ω : das Arbeitspferd moderner Compiler von Greg Morrisett