Wie lese ich Schreibregeln?

Question

Ich begann immer mehr Sprachforschungsarbeiten zu lesen. Ich finde es sehr interessant und eine gute Möglichkeit, mehr über das Programmieren im Allgemeinen zu erfahren. Es gibt jedoch normalerweise einen Abschnitt, mit dem ich immer Probleme habe (zum Beispiel Teil drei von Nehmen Dies) Da ich den theoretischen Hintergrund in Informatik fehlt: Typregeln.

Gibt es gute Bücher oder Online -Ressourcen für den Einstieg in diesem Bereich? Wikipedia ist unglaublich vage und hilft einem Anfänger nicht wirklich.

Answer 1

In den meisten Typsystemen arbeiten die Typregeln zusammen, um Urteile der Form zu definieren:

$$ gamma vdash e: tau $$

Dies besagt, dass der Ausdruck $ e $ im Kontext $ gamma $ $ $ tau $ hat.
$ Gamma $ ist eine Zuordnung der kostenlosen Variablen von $ e $ an ihre Typen.

Ein Typsystem besteht aus einer Reihe von Axiomen und Regeln (ein formales System von Inferenzregeln, wie Raphael betont).

Ein Axiom ist von der Form

$$ dfrac {} { gamma vdash e: tau} $$

Dies besagt, dass das Urteil $ gamma vdash e: tau $ (immer) gilt.

Ein Beispiel ist

$$ dfrac {} {x: tau vdash x: tau} $$

Dies besagt, dass unter der Annahme, dass die Art der Variablen $ x $ $ Tau $ ist, der Ausdruck $ x $ $ Tau $ hat.

Inferenzregeln nehmen Fakten an, die bereits ermittelt wurden, und bauen größere Fakten von ihnen auf. Zum Beispiel die Inferenzregel

acht

sagt, wenn ich eine Ableitung der Tatsache habe $ gamma vdash e_1: tau to tau Fakt $ gamma vdash e_1 e_2: tau '$. In diesem Fall ist dies die Regel für die Typisierungsfunktionsanwendung.

Es gibt zwei Möglichkeiten, diese Regel zu lesen:

• Top -Down - Bei zwei Ausdrücken (eine Funktion und einem anderen Ausdruck) und einigen Einschränkungen für ihren Typ können wir einen anderen Ausdruck (die Anwendung der Funktion auf den Ausdruck) mit dem gegebenen Typ konstruieren.
• Bottom -up - Bei einem Ausdruck, der in diesem Fall die Anwendung einer Funktion auf einen Ausdruck ist, wird die Art und Weise, wie dies getippt wird Funktionstyp und die zweite hat den Argumentyp der Funktion.

Einige Inferenzregeln manipulieren auch $ gamma $, indem neue Zutaten in sie hinzugefügt werden (Bottom-up). Hier ist die Regel für $ lambda $ -abstraktion:

acht

Die Inferenzregeln werden induktiv angewendet, basierend auf der Syntax des Expression, der als Ableitungstaum angesehen wird. An den Blättern des Baumes (oben) sind Axiome und Zweige werden durch Anwenden von Inferenzregeln gebildet. Ganz im Boden des Baumes befindet sich der Ausdruck, an dem Sie interessiert sind.

Zum Beispiel ist eine Ableitung der Typisierung des Ausdrucks $ lambda f. Lambda xf x $ ist

$$dfrac{dfrac{}{f:tautotau',x:tauvdash f:tautotau'} qquad dfrac{}{f:tauto Tau ', x: tau vdash x: tau}} { dfrac {f: tau to tau', x: tau vdash f x: tau '} { dfrac {f: Tau to Tau ' vdash lambda xf x: tau'} { vdash lambda f.

• Typen und Programmiersprachen Von Benjamin Pierce
• Praktische Grundlagen für Programmiersprachen Von Robert Harper

Beide Bücher sind sehr umfassend und beginnen langsam und bauen eine solide Grundlage auf.

Answer 2

Es gibt ein süßes interaktives Online -Tutorial für Sequent Calculus, was dazu beitragen kann, einige Intuitionen aufzubauen und zu spüren, wie Inferenz funktioniert:Ein interaktives Tutorial des Sequenzkalküls

Answer 3

Auf dieser Wikipedia -Seite wird es empfohlen "Typsysteme, Luca Cardelli, ACM Computing -Umfragen", Es ist eine 2-Seiten-Umfrage, die Ihnen helfen kann zu verstehen, wie man eine Regel liest. Wie auch immer, wie man eine Regel liest Das Ganze, Sie müssen verstehen, was ein Schreibsystem ist (zusammengesetzt aus mehreren Regeln), für das das "Typ System"Wikipedia -Artikel ist ein guter Anfang (und Sie haben mehrere Bücher im Abschnitt"Verweise"Von dieser Seite, wenn Sie weiter gehen möchten).