Frage zur „Tutorial-Implementierung der abhängig typisierten Lambda-Kalküle“

Question

Ich habe ein leichtes technisches Problem damit Das wunderbares Tutorial.Auf Seite 5 spricht das Tutorial über Typisierungsregeln für Simply Typed Lambdas und präsentiert die folgende Beurteilung, wie sie über die Regeln in Abbildung 3 abgeleitet werden kann.

Ich konnte weder das eine noch das andere beweisen id noch const Aus dem gleichen Grund.Nehmen Sie zum Beispiel die id Beispiel.

• Angenommen, ich suche nach einer Typprüfungsregel CHK.Das heißt, um check types Ich sollte zuerst eine Schlussfolgerung ziehen und dann das Ergebnis mit meinen Erwartungen vergleichen.
• Um die Schlussfolgerung auf die Anwendung zu ziehen, muss ich die verwenden APP Regel, die mich sofort dazu zwingt, auf den Typ der linken Seite der Anwendung zu schließen, nämlich (id :: α -> α)
• Dazu verwende ich die ANN Regel, die mich zwingt, das zu überprüfen α -> α ist ein Typ (und ich kann es problemlos beweisen).Dann habe ich das nackt gemacht id Symbol und müssen beweisen, dass es sich um einen Typ handelt α -> α.
• Schließlich gibt es hier ein Problem.Dazu muss ich verwenden var Regel, die den Typ von erfordert id explizit in den Kontext Gamma gesetzt werden, dies geschieht jedoch nicht, daher fällt der Beweis auseinander.

Answer 1

$\mathsf{id}$ Und $\mathsf{const}$ sind keine Variablen des Kalküls, sondern syntaktischer Zucker für $\lambda x ightarrow x$ Und $\lambda x ightarrow \lambda y ightarrow x$ jeweils.Dies wird am Ende von §2.2 angegeben und durch die Verwendung einer serifenlosen Schriftart anstelle von Kursivschrift auf subtile Weise zum Ausdruck gebracht (dies ist eine typografische Konvention dieses bestimmten Dokuments, keine allgemeine Konvention).

So zum Beispiel das Typenurteil$$ alpha ::\ast, y ::\alpha \vdash (\mathsf{id} ::\alpha ightarrow \alpha) \:y ::rightarrow alpha $$ist auch das Typurteil$$ alpha ::\ast, y ::\alpha \vdash (\lambda x ightarrow x ::\alpha ightarrow \alpha) \:y ::rightarrow alpha.$$Es ist eine andere Notation für dasselbe mathematische Objekt.