Ich schwöre, es gab früher ein T-Shirt zum Verkauf mit den unsterblichen Worten:
Welchen Teil von
verstehst du nicht
In meinem Fall wäre die Antwort ... alles!
Insbesondere sehe ich in Haskell-Zeitungen oft eine solche Notation, aber ich habe keine Ahnung, was dies bedeutet. Ich habe keine Ahnung, welcher Zweig der Mathematik es sein soll.
Ich erkenne natürlich die Buchstaben des griechischen Alphabets und Symbole wie "∉" (was normalerweise bedeutet, dass etwas kein Element einer Menge ist).
Andererseits habe ich noch nie "⊢" gesehen ( Wikipedia behauptet, es könnte "Partition" bedeuten ). Ich bin auch mit der Verwendung des Vinculums hier nicht vertraut. ( In der Regel bezeichnet er einen Bruchteil, aber das bedeutet nicht erscheinen hier der Fall zu sein.)
Wenn mir zumindest jemand sagen könnte, wo ich anfangen soll, um zu verstehen, was dieses Meer von Symbolen bedeutet, wäre das hilfreich.
quelle
Antworten:
:
Mittel hat Typ∈
Mittel ist in . (Bedeutet ebenfalls∉
"ist nicht in".)Γ
wird normalerweise verwendet, um sich auf eine Umgebung oder einen Kontext zu beziehen ; In diesem Fall kann es sich um eine Reihe von Typanmerkungen handeln, bei denen ein Bezeichner mit seinem Typ gepaart wird. Daherx : σ ∈ Γ
bedeutet, dass die UmgebungΓ
die Tatsache enthält, dassx
Typ hatσ
.⊢
kann gelesen werden als beweist oder bestimmt.Γ ⊢ x : σ
Mittel , dass die UmgebungΓ
bestimmt , dassx
Typ hatσ
.,
ist eine Möglichkeit , mit bestimmten zusätzlichen Voraussetzungen in eine UmgebungΓ
.Daher
Γ, x : τ ⊢ e : τ'
bedeutet die UmweltΓ
, mit dem zusätzlichen, zwingende Voraussetzung , daßx
Typ hatτ
, zeigt , dasse
Typ hatτ'
.Wie gewünscht: Operatorrang, vom höchsten zum niedrigsten:
λ x . e
,∀ α . σ
undτ → τ'
,let x = e0 in e1
und Leerzeichen für Funktionsanwendung.:
∈
und∉
,
(linksassoziativ)⊢
quelle
:
und∈
sind insofern sehr ähnlich, als sie bedeuten, dass eine Sache in einer anderen Sache enthalten ist - eine Menge enthält Elemente, und ein Typ enthält gewissermaßen Werte. Der entscheidende Unterschied besteht darinx ∈ S
, dass eine MengeS
buchstäblich ein Element enthältx
, während diesΓ ⊢ x : T
bedeutet,x
dass abgeleitet werden kann, um den TypT
im Kontext zu bewohnenΓ
. In Anbetracht dessen lautet die Var-Regel: »Wenn x buchstäblich im Kontext enthalten ist, kann es (trivial) daraus abgeleitet werden«.(Γ,(x:τ))⊢(x:σ)
siehe overleaf.com/read/ddmnkzjtnqbd#/61990222Diese Syntax mag zwar kompliziert aussehen, ist aber eigentlich ziemlich einfach. Die Grundidee stammt aus der formalen Logik: Der gesamte Ausdruck ist eine Implikation, wobei die obere Hälfte die Annahmen und die untere Hälfte das Ergebnis sind. Das heißt, wenn Sie wissen, dass die oberen Ausdrücke wahr sind, können Sie daraus schließen, dass auch die unteren Ausdrücke wahr sind.
Symbole
Eine andere Sache zu beachten ist, dass einige Buchstaben traditionelle Bedeutungen haben; Insbesondere repräsentiert Γ den "Kontext", in dem Sie sich befinden - das sind die Arten anderer Dinge, die Sie gesehen haben. So etwas wie
Γ ⊢ ...
bedeutet "der Ausdruck,...
wenn Sie die Typen jedes Ausdrucks in kennenΓ
.Das
⊢
Symbol bedeutet im Wesentlichen, dass Sie etwas beweisen können. SoΓ ⊢ ...
heißt es in einer Aussage: "Ich kann...
in einem Kontext beweisenΓ
. Diese Aussagen werden auch als Typurteile bezeichnet."Eine andere Sache zu beachten: In der Mathematik bedeutet genau wie ML und Scala,
x : σ
dassx
Typ hatσ
. Sie können es genauso lesen wie Haskellx :: σ
.Was jede Regel bedeutet
Wenn wir das wissen, wird der erste Ausdruck leicht zu verstehen: Wenn wir das wissen
x : σ ∈ Γ
(x
dhσ
in einem bestimmten Kontext einen Typ habenΓ
), dann wissen wir dasΓ ⊢ x : σ
(das heißt, inΓ
,x
hat einen Typσ
). Das sagt Ihnen also wirklich nichts sehr Interessantes. Es zeigt Ihnen nur, wie Sie Ihren Kontext verwenden.Die anderen Regeln sind ebenfalls einfach. Nehmen Sie zum Beispiel
[App]
. Diese Regel hat zwei Bedingungen:e₀
ist eine Funktion von einem Typτ
zu einem Typτ'
unde₁
ist ein Wert vom Typτ
. Jetzt wissen Sie , welche Art Sie durch die Anwendung erhaltene₀
zue₁
! Hoffentlich ist das keine Überraschung :).Die nächste Regel hat eine neue Syntax. Insbesondere
Γ, x : τ
bedeutet nur der KontextΓ
und das Urteilx : τ
. Wenn wir also wissen, dass die Variablex
einen Typ vonτ
und der Ausdrucke
einen Typ hatτ'
, kennen wir auch den Typ einer Funktion, die nimmtx
und zurückgibte
. Dies sagt uns nur, was zu tun ist, wenn wir herausgefunden haben, welchen Typ eine Funktion hat und welchen Typ sie zurückgibt. Es sollte also auch nicht überraschend sein.Der nächste zeigt Ihnen nur, wie Sie mit
let
Anweisungen umgehen . Wenn Sie wissen, dass ein Ausdrucke₁
einen Typ hatτ
, solange erx
einen Typ hatσ
, hat einlet
Ausdruck, der lokal anx
einen Wert vom Typσ
gebunden ist,e₁
einen Typτ
. Dies sagt Ihnen nur, dass Sie mit einer let-Anweisung den Kontext im Wesentlichen mit einer neuen Bindung erweitern können - genau daslet
tut es!Die
[Inst]
Regel behandelt die Untertypisierung. Es heißt, wenn Sie einen Wert vom Typ habenσ'
und es sich um einen Untertyp handeltσ
(⊑
der eine partielle Ordnungsbeziehung darstellt), dann ist dieser Ausdruck auch vom Typσ
.Die letzte Regel befasst sich mit der Verallgemeinerung von Typen. Ein kurzer Hinweis: Eine freie Variable ist eine Variable, die nicht durch eine let-Anweisung oder ein Lambda in einem Ausdruck eingeführt wird. Dieser Ausdruck hängt jetzt vom Wert der freien Variablen aus ihrem Kontext ab. Die Regel besagt, dass, wenn es in Ihrem Kontext eine Variable gibt,
α
die in nichts "frei" ist, jeder Ausdruck, dessen Typ Sie kennen, mit Sicherheit gesagt werden kanne : σ
wird diesen Typ für jeden Wert von habenα
.Wie man die Regeln benutzt
Was machen Sie mit diesen Regeln, nachdem Sie die Symbole verstanden haben? Nun, Sie können diese Regeln verwenden, um die Art der verschiedenen Werte herauszufinden. Schauen Sie sich dazu Ihren Ausdruck an (sagen wir
f x y
) und finden Sie eine Regel, deren Schlussfolgerung (unterer Teil) Ihrer Aussage entspricht. Nennen wir das, was Sie versuchen, Ihr "Ziel" zu finden. In diesem Fall würden Sie sich die Regel ansehen, die mit endete₀ e₁
. Wenn Sie dies gefunden haben, müssen Sie jetzt Regeln finden, die alles über der Linie dieser Regel beweisen. Diese Dinge entsprechen im Allgemeinen den Arten von Unterausdrücken, sodass Sie im Wesentlichen auf Teile des Ausdrucks zurückgreifen. Sie tun dies einfach, bis Sie Ihren Proofbaum fertiggestellt haben, der Ihnen einen Proof für die Art Ihres Ausdrucks gibt.Alles, was diese Regeln tun, ist genau anzugeben - und in den üblichen mathematisch pedantischen Details: P -, wie die Arten von Ausdrücken herauszufinden sind.
Dies sollte Ihnen bekannt vorkommen, wenn Sie jemals Prolog verwendet haben - Sie berechnen den Proof-Baum im Wesentlichen wie einen menschlichen Prolog-Interpreter. Es gibt einen Grund, warum Prolog "Logikprogrammierung" genannt wird! Dies ist auch wichtig, da ich zuerst in den HM-Inferenzalgorithmus eingeführt wurde, indem ich ihn in Prolog implementierte. Das ist eigentlich überraschend einfach und macht klar, was los ist. Sie sollten es auf jeden Fall versuchen.
Hinweis: Ich habe wahrscheinlich einige Fehler in dieser Erklärung gemacht und würde es lieben, wenn jemand darauf hinweisen würde. Ich werde dies in ein paar Wochen im Unterricht behandeln, also bin ich dann sicherer: P.
quelle
Γ = {x : τ}
)λy.x : σ → τ
zu∀ σ. σ → τ
, aber nicht beschränkt auf∀ τ. σ → τ
, weilτ
freier Variable in istΓ
. Wikipedia-Artikel über HM erklärt es ganz nett.[Inst]
ist etwas ungenau. Dies ist nur zu verstehen , mein bisher, aber die Sigmas in den[Inst]
und[Gen]
Regeln beziehen sich nicht auf Typen, sondern Regelungen zu geben . Der⊑
Operator ist also eine Teilreihenfolge, die nichts mit der Untertypisierung zu tun hat, wie wir sie aus OO-Sprachen kennen. Es hängt mit polymorphen Werten wie zusammenid = λx. x
. Die vollständige Syntax für eine solche Funktion wäreid = ∀x. λx. x
. Jetzt können wir natürlich eine habenid2 = ∀xy. λx. x
, woy
nicht verwendet wird. Dannid2 ⊑ id
, was die[Inst]
Regel sagt.Siehe " Praktische Grundlagen von Programmiersprachen ", Kapitel 2 und 3, zum Stil der Logik durch Urteile und Ableitungen. Das gesamte Buch ist jetzt bei Amazon erhältlich.
Kapitel 2
Induktive Definitionen
Induktive Definitionen sind ein unverzichtbares Werkzeug beim Studium von Programmiersprachen. In diesem Kapitel werden wir das Grundgerüst induktiver Definitionen entwickeln und einige Beispiele für deren Verwendung geben. Eine induktive Definition besteht aus einer Reihe von Regeln zum Ableiten von Urteilen oder Behauptungen verschiedener Formen. Urteile sind Aussagen über ein oder mehrere syntaktische Objekte einer bestimmten Art. Die Regeln legen die notwendigen und ausreichenden Bedingungen für die Gültigkeit eines Urteils fest und bestimmen somit dessen Bedeutung vollständig.
2.1 Urteile
Wir beginnen mit dem Begriff eines Urteils oder einer Behauptung über ein syntaktisches Objekt. Wir werden viele Formen des Urteils anwenden, einschließlich solcher Beispiele:
Ein Urteil besagt, dass ein oder mehrere syntaktische Objekte eine Eigenschaft haben oder in irgendeiner Beziehung zueinander stehen. Die Eigenschaft oder Beziehung selbst wird als Urteilsform bezeichnet , und das Urteil, dass ein Objekt oder Objekte diese Eigenschaft haben oder in dieser Beziehung stehen, wird als Instanz dieser Urteilsform bezeichnet. Eine Urteilsform wird auch als Prädikat bezeichnet , und die Objekte, die eine Instanz bilden, sind ihre Subjekte . Wir schreiben ein J für das Urteil, das besagt , dass J von a gilt . Wenn es nicht wichtig ist, das Thema des Urteils zu betonen (Text wird hier abgeschnitten)
quelle
Wie verstehe ich die Hindley-Milner-Regeln?
Hindley-Milner ist ein Regelwerk in Form eines sequentiellen Kalküls (kein natürlicher Abzug), das zeigt, dass wir den (allgemeinsten) Typ eines Programms aus der Erstellung des Programms ohne explizite Typdeklarationen ableiten können.
Die Symbole und Notation
Lassen Sie uns zunächst die Symbole erläutern und die Priorität des Operators erörtern
𝜆𝑥.𝑒 bedeutet, dass 𝜆 (Lambda) eine anonyme Funktion ist, die ein Argument 𝑥 verwendet und einen Ausdruck 𝑒 zurückgibt .
sei 𝑥 = 𝑒₀ in 𝑒₁ bedeutet im Ausdruck 𝑒₁ , ersetze 𝑒₀ wo immer 𝑥 erscheint.
⊑ bedeutet, dass das vorherige Element ein Subtyp (informell - Unterklasse) des letzteren Elements ist.
Alles über der Linie ist die Prämisse, alles darunter ist die Schlussfolgerung ( Per Martin-Löf )
Vorrang, zum Beispiel
Ich habe einige der komplexeren Beispiele aus den Regeln genommen und redundante Klammern eingefügt, die Vorrang haben:
𝚪 ⊦ 𝑥 : 𝜎 könnte geschrieben werden 𝚪 ⊦ ( 𝑥 : 𝜎 )
𝚪 ⊦ sei 𝑥 = 𝑒₀ in 𝑒₁ : 𝜏 ist äquivalent 𝚪 ⊦ (( sei ( 𝑥 = 𝑒₀ ) in 𝑒₁ ): 𝜏 )
𝚪 ⊦ 𝜆𝑥.𝑒 : 𝜏 → 𝜏 ' ist äquivalent 𝚪 ⊦ (( 𝜆𝑥.𝑒 ): ( 𝜏 → 𝜏' ))
Dann zeigen große Räume, die Assertionsaussagen und andere Voraussetzungen trennen, eine Reihe solcher Voraussetzungen an, und schließlich bringt die horizontale Linie, die Prämisse von Schlussfolgerung trennt, das Ende der Rangfolge.
Die Regeln
Was hier folgt, sind englische Interpretationen der Regeln, denen jeweils eine lose Anpassung und eine Erklärung folgen.
Variable
Anders ausgedrückt, in 𝚪 wissen wir, dass 𝑥 vom Typ 𝜎 ist, weil 𝑥 vom Typ 𝜎 in 𝚪 ist.
Dies ist im Grunde eine Tautologie. Ein Bezeichnername ist eine Variable oder eine Funktion.
Funktionsanwendung
Um die Regel neu zu formulieren, wissen wir, dass die Funktionsanwendung den Typ 𝜏 'zurückgibt, da die Funktion den Typ 𝜏 → 𝜏' hat und ein Argument vom Typ 𝜏 erhält.
Dies bedeutet, dass wenn wir wissen, dass eine Funktion einen Typ zurückgibt und wir ihn auf ein Argument anwenden, das Ergebnis eine Instanz des Typs ist, von dem wir wissen, dass er zurückgibt.
Funktionsabstraktion
Wenn wir wieder eine Funktion sehen, die 𝑥 nimmt und einen Ausdruck 𝑒 zurückgibt, wissen wir, dass sie vom Typ 𝜏 → 𝜏 'ist, weil 𝑥 (a 𝜏) behauptet, dass 𝑒 ein 𝜏' ist.
Wenn wir wissen, dass 𝑥 vom Typ 𝜏 ist und somit ein Ausdruck 𝑒 vom Typ 𝜏 'ist, dann ist eine Funktion von 𝑥, die den Ausdruck 𝑒 zurückgibt, vom Typ 𝜏 → 𝜏'.
Lassen Sie die Variablendeklaration
Locker ist 𝑥 in 𝑒₁ (a 𝜏) an 𝑒₀ gebunden, weil 𝑒₀ ein 𝜎 ist und 𝑥 ein 𝜎 ist, das behauptet, 𝑒₁ sei ein 𝜏.
Das heißt, wenn wir einen Ausdruck 𝑒₀ haben, der ein 𝜎 ist (eine Variable oder eine Funktion), und einen Namen 𝑥, auch ein 𝜎, und einen Ausdruck 𝑒₁ vom Typ 𝜏, dann können wir 𝑒₀ für 𝑥 ersetzen, wo immer er im Inneren erscheint von 𝑒₁.
Instanziierung
Ein Ausdruck 𝑒 ist vom übergeordneten Typ 𝜎, da der Ausdruck 𝑒 vom Subtyp 𝜎 'und 𝜎 vom übergeordneten Typ von 𝜎' ist.
Wenn eine Instanz von einem Typ ist, der ein Subtyp eines anderen Typs ist, dann ist es auch eine Instanz dieses Supertyps - des allgemeineren Typs.
Verallgemeinerung
Im Allgemeinen wird 𝑒 für alle Argumentvariablen (𝛼) eingegeben, die 𝜎 zurückgeben, da wir wissen, dass 𝑒 ein 𝜎 und 𝛼 keine freie Variable ist.
Dies bedeutet, dass wir ein Programm verallgemeinern können, um alle Typen für Argumente zu akzeptieren, die nicht bereits im enthaltenen Bereich gebunden sind (Variablen, die nicht lokal sind). Diese gebundenen Variablen sind austauschbar.
Alles zusammenfügen
Unter bestimmten Voraussetzungen (z. B. keine freien / undefinierten Variablen, eine bekannte Umgebung) kennen wir die Arten von:
Fazit
Diese Regeln zusammen ermöglichen es uns, den allgemeinsten Typ eines behaupteten Programms zu beweisen, ohne dass Typanmerkungen erforderlich sind.
quelle
Die Notation stammt aus dem natürlichen Abzug .
⊢ Symbol heißt Drehkreuz .
Die 6 Regeln sind sehr einfach.
Var
Die Regel ist eine eher triviale Regel. Wenn in Ihrer Typumgebung bereits ein Typ für einen Bezeichner vorhanden ist, nehmen Sie ihn einfach aus der Umgebung, um auf den Typ zu schließen.App
Die Regel besagt, dass Sie den Anwendungstyp ableiten können , wenn Sie zwei Bezeichner habene0
unde1
deren Typ ableiten könnene0 e1
. Die Regel lautet wie folgt: Wenn Sie dase0 :: t0 -> t1
unde1 :: t0
(das gleiche t0!) Wissen, ist die Anwendung gut typisiert und der Typ istt1
.Abs
undLet
sind Regeln, um Typen für Lambda-Abstraktion und Einlass abzuleiten.Inst
Die Regel besagt, dass Sie einen Typ durch einen weniger allgemeinen ersetzen können.quelle
Es gibt zwei Möglichkeiten, sich e vorzustellen: σ. Einer ist "der Ausdruck e hat den Typ σ", ein anderer ist "das geordnete Paar des Ausdrucks e und des Typs σ".
Betrachten Sie Γ als das Wissen über die Arten von Ausdrücken, implementiert als eine Menge von Ausdrucks- und Typpaaren, e: σ.
Das Drehkreuz ⊢ bedeutet, dass wir aus dem Wissen auf der linken Seite ableiten können, was auf der rechten Seite ist.
Die erste Regel [Var] kann also gelesen werden:
Wenn unser Wissen Γ das Paar e: σ enthält, können wir aus Γ ableiten, dass e den Typ σ hat.
Die zweite Regel [App] kann gelesen werden:
Wenn wir aus Γ ableiten können, dass e_0 den Typ τ → τ 'hat, und wir aus Γ ableiten können, dass e_1 den Typ τ hat, dann können wir aus Γ ableiten, dass e_0 e_1 den hat Typ τ '.
Es ist üblich, Γ, e: σ anstelle von Γ Γ {e: σ} zu schreiben.
Die dritte Regel [Abs] kann also gelesen werden:
Wenn wir aus Γ mit x: τ erweitern können, dass e den Typ τ 'hat, dann können wir aus Γ ableiten, dass λx.e den Typ τ → τ' hat.
Die vierte Regel [Let] bleibt als Übung übrig. :-)
Die fünfte Regel [Inst] kann gelesen werden:
Wenn wir aus Γ ableiten können, dass e den Typ σ 'hat und σ' ein Subtyp von σ ist, können wir aus Γ ableiten, dass e den Typ σ hat.
Die sechste und letzte Regel [Gen] kann gelesen werden:
Wenn wir aus Γ ableiten können, dass e den Typ σ hat und α in keinem der Typen in Γ eine freie Typvariable ist, können wir aus Γ ableiten, dass e den Typ hat ∀α σ.
quelle