Ich weiß, dass verschiedene Autoren unterschiedliche Schreibweisen verwenden, um die Semantik der Programmiersprache darzustellen. In der Tat spricht Guy Steele dieses Problem in einem interessanten Video an .
Ich würde gerne wissen, ob jemand weiß, ob der führende Drehkreuzbetreiber eine allgemein anerkannte Bedeutung hat. Zum Beispiel verstehe ich den führenden Operator am Anfang des Nenners von Folgendem nicht:
Kann mir jemand helfen zu verstehen? Vielen Dank.
type-theory
denotational-semantics
Jim Newton
quelle
quelle
type-checking
Antworten:
Auf der linken Seite des Drehkreuzes finden Sie den lokalen Kontext, eine endliche Liste von Annahmen über die Arten der zur Verfügung stehenden Variablen.
Oben, kann gleich Null sein, was zu ⊢ e : T . Dies bedeutet, dass keine Annahmen zu Variablen getroffen werden. Normalerweise bedeutet dies, dass e ein geschlossener Term (ohne freie Variablen) vom Typ T ist .n ⊢e:T e T
Häufig wird die von Ihnen erwähnte Regel allgemeiner formuliert, wobei es mehr Hypothesen geben kann als die in der Frage erwähnte.
Hier steht für einen beliebigen Kontext, und Γ steht x : T 1 für seine Erweiterung, die durch Anhängen der zusätzlichen Hypothese x : T 1 an die Liste Γ erhalten wird . Es ist üblich , zu verlangen , dass x nicht in erschien Γ , so dass die Erweiterung nicht „Konflikt“ mit einer früheren Annahme.Γ Γ,x:T1 x:T1 Γ x Γ
quelle
Beachten Sie als Ergänzung zu den anderen Antworten, dass es drei Ebenen der "Implikation" bei der Typisierung von Ableitungen gibt. Und die gleiche Bemerkung gilt für logische Ableitungen, da es tatsächlich eine Entsprechung zwischen den beiden gibt (die als Curry-Howard-Korrespondenz bezeichnet wird).
Die erste Implikation ist der Pfeil, der in Formeln erscheint und der logischen Implikation in einer Formel (oder einem Funktionstyp für den Kalkül) entspricht.λ
Die zweite Implikation wird durch das Drehkreuzsymbol materialisiert und bedeutet "unter der Annahme, dass jede Formel auf der linken Seite gilt, gilt die Formel auf der rechten Seite". Insbesondere sagt die Regel, die Sie geben, wie man eine Implikation beweisen soll: Um zu beweisen , muss man B unter der Annahme beweisen, dass A gilt. In Bezug auf den λ- Kalkül, um zu beweisen, dass λ x . t hat den Typ A → B , man muss zeigen, dass t den Typ B hat , vorausgesetzt, x ist eine Variable vom Typ A (siehe die Entsprechung?).A⇒B B A λ λx.t A→B t B x A
Die dritte Implikationsebene wird durch den horizontalen Balken materialisiert und bedeutet "Wenn jede Prämisse (Elemente oben) gilt, gilt die Schlussfolgerung (das Element unten)". Sie können dies mit der Interpretation der von Ihnen angegebenen Typisierungsregel für die -Abstraktion verknüpfen (siehe die Erläuterung im vorherigen Absatz).λ
quelle
In repräsentiert ( ⊢ ) die ternäre Beziehung über Typumgebungen , Ausdrücke und Typen: ⊢ E n v × E x p × T y p .⊢ ⊢Env×Exp×Typ
In Ihrem Beispiel ist der Ausdruck Typ T 2 wrt. auf eine Typumgebung mit einer Typannahme, die T 1 auf eine Typvariable x abbildett2 T2 T1 x
In diesem Zusammenhang ist eine Typ - Umgebung eine Teilfunktion , dass Abtretungstypen Variablen, in der Regel mit bezeichnet wobei Γ ∈ E n V : V a r ⇀ T y pΓ Γ∈Env:Var⇀Typ
Es ist zu beachten, dass der Betreiber seine Funktionalität unabhängig davon behält, wo sie auftaucht, entweder in der Prämisse oder im Abschluss der Regel.
quelle
In jeder Situation, die ich gesehen habe, bedeutet , dass es einen Beweis dafür gibt , dass Y angenommen hat, dass X gilt. Wenn X leer ist, bedeutet dies, dass Y eine Tautologie ist: Es gibt einen Beweis, ohne dass Annahmen erforderlich sind.X⊢Y Y X X Y
quelle