Typinferenz nach Hindley-Milner
Hindley-Milner (HM) ist ein Verfahren der Typinferenz mit parametrischem Polymorphismus für den Lambda-Kalkül. Es wurde erstmals von J. Roger Hindley[1] beschrieben und später von Robin Milner[2] wiederentdeckt. Luis Damas trug eine genaue formale Analyse und einen Beweis der Methode in seiner Doktorarbeit[3] bei, weshalb das Verfahren auch als Damas-Milner[4] bezeichnet wird. Unter den herausragenden Eigenschaften des HM sind Vollständigkeit und die Fähigkeit, den allgemeinsten Typ einer gegebenen Quelle ohne Hinzunahme von Annotationen oder sonstigen Hinweisen bestimmen zu können. HM ist ein effizientes Verfahren, das die Typisierung nahezu in linearer Zeit bzgl. der Größe der Quelle ermitteln kann, womit es praktisch zum Typisieren großer Programme anwendbar ist. HM wird bevorzugt in funktionalen Sprachen wie OCaml/Reason eingesetzt. Es wurde erstmals als Teil des Typsystems der Programmiersprache ML implementiert. Seitdem wurde HM auf verschiedene Weise erweitert, insbesondere durch beschränkte Typen, wie sie in Haskell verwendet werden.
Einleitung
Damas und Milner[4] trennen in der Gliederung ihrer Original-Veröffentlichung zwei sehr verschiedene Aufgaben, wobei die erste darin besteht, zu beschreiben, welche Typen ein Ausdruck haben kann. Die andere ist, einen Algorithmus anzugeben, der tatsächlich einen Typ ermittelt.
Beide Aspekte getrennt voneinander zu betrachten, erlaubt, sich eigens auf die Logik (d. h. Bedeutung) hinter dem Algorithmus konzentrieren und zugleich einen Prüfstein für die Eigenschaften des Verfahrens festlegen zu können. Wie Ausdrücke und Typen zueinander passen, wird mit Hilfe eines Deduktionssystems beschrieben. Wie jedes Beweissystem erlaubt es, auf verschiedenen Wegen zu einem Schluss zu gelangen. Da ein und derselbe Ausdruck begründbar verschiedene Typen haben kann, kann das Deduktionssystem auch zu durchaus unterschiedlichen Schlüssen über einen Ausdruck kommen. Im Gegensatz dazu ist bei der Typinferenz-Methode selbst (Algorithmus W) jeder Ausführungsschritt eindeutig bestimmt. Natürlich können in der Konstruktion des Algorithmus Entscheidungen getroffen worden sein, die so nicht in der Logik vorkommen, und eine genauere Betrachtung und Begründung verlangen, die ohne die obige Differenzierung nicht sichtbar würde.
Die Syntax
Ausdrücke |
Typen |
Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle {\begin{array}{llrll}{\textrm {mono}}&\tau &=&\alpha &\ {\textrm {Variable}}\\&&\vert &D\ \tau \dots \tau &\ {\textrm {Anwendung}}\\{\textrm {poly}}&\sigma &=&\tau \\&&\vert &\forall \ \alpha \ .\ \sigma &\ {\textrm {Quantor}}\\\\\end{array}}} |
Logik und Algorithmus teilen sich die Begriffe "Ausdruck" und "Typ", deren Form durch die Syntax präzisiert wird.
Die zu typisierenden Ausdrücke sind die des Lambda-Kalküls, erweitert um einen let-Ausdruck.
Die Form stellt die auch oft als geschriebene Funktionsanwendung dar, während die Abstraktion Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \lambda \ x.e} die anonyme Funktion bzw. das Funktionsliteral meint, die inzwischen in vielen zeitgenössischen Programmiersprachen verfügbar ist, dort vielleicht nur wortreicher etwa als Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle {\mathtt {function}}\,(x)\ {\mathtt {return}}\ e\ {\mathtt {end}}} ausgeschrieben.
Das Gesamt der Typen (Sorten) teilt sich in zwei Gruppen, die Mono- und Polytypen genannt werden.[note 1]
Monotypen , syntaktisch Terme, bezeichnen immer bestimmte Typen in dem Sinne, dass sie gleich nur sich selbst und verschieden von allen anderen sind. Charakteristische Vertreter der Monotypen sind Typkonstanten wie oder Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle string} . Typen können parametrisch sein, wie z. B. Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle Map\ (Set\ string)\ int} . All diese Typen sind Beispiele von Anwendungen von Typfunktionen , z. B. in den vorangegangenen Beispielen, wobei die hochgestellte Ziffer die Zahl der Typparameter angibt. Während die Wahl von grundsätzlich beliebig ist, muss sie im Zusammenhang des HM wenigstens den bequemerweise infix geschriebenen Funktionstyp enthalten. Beispielsweise hat eine Funktion, die ganze Zahlen auf Zeichenketten abbildet, den Typ Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle int\rightarrow string} .[note 2]
Vielleicht etwas irritierenderweise sind Typvariablen ebenfalls Monotypen. Eine allein stehende Typvariable bezeichnet einen Typ, der genau so konkret ist wie etwa oder und von beiden verschieden ist. Eine als Monotyp auftretende Typvariable verhält sich gerade so, als wäre sie eine Typkonstante über die man nur eben keine weiteren Informationen besitzt. Entsprechend bildet eine Funktionen mit dem Typ nur Werte des Typs auf sich selbst ab und kann nur auf Werte dieses Typs angewendet werden und auf keine anderen sonst.
Im Gegensatz dazu kann eine Funktion mit dem Polytyp jeden Wert auf einen Wert gleichen Typs abbilden. Die identische Funktion ist ein Wert für diesen Typ. Als weiteres Beispiel ist der Typ einer Funktion, die beliebige endliche Menge auf ganze Zahlen abbildet. Die Zahl der Elemente der Menge ist ein Wert für diesen Typ. Quantoren dürfen allerdings nur auf oberster Ebene auftreten, d. h. der Typ beispielsweise ist durch die Syntax ausgeschlossen. Ferner sind Monotypen eine Teilmenge der Polytypen, so dass Typen insgesamt die allgemeine Form haben.
Freie Typvariablen
Freie Typvariablen |
In einem Typ ist das Symbol der die Typvariablen im Monotyp bindende Quantor. Die Variablen heißen quantifiziert. Jedes Auftreten einer quantifizierten Variablen in heißt gebunden und alle ungebundenen Typvariablen heißen frei. Wie im Lambda-Kalkül ist der Begriff der freien und gebundenen Variablen grundlegend für das Verständnis der Bedeutung der Typen.
Dies ist sicherlich der schwierigste Teil des HM, vielleicht weil Polytypen, die freie Typvariablen enthalten, nicht in Programmiersprachen wie Haskell ausgedrückt werden können. Genauso gibt es keine freien Variablen in Prolog-Klauseln. Insbesondere mit beiden Sprachen erfahrene Entwickler, die somit eigentlich alle Voraussetzungen für den HM kennen, können diesen Punkt leicht übersehen. In Haskell beispielsweise sind alle Typvariablen implizit quantifiziert, z. B. bedeutet der Haskell-Typ Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle {\texttt {a~->~a}}} hier . Da Typen wie , obwohl sie durchaus in Haskell auftreten können, dort nicht ausdrückbar sind, können sie leicht mit der quantifizierten Version verwechselt werden.
Welche Funktionen können nun einen Typ wie z. B. , d. h. eine Mischung von gebundenen und ungebundenen Typvariablen, enthalten und was bedeutet eine freie Typvariable darin?
Beispiel 1 |
In Beispiel 1 ist der let-Ausdruck mit Typ-Annotationen in eckigen Klammern versehen. Offensichtlich wird der Parameter im Körper nicht verwendet, wohl aber die im äußeren Kontext von gebundene Variable . Als Konsequenz akzeptiert jeden Wert als Argument, während sie einen Wert liefert, der außerhalb gebunden ist und mithin auch sein Typ.
Im Gegensatz dazu hat den Typ , in dem alle Typvariablen gebunden auftreten. Wertet man z. B. aus, erhält man als Ergebnis eine Funktion vom Typ , was perfekt wiedergibt, dass der Monotyp von in durch den Aufruf verfeinert wurde.
In diesem Beispiel wird die freie Monotypvariable im Typ von durch die Quantifikation im äußeren Geltungsbereich mit Bedeutung beladen, nämlich im Typ von . Dies heißt im Zusammenhang dieses Beispiels, dass dieselbe Typvariable sowohl gebunden als auch frei in verschiedenen Typen auftritt. Insofern kann eine freie Typvariable ohne Kenntnis des Kontexts nicht besser interpretiert werden als zu konstatieren, dass es sich um einen Monotyp handelt. Anders gesagt ist eine Typung im Allgemeinen ohne Kenntnis des Kontexts nicht aussagekräftig.
Kontext und Typung
Syntax |
Freie Typvariablen |
Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle {\begin{array}{ll}{\text{frei}}(\ \Gamma \ )&=\ \bigcup \limits _{x:\sigma \in \Gamma }{\text{frei}}(\ \sigma \ )\end{array}}} |
Um die bislang getrennten Teile der Syntax, Ausdrücke und Typen sinnvoll zusammenzubringen, wird also ein Drittes, der Kontext, benötigt. Syntaktisch ist dieser einer Liste von Paaren Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle x:\sigma } , Belegung (s. a. Belegung, Zuordnung, Zuweisung) genannt, die jeder Wertvariablen im Kontext einen Typ zuordnet. Alle drei Teile zusammen ergeben eine Typung der Form Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \Gamma \ \vdash \ e:\sigma } , die aussagt, dass unter der Annahme der Ausdruck den Typ hat.
Da nun die vollständige Syntax zur Verfügung steht, kann schließlich eine sinnvolle Aussage über den Typ von in Beispiel 1 gemacht werden, nämlich . Im Gegensatz zu den vorangehenden Formulierungen ist die Monotypvariable nicht länger frei, d. h. bedeutungslos, sondern im Kontext als Typ der Wertvariablen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle x} gebunden. Offenbar spielt der Umstand, ob eine Typvariable im Kontext frei oder gebunden auftritt, eine bedeutsame Rolle für einen Typ im Rahmen einer Typung, daher wird Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathrm{frei}(\ \Gamma\ )} im Kasten präzisiert.
Anmerkungen zur Ausdrucksstärke
Da die Syntax des Ausdrucks einem mit dem Lambda-Kalkül unvertrauten Leser bei weitem zu ausdrucksschwach erscheinen mag und da die Beispiele dieses Vorurteil eher stützen werden, ist vielleicht der Hinweis hilfreich, dass sich HM nicht auf Spielzeugsprachen bezieht. Ein wesentliches Ergebnis der Forschung im Bereich der Berechenbarkeit ist, dass obige Ausdruckssyntax (ohne die let-Klausel) stark genug ist, jede berechenbare Funktion zu beschreiben. Darüber hinaus können alle weiteren Konstruktionen in Programmiersprachen relativ direkt syntaktisch in Ausdrücke des Lambda-Kalküls überführt werden. Darum werden diese einfachen Ausdrücke als Modell für Programmiersprachen verwendet. Ein Verfahren, das gut auf das Lambda-Kalkül anwendbar ist, kann leicht auf alle oder wenigstens viele andere syntaktische Konstruktionen einer speziellen Programmiersprache mittels der eben erwähnten Transformationen übertragen werden.
Zum Beispiel kann die zusätzliche Ausdrucksvariante Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \textbf{let}\ x = e_1\ \textbf{in}\ e_2} transformiert werden nach Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle (\lambda x.e_2)\ e_1} . Sie ist der Ausdruckssyntax im HM nur zur Unterstützung der Generalisierung während der Typinferenz hinzugefügt worden und nicht weil es der Syntax an Berechnungsstärke fehlt. HM behandelt also die Inferenz von Typen in Programmen im Allgemeinen und die verschieden funktionalen Sprachen, die diese Methode verwenden, belegen, wie gut ein Ergebnis, das nur für die Syntax des Lambda-Kalküls formuliert ist, auf syntaktisch komplexe Sprachen erweitert werden kann.
Im Gegensatz zum Eindruck, dass die Ausdrücke zu ausdrucksschwach für praktische Anwendungen seien, sind sie tatsächlich zu ausdrucksstark, um (im Allgemeinen) überhaupt typisiert zu werden. Dies ist eine Konsequenz der Unentscheidbarkeit für inhaltliche Aussagen über Ausdrücke des Lambda-Kalküls. Entsprechend ist die Berechnung der Typung von Programmen i. Allg. ein hoffnungsloses Unterfangen. Abhängig von der Natur des Typsystems wird dieses u. U. entweder nicht terminieren oder anderweitig den Dienst verweigern.
HM gehört zur letzteren Gruppe von Typsystemen. Ein Kollaps des Sortenapparats erscheint hier als eher subtile Situation, in der nur noch ein und derselbe Typ für die interessierenden Ausdrücke ermittelt wird. Dies ist kein Fehler im HM, sondern ein dem Problem der Typisierung selbst innewohnende Eigenschaft, die leicht in jeder stark getypten Sprache erzeugt werden kann. Hierzu kodiert man einen Auswerter (d. h. die universelle Funktion) für die „zu einfachen“ Ausdrücke. Man erhält damit einen einzelnen konkreten Typ, der den universellen Datentyp repräsentiert, wie er in typlosen Sprachen auftritt. Der Sortenapparat der Gastsprache ist dann kollabiert und kann die verschiedenen Typen von Werten nicht mehr unterscheiden, die der Auswertung übergeben oder von dieser erhalten werden. In diesem Zusammenhang ermittelt oder überprüft der Sortenapparat immer noch Typen, aber immer denselben, gerade als wäre das Typsystem gar nicht mehr vorhanden.
Ordnung polymorpher Typen
Während die Gleichheit von Monotypen rein syntaktisch ist, haben Polytypen eine reichere Beziehung zu anderen Sorten, die durch eine Spezialisierungsrelation Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sqsubseteq} ausgedrückt wird, wobei Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sigma \sqsubseteq \sigma'} bedeutet, dass Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sigma'} spezieller ist als Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sigma} .
Wird eine polymorphe Funktion auf einen Wert angewendet, dann muss sie ihre Form an den speziellen Typ dieses Wertes anpassen. Während dieser Anpassung ändert sie mithin auch ihren Typ, um zu dem des Parameters zu passen. Wird beispielsweise die identische Funktion mit dem Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\alpha.\alpha\rightarrow\alpha} auf eine Zahl mit dem Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle int} angewendet, dann können diese zunächst nicht zusammenwirken, da alle Typen verschieden sind und nicht passen. Was in dieser Lage benötigt wird, ist eine Funktion vom Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle int\rightarrow int} . Hierzu wird die polymorphe Identität im Rahmen der Anwendung in eine monomorphe Version ihrer selbst verwandelt. In Begriffen der Spezialisierung ausgedrückt, kann man dies als Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\alpha.\alpha\rightarrow\alpha \sqsubseteq\ int\rightarrow int} schreiben.
Nun ist die Formwandlung polymorpher Werte nicht völlig beliebig, sondern vielmehr durch den ursprünglichen Polytyp begrenzt. Dem Vorgang in diesem Beispiel folgend kann man die Spezialisierungsregel so umschreiben, dass ein polymorpher Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\alpha.\tau} durch konsistente Ersetzung jedes Auftretens von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \alpha} in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \tau} spezialisiert wird, wonach die Quantifizierung entfällt. Während diese Regel gut für alle Monotypen als Einsetzung funktioniert, schlägt sie fehl, wenn ein Polytyp als Ersetzung auftritt. Versucht man dies z. B. mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\beta.\beta} , dann erhält man einen unsyntaktischen Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\beta.\beta\rightarrow\forall\beta.\beta} . Aber nicht nur das. Selbst wenn eine geschachtelte Quantifizierung in der Syntax zulässig wäre, würde das Ergebnis dieser Ersetzung die Eigenschaft des ursprünglichen Typs in dem Parameter und Resultat der Funktion denselben Typ haben, nicht mehr erhalten, da nun beide Untertypen unabhängig voneinander geworden sind und jeder eine Spezialisierung mit verschiedenen Typen erlauben würde, so z. B. Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle string\rightarrow Set\ int} , was kaum die richtige Aufgabe für eine identische Funktion wäre.
Die syntaktische Einschränkung der Quantifizierung auf die oberste Ebene verhindert diese unerwünschte Generalisierung während der Spezialisierung. Anstelle von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\beta.\beta\rightarrow\forall\beta.\beta} muss in diesem Fall der speziellere Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\beta.\beta\rightarrow\beta} verwendet werden.
Man kann die eben erfolgte Spezialisierung durch eine weitere mit dem Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\alpha.\alpha} wieder aufheben. In Bezeichnungen der Relation erhält man zusammenfassend Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\alpha.\alpha\rightarrow\alpha \sqsubseteq \forall\beta.\beta\rightarrow\beta \sqsubseteq\forall\alpha.\alpha\rightarrow\alpha} , was bedeutet, dass syntaktische verschiedene Polytypen gleich bzgl. der Umbenennung ihrer quantifizierten Variablen sind.
Spezialisierungsregel |
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \displaystyle\frac{\tau' = \left[\alpha_i := \tau_i\right] \tau \quad \beta_i \not\in \textrm{frei}(\forall \alpha_1...\forall\alpha_n . \tau)}{\forall \alpha_1...\forall\alpha_n . \tau \sqsubseteq \forall \beta_1...\forall\beta_m . \tau'}} |
Konzentriert man sich nun nur auf die Frage, ob ein Typ spezieller als ein anderer ist, und mehr, wofür ein speziellerer Typ verwendet wird, dann kann man die Spezialisierung wie im nebenstehenden Kasten zusammenfassen. Im Uhrzeigersinn umschrieben, wird ein Typ spezialisiert, indem man jede der quantifizierten Variablen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \alpha_i} konsistent durch einen beliebigen Monotyp Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \tau_i} ersetzt, so dass man insgesamt einen Monotyp Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \tau'} erhält. Abschließend können Typvariablen, die im ursprünglichen Typ nicht frei auftraten, optional quantifiziert werden.
Die Spezialisierungsregel trägt also Sorge, dass keine freie Variable, d. h. Monotyp im ursprünglichen Typ, ungewollt durch einen Quantor gebunden wird. Ursprünglich quantifizierte Variablen können aber beliebig (konsistent) ersetzt werden, auch durch Typen, die neue quantifizierte oder unquantifizierte Variablen einführen.
Beginnend mit dem Polytyp Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \forall\alpha.\alpha} kann eine Spezialisierung den Körper entweder durch eine andere quantisierte Variable ersetzen, letztlich eine Umbenennung, oder durch eine Typkonstante (einschließlich des Funktionstyps), die die Parameter haben kann oder nicht, jede gefüllt mit einem Monotyp oder einer quantifizierten Typvariablen. Sobald eine quantifizierte Variable durch eine Typanwendung ersetzt worden ist, kann diese nicht mehr durch eine weitere Spezialisierung wieder aufgehoben werden, wie es bei der Ersetzung durch eine quantifizierte Variable möglich war. Typanwendungen sind also da, um zu bleiben. Nur wenn diese eine weitere quantifizierte Typvariable enthalten, kann die Spezialisierung durch deren weitere Ersetzung fortgeführt werden.
Die Spezialisierung führt also keine weiteren Gleichheiten auf Polytypen außer der bereits bekannten Umbenennung ein. Polytypen sind bis auf die Umbenennung ihrer gebundenen Variablen syntaktisch gleich. Die Gleichheit von Typen ist eine reflexive, antisymmetrische und transitive Relation und die verbleibende Spezialisierung von Polytypen ist transitiv. Damit ist die Relation Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sqsubseteq} eine Halbordnung.
Die Deduktionsmaschinerie
Die Syntax der Regeln |
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{lrl} \mathrm{Pr\ddot{a}dikat} & = &\sigma\sqsubseteq\sigma\\ & \vert\ &\alpha\not\in \mathrm{frei}(\Gamma)\\ & \vert\ &x:\alpha\in \Gamma\\ \\ \text{Urteil} & = &\text{Typung}\\ \mathrm{Pr\ddot{a}misse} & = &\text{Urteil}\ \vert\ \mathrm{Pr\ddot{a}dikat}\\ \text{Schluss} & = &\text{Urteil}\\ \\ \text{Regel} & = &\displaystyle\frac{\mathrm{Pr\ddot{a}misse}\ \dots}{\textrm{Schluss}}\quad [\mathtt{Name}] \end{array} } |
Die Syntax von HM wird durch die Syntax der Inferenzregeln fortgeführt, die den Körper des formalen Systems bilden, indem sie die Typungen als Urteile verwenden. Die Regeln definieren, aus welchen Voraussetzungen man welche Schlüsse ziehen kann. Zusätzlich zu den Urteilen können einige weiter oben eingeführte Randbedingungen als Prämissen verwendet werden.
Ein Beweis mittels der Regeln ist eine Sequenz von Urteilen, so dass alle Prämissen vor den Schlüssen aufgelistet werden. Siehe die folgenden Beispiele 2,3 für ein mögliches Format der Beweise. Von links nach rechts zeigt jede Zeile den Schluss, den Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Namen}]} der angewandten Regel und die Prämissen, entweder durch Verweis auf eine vorangehende Zeile, wenn die Prämisse ein Urteil ist, oder durch explizite Angabe des Prädikats.
Die Typungsregeln
Deklaratives Regelsystem |
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{cl} \displaystyle\frac{x:\sigma \in \Gamma}{\Gamma \vdash x:\sigma}&[\mathtt{Var}]\\ \\ \displaystyle\frac{\Gamma \vdash e_0:\tau \rightarrow \tau' \quad\quad \Gamma \vdash e_1 : \tau }{\Gamma \vdash e_0\ e_1 : \tau'}&[\mathtt{App}]\\ \\ \displaystyle\frac{\Gamma,\;x:\tau\vdash e:\tau'}{\Gamma \vdash \lambda\ x\ .\ e : \tau \rightarrow \tau'}&[\mathtt{Abs}]\\ \\ \displaystyle\frac{\Gamma \vdash e_0:\sigma \quad\quad \Gamma,\,x:\sigma \vdash e_1:\tau}{\Gamma \vdash \mathtt{let}\ x = e_0\ \mathtt{in}\ e_1 : \tau} &[\mathtt{Let}]\\ \\ \\ \displaystyle\frac{\Gamma \vdash e:\sigma' \quad \sigma' \sqsubseteq \sigma}{\Gamma \vdash e:\sigma}&[\mathtt{Inst}]\\ \\ \displaystyle\frac{\Gamma \vdash e:\sigma \quad \alpha \notin \text{frei}(\Gamma)}{\Gamma \vdash e:\forall\ \alpha\ .\ \sigma}&[\mathtt{Gen}]\\ \\ \end{array}} |
Der seitliche Kasten zeigt die Deduktionsregel des HM-Typsystems. Man kann sie grob in zwei Gruppen einteilen:
Die ersten vier Regeln Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Var}]} , Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{App}]} , und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Let}]} sind um die Syntax zentriert und geben je eine Regel für jede der Ausdrucksformen an. Ihre Bedeutung ist schon auf den ersten Blick recht offensichtlich, da sie jeden Ausdruck aufteilen, die Beweise der Teilausdrücke heranziehen und die Einzeltypen in den Prämissen zum Typ im Schluss kombinieren.
Die zweite Gruppe wird durch die verbleibenden Regeln Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Inst}]} and Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Gen}]} gebildet, die die Spezialisierung und Generalisierung von Typen behandeln. Während die Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Inst}]} Regel inhaltlich im Abschnitt über die Spezialisierung bereits beschrieben wurde, vervollständigt die Regel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Gen}]} diese durch die umgekehrter Richtung. Sie erlaubt eine Generalisierung, d. h. eine Quantifizierung einer nicht im Kontext gebundenen Monotypvariablen. Die Notwendigkeit für die Einschränkung Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \alpha \not\in \mathrm{frei}(\ \Gamma\ )} wurde im Abschnitt über die freien Typvariablen eingeführt.
Die folgenden beiden Beispiele exerzieren das Regelsystem in Aktion.
Beispiel 2: Ein Beweis für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma \vdash id(n):int} mit kann wie folgt geschrieben werden:
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{llll} 1:&\Gamma \vdash id : \forall\alpha.\alpha \rightarrow \alpha &[\mathtt{Var}]& (id : \forall\alpha.\alpha \rightarrow \alpha \in \Gamma) \\ 2:&\Gamma \vdash id : int \rightarrow int & [\mathtt{Inst}]&(1),\ (\forall\alpha.\alpha \rightarrow \alpha \sqsubseteq int\rightarrow int)\\ 3:&\Gamma \vdash n : int&[\mathtt{Var}]&(n : int \in \Gamma)\\ 4:&\Gamma \vdash id(n) : int&[\mathtt{App}]& (2),\ (3)\\ \end{array} }
Beispiel 3: Um die Generalisierung zu demonstrieren, wird Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash\ \textbf{let}\, id = \lambda x . x\ \textbf{in}\ id\, :\, \forall\alpha.\alpha\rightarrow\alpha} gezeigt:
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{llll} 1: & x:\alpha \vdash x : \alpha & [\mathtt{Var}] & (x:\alpha \in \left\{x:\alpha\right\})\\ 2: & \vdash \lambda x.x : \alpha\rightarrow\alpha & [\mathtt{Abs}] & (1)\\ 3: & \vdash \lambda x.x : \forall \alpha.\alpha\rightarrow\alpha & [\mathtt{Gen}] & (2),\ (\alpha \not\in \mathrm{frei}(\epsilon))\\ 4: & id:\lambda\alpha.\alpha\rightarrow\alpha \vdash id : \lambda\alpha.\alpha\rightarrow\alpha & [\mathtt{Var}] & (id:\lambda\alpha.\alpha\rightarrow\alpha \in \left\{id : \lambda\alpha.\alpha\rightarrow\alpha\right\})\\ 5: & \vdash \textbf{let}\, id = \lambda x . x\ \textbf{in}\ id\, :\,\forall\alpha.\alpha\rightarrow\alpha & [\mathtt{Let}] & (3),\ (4)\\ \end{array} }
Haupttyp
Wie in der Einleitung erwähnt, erlauben die Regeln verschiedene Typen für ein und denselben Ausdruck zu erschließen. Siehe Beispiel 2, Schritte 1,2 und Beispiel 3, Schritte 2,3 für drei verschiedene Typungen desselben Ausdrucks. Offenbar sind die verschiedenen Ergebnisse nicht völlig unabhängig, sondern durch die Typordnung verbunden. Es ist eine wesentliche Eigenschaft des Regelsystems und der Typordnung, dass, wenn mehr als ein Typ für einen Ausdruck erschlossen werden kann, sich unter diesen Typen (modulo Gleichheit) ein eindeutig bestimmter, allgemeinster Typ in dem Sinne befindet, dass alle anderen Spezialisierungen von ihm sind. Während ein Regelsystem es zulassen muss, spezialisierte Typen herzuleiten, sollte ein Typinfernzalgorithmus den allgemeinsten oder Haupttyp als Ergebnis liefern.
Let-Polymorphismus
Nicht unmittelbar ersichtlich kodiert die Regelmenge eine Vorschrift, unter welchen Umständen ein Typ generalisiert werden darf und wann nicht. Dies geschieht durch eine leichte Variation im Gebrauch von Mono- und Polytypen in den Regeln und .
In der Regel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Abs}]} wird die Wertvariable des Parameters der Funktion Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \lambda x.e} dem Kontext als ein monomorpher Typ durch die Prämisse Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma,\ x:\tau \vdash e:\tau'} hinzugefügt, während in der Regel Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Let}]} die Variable die Umgebung in polymorpher Form Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma,\ x:\sigma \vdash e_1:\tau'} betritt. Obwohl in beiden Fällen die Anwesenheit von x im Kontext den Gebrauch der Generalisierungsregel für jede Monotypvariable in der Zuordnung verhindert, erzwingt diese Vorschrift, dass ein Parameter x in einem Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \lambda} -Ausdruck monomorph bleibt, während in einem let-Ausdruck die Typvariablen bereits polymorph eingeführt werden können, was Spezialisierungen ermöglicht.
Als Konsequenz dieses Reglements kann kein Typ für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \lambda f.(f\, \textrm{true}, f\, \textrm{0})} erschlossen werden, da sich der Parameter Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle f} in monomorpher Position befindet, während Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \textbf{let}\ f = \lambda x . x\, \textbf{in}\, (f\, \textrm{true}, f\, \textrm{0})} den Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle (bool, int)} darum ergibt, weil Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle f} in einem let-Ausdruck eingeführt und darum polymorph behandelt wird. Beachte, dass dieses Verhalten sich in starkem Gegensatz zu üblichen Definition Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \textbf{let}\ x = e_1\ \textbf{in}\ e_2\ ::= (\lambda\ x.e_2)\ e_1} befindet, was der Grund dafür ist, die let-Variante überhaupt in die Syntax des Ausdrucks aufzunehmen. Diese Unterscheidung wird let-Polymorphismus genannt und ist dem HM eigentümlich.
Übergang zum Algorithmus
Da nun das Deduktionssystem des HMs zur Hand ist, könnte man einen Algorithmus vorstellen diesen gegen die Regel überprüfen. Alternativ kann man ihn möglicherweise durch einen genaueren Blick darauf, wie die Regeln zusammenwirken und die Beweise geformt sind, auch herleiten. Dieser Weg wird nun im verbleibenden Rest dieses Artikels durch eine Fokussierung auf die möglichen Entscheidungen während des Beweisens einer Typung beschritten.
Freiheitsgrade bei der Regelauswahl
Isoliert man in einem Beweise die Stellen an denen überhaupt keine Auswahl möglich ist, dann erhält man die um die Ausdruckssyntax zentrierte erste Gruppe von Regeln, die gleichsam das Gerüst des Beweises bestimmt, da jede der Schlussregeln genau einer Regel der Syntax entspricht, während zwischen den Prämissen und Schlüssen dieser festen Regelanwendungen verbindende Ketten von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Inst}]} and Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle [{\mathtt {Gen}}]} auftreten können. Alle Beweise müssen die so skizzierte Form haben.
Da die einzige Möglichkeit in einem Beweis im Hinblick auf die Regelauswahl diese Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Inst}]} und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Gen}]} Ketten sind, legt die Gestalt der Beweise die Frage nahe, ob man präzisieren kann wo diese Ketten benötigt werden. Dies ist in der Tat möglich und führt auf eine Variante des Regelsystems ohne diese beiden Regeln.
Syntaxgesteuertes Regelsystem
Syntaktisches Regelsystem |
Generalisierung |
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bar{\Gamma}(\tau) = \forall\ \hat{\alpha}\ .\ \tau \quad\quad \hat{\alpha} = \textrm{frei}(\tau) - \textrm{frei}(\Gamma) } |
Eine zeitgenössische Behandlung des HM verwendet ein rein syntaxgesteuertes Regelsystem nach Clement[5] als Zwischenschritt. In diesem System ist die Spezialisierung direkt hinter der ursprünglichen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Var}]} Regel platziert und nun in diese eingemischt, während die Generalisierung mit in die Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Let}]} Regel aufgenommen wurde. Hierbei ist die Generalisierung zudem durch die Einführung der Funktion Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bar{\Gamma}(\tau)} so bestimmt, dass sie immer den allgemeinsten Typ erzeugt, indem sie alle nicht in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma} gebundenen Monotypvariablen quantifiziert.
Um zu überprüfen, dass dieses neue Regelsystem Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S} zum Original äquivalent ist, hat man zu zeigen, dass Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \Gamma \vdash _{D}\ e:\sigma \Leftrightarrow \Gamma \vdash _{S}\ e:\sigma } , was in zwei Teilbeweise zerfällt:
- (Korrektheit)
- Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma \vdash_D\ e:\sigma \Rightarrow \Gamma \vdash_S\ e:\sigma} (Vollständigkeit)
Während man die Korrektheit durch Zerlegung der Regeln Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Let}]} and Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Var}]} von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S} zu Beweisen in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_D} sehen kann, ist ebenso erkennbar, dass Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S} unvollständig ist, da man z. B. nicht zeigen kann, dass Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S\ \lambda\ x.x:\forall\alpha.\alpha\rightarrow\alpha} gilt, sondern bestenfalls nur Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S\ \lambda\ x.x:\alpha\rightarrow\alpha} . Allerdings ist eine nur leicht schwächere Version der Vollständigkeit nachweisbar[6], nämlich:
- Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma \vdash_D\ e:\sigma \Rightarrow \Gamma \vdash_S\ e:\tau \wedge \bar{\Gamma}(\tau)\sqsubseteq\sigma}
was besagt, dass man den Haupttyp für einen Ausdruck in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S} herleiten kann, wenn man erlaubt, den Beweis am Ende zu generalisieren.
Beachte, dass Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S} im Vergleich zu Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_D} nur noch Monotypen in den Urteilen seiner Regeln enthält.
Freiheitsgrade bei der Regelinstanzierung
Bei gegebenem Ausdruck ist man innerhalb der Regeln selber frei die Instanzen für alle (Regel-)Variablen zu wählen, die nicht bereits durch die Ausdrücke festgelegt sind. Dies sind die Instanzen für die Typvariablen in den Regeln. Arbeitet man darauf hin, den Haupttyp zu zeigen, dann lässt sich die Wahl auf das Aussuchen geeigneter Typen für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \tau} in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Var}]} und einschränken. Die Entscheidung für eine angemessene Auswahl kann nicht lokal erfolgen, aber deren Qualität wird in den Prämissen von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{App}]} erkennbar, der einzigen Regel, in der zwei unterschiedliche Typen, nämlich der des formalen und der des aktuellen Parameters, zu einem zusammenkommen müssen.
Darum würde eine allgemeine Strategie, um einen Beweis zu finden, darin bestehen, die allgemeinste Annahme (Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \alpha \not\in \mathrm{frei}(\Gamma)} ) für Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \tau} zu machen und diese sowie die in Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Abs}]} zu treffende Wahl zu verfeinern, bis alle durch die Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{App}]} Regeln geforderten Randbedingungen endlich erfüllt sind. Glücklicherweise sind hierfür weder Versuch und Irrtum noch irgendwelche Iterationen erforderlich, da eine effektive Methode zur Berechnung aller notwendigen Entscheidungen bekannt ist, die Unifikation nach Robinson in Verbindung mit dem sogenannten Union-Find-Algorithmus.
Um das Union-Find-Verfahren kurz zusammenzufassen, erlaubt es bei gegebener Menge aller Typen in einem Beweis, diese mittels der Prozedur Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathtt{union}} in Äquivalenzklassen zu teilen und mittels der Prozedur Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle {\mathtt {find}}} einen Repräsentanten zu bestimmen. Das Wort Prozedur im Sinne von Nebenwirkung betonend, wird das Reich der Logik hier verlassen, um einen effektiven Algorithmus vorzubereiten. Der Repräsentant von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathtt{union}(a,b)} ist hierbei so bestimmt, dass, falls sowohl Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle a} und auch Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle b} Typvariablen sind, der Repräsentant beliebig eine von ihnen ist, während bei einer Vereinigung von einer Variablen und einer Anwendung letztere zum Repräsentanten gewählt wird. Hat man eine solche Implementierung des Union-Find zur Hand, dann kann man die Unifikation zweier Monotypen wie folgt formulieren:
unify(ta,tb): ta = find(ta) tb = find(tb) wenn ta,tb beide Anwendungen der Form D p1..pn mit identischen D,n sind dann unify(ta[i],tb[i]) für jeden korrespondierenden i-ten Parameter sonst wenn wenigstens einer von ta,tb eine Typvariable ist dann union(ta,tb) sonst fehler 'Die Typen ta,tb passen nicht zusammen.'
Algorithmus W
Algorithmus W |
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \begin{array}{cl} \displaystyle\frac{x:\sigma \in \Gamma \quad \tau = \mathit{inst}(\sigma)}{\Gamma \vdash x:\tau}&[\mathtt{Var}]\\ \\ \displaystyle\frac{\Gamma \vdash e_0:\tau_0 \quad \Gamma \vdash e_1 : \tau_1 \quad \tau'= \mathit{newvar} \quad \mathit{unify}(\tau_0,\ \tau_1 \rightarrow \tau') }{\Gamma \vdash e_0\ e_1 : \tau'}&[\mathtt{App}]\\ \\ \displaystyle\frac{\tau = \mathit{newvar} \quad \Gamma,\;x:\tau\vdash e:\tau'}{\Gamma \vdash \lambda\ x\ .\ e : \tau \rightarrow \tau'}&[\mathtt{Abs}]\\ \\ \displaystyle\frac{\Gamma \vdash e_0:\tau \quad\quad \Gamma,\,x:\bar{\Gamma}(\tau) \vdash e_1:\tau'}{\Gamma \vdash \mathtt{let}\ x = e_0\ \mathtt{in}\ e_1 : \tau'}&[\mathtt{Let}] \end{array} } |
Die Präsentation des Algorithmus W wie er im Kasten an der Seite gezeigt wird, weicht nicht nur signifikant vom Original[4] ab, sondern stellt auch einen erheblichen Fehlgebrauch der Notation logischer Regeln dar, da er Nebeneffekte mit einschließt. Dies ist hier dadurch legitimiert, um einen direkten Vergleich mit Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \vdash_S} zu ermöglichen und zugleich eine effektive Implementierung anzugeben. Die Regeln spezifizieren nun eine Prozedur mit Parametern und Resultat Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \tau} im Schluss, wobei die Ausführung der Prämissen von links nach rechts verläuft. Alternativ zu einer Prozedur können die Regeln als eine Attributierung (mit denselben Anmerkungen bzgl. der Nebeneffekte) angesehen werden.
Die Prozedur 'Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle inst(\sigma)} ' spezialisiert den Polytyp Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \sigma} , indem sie den Term kopiert und die darin enthaltenen gebundenen Variablen konsistent durch (global) neue Monotypvariablen ersetzt. 'Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle newvar} ' erzeugt eine neue Monotypvariable. In ähnlicher Weise hat eine Kopie des Typs herzustellen, in der (global) neue Typvariablen für die Quantifikation eingeführt werden, um ungewollte Bindungen zu vermeiden.
Insgesamt verfährt der Algorithmus nun, indem er immer die allgemeinst mögliche Auswahl triff und die Spezialisierung der Unifikation überlässt, die ihrerseits das allgemeinst mögliche Resultat erzeugt. Wie oben angemerkt, ist das Ergebnis Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \tau} am Ende noch einmal zu Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bar{\Gamma}(\tau)} zu generalisieren, um den Haupttyp für einen gegebenen Ausdruck zu erhalten.
Da die im Algorithmus verwendeten Prozeduren Kosten nahe Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle O(1)} haben, sind die Gesamtkosten des Verfahrens nahezu linear zur Größe des Ausdrucks, für den ein Typ zu inferieren ist. Es steht damit in starkem Kontrast zu vielen anderen Versuchen, ein Typinferenzverfahren herzustellen, die sich oft als NP-schwer, wenn nicht unentscheidbar bzgl. Terminierung herausgestellt haben. Mithin hat HM denselben Durchsatz, den das beste voll informierte Typprüfungsverfahren haben kann. Typprüfung heißt hier, dass ein Algorithmus keinen Beweis zu finden hat, sondern diesen nur zu überprüfen braucht.
Die Effizienz ist aus zwei Gründen geringfügig niedriger. Zum ersten sind die Bindungen der Typvariablen im Kontext zu verwalten, um die Berechnung von Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \bar{\Gamma}(\tau)} zu erlauben. Ferner ist ein occurs check erforderlich, um die Entstehung rekursiver Typen während Unifikation zu verhindern. Ein Beispiel für einen solchen Fall ist , für das kein Typ mit dem HM hergeleitet werden kann. Da in der Praxis die Typen nur kleine Terme sind und sich zudem nicht zu expandierenden Strukturen aufbauen, kann man sie in der Komplexitätsanalyse als kleiner als eine bestimmte Konstante betrachten, so dass die O(1)-Kosten gewahrt bleiben.
Der Algorithmus W im Original
In der Originalpublikation[4] wird der Algorithmus formaler in einem Substitutionsstil beschrieben statt durch Nebeneffekte wie in der Methode oben. In letzter Form kümmert sich der Nebeneffekte unsichtbar um alle Stellen, in denen Typvariablen verwendet werden. Explizite Verwendung der Substitution macht nicht nur den Algorithmus schwerer zu lesen, da die Nebeneffekte praktisch überall auftreten, sondern vermittelt auch den falschen Eindruck, dass die Methode teuer ist. Wird sie hingegen mit rein funktionalen Mitteln oder zum Zweck des Beweises der Äquivalenz zum Deduktionssystem implementiert, ist voll Explizitheit natürlich notwendig und die Originalformulierung eine notwendige Verfeinerung.
Weitere Themen
Rekursive Definitionen
Eine zentrale Eigenschaft des Lambda-Kalküls ist, dass rekursive Definitionen nicht elementar sind, sondern mit Hilfe des Fixpunktkombinators ausgedrückt werden können. In der Originalpublikation[4] wird angemerkt, dass Rekursion mit dem Typ Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle fix:\forall\alpha.(\alpha\rightarrow\alpha)\rightarrow\alpha} dieses Kombinators realisiert werden kann. Eine mögliche rekursive Definition kann damit als Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathtt{rec}\ v = e_1\ \mathtt{in}\ e_2\ ::=\mathtt{let}\ v = fix(\lambda v.e_1)\ \mathtt{in}\ e_2} formuliert werden.
Alternativ ist eine Erweiterung der Ausdruckssyntax und eine zusätzliche Typregel möglich mit:
Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \displaystyle\frac{ \Gamma, \Gamma' \vdash e_1:\tau_1\quad\dots\quad\Gamma, \Gamma' \vdash e_n:\tau_n\quad\Gamma, \Gamma'' \vdash e:\tau }{ \Gamma\ \vdash\ \mathtt{rec}\ v_1 = e_1\ \mathtt{and}\ \dots\ \mathtt{and}\ v_n = e_n\ \mathtt{in}\ e:\tau }\quad[\mathtt{Rec}]}
mit
- Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \Gamma' = v_1:\tau_1,\ \dots,\ v_n:\tau_n}
- Fehler beim Parsen (Konvertierungsfehler. Der Server („https://wikimedia.org/api/rest_“) hat berichtet: „Cannot get mml. Server problem.“): {\displaystyle \Gamma ''=v_{1}:{\bar {\Gamma }}(\ \tau _{1}\ ),\ \dots ,\ v_{n}:{\bar {\Gamma }}(\ \tau _{n}\ )}
Hierin sind grundsätzlich Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Abs}]} und Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle [\mathtt{Let}]} zusammengemischt, wobei die rekursiv definierten Variablen monomorph behandelt werden, wenn sie links vom Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle \mathtt{in}} auftreten, aber polymorph rechts davon. Diese Formulierung fasst die Essenz des let-Polymorphismus vielleicht am besten zusammen.
Anmerkungen
- ↑ Polytypen werden in der Originalpublikation als Typ-Schemata ("type schemes") bezeichnet.
- ↑ Die parametrischen Typen Fehler beim Parsen (MathML mit SVG- oder PNG-Rückgriff (empfohlen für moderne Browser und Barrierefreiheitswerkzeuge): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle D\ \tau\dots\tau} sind in der Originalpublikation über HM nicht enthalten und für die Darstellung der Methode auch nicht erforderlich. Keine der Inferenzregeln ist für sie zuständig oder würde ihre Abwesenheit bemerken. Dasselbe gilt für die nichtparametrischen "primitiven Typen" im betreffenden Papier. Die gesamte Maschinerie polymorpher Typinferenz kann ohne sie definiert werden. Sie sind hier teils der Beispiele wegen aufgenommen, aber vor allem, da sich die Natur des HM ganz und gar um polymorphe Typen dreht. Der parametrische Polymorphismus tritt im Original nur in spezieller Form durch den in den Inferenzregeln fest verdrahteten Funktionstyp auf, der zwei polymorphe Parameter hat und hier nur als spezieller Fall behandelt wird.
Einzelnachweise
- ↑ R. Hindley, (1969) The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, Vol. 146, S. 29–60 JSTOR 1995158
- ↑ Milner, (1978) A Theory of Type Polymorphism in Programming. Journal of Computer and System Science (JCSS) 17, S. 348–374 online
- ↑ Luis Damas (1985): Type Assignment in Programming Languages. PhD thesis, University of Edinburg (CST-33-85)
- ↑ a b c d e Damas, Milner (1982), Principal type-schemes for functional programs. 9th Symposium on Principles of programming languages (POPL'82) S. 207–212, ACM: PDF (Memento vom 24. März 2012 im Internet Archive)
- ↑ Clement, (1987). The Natural Dynamic Semantics of Mini-Standard ML. TAPSOFT'87, Vol 2. LNCS, Vol. 250, pp 67-81
- ↑ Jeff Vaughan, A proof of correctness for the Hindley-Milner type inference algorithm (Memento vom 24. März 2012 im Internet Archive) (PDF, 152 KB)