Was ist der Unterschied zwischen Moggis rechnergestützter Metasprache und Moggis Lambda-Kalkül?

Dies ist eine Referenzverwirrung. Manchmal sehe ich Leute, die den Begriff "Moggis rechnergestützte Metasprache" verwenden, um sich auf den von Moggi vorgestellten Kalkül zu beziehen, und manchmal auf "Moggis rechnergestütztes Lambda-Kalkül". Manchmal verwenden sie und manchmal .$\lambda_{ml}$$\lambda_c$

Ich habe immer angenommen, dass beide dasselbe sind, aber wenn ich die Zusammenfassung eines Vortrags von Katsumata und Moegelberg lese, heißt es :

Wir zeigen die Fülle von Moggis monadischer Übersetzung vom rechnerischen Lambda-Kalkül mit Summen zur rechnergestützten Metasprache mit Summen unter Verwendung des TT- und TT-Closure-Operators.$\lc$$\lml$

Sind diese Sprachen nicht dasselbe? Wo werden sie speziell mit diesen Namen eingeführt? Es scheint, als würde Moggi manchmal über das Modell für eine sogenannte Metasprache , aber in einem anderen spricht er über die rechnergestützte Lambda-Berechnung.$\lambda_c$

Die Terminologie kann etwas verwirrend sein, aber es gibt zwei Sprachen, zum Beispiel in Moggis "Vorstellungen von Berechnungen als Monaden" (kostenloser Link hier: https://core.ac.uk/download/pdf/21173011.pdf ).

In diesem Artikel werden die Sprachen als $\lambda_{ml}$ , die Metasprache, und $\lambda_{pl}$ als "Programmiersprache" bezeichnet. Ich glaube, $\lambda_{pl}$ spielt die Rolle des rechnerischen Lambda-Kalküls, aber ich kann mich irren. Ein verwirrender Aspekt ist, dass beide Sprachen einen expliziten Typkonstruktor $T$ der die Monade darstellt, aber unterschiedlich verwendet werden.

$\lambda_{ml}$ ist eine "reine" Sprache mit einer Monade$T$ , dh jede Manipulation der Monade ist in den Typen explizit und der Funktionstyp$\tau_1 \to \tau_2$ ist der Typ der reinen Funktionen. Beachten Sie die Bindungsregel (aus Abbildung 3 auf Seite 9):

$$\frac{x : \tau \vdash_{ml} e_1 : T \tau_1 \quad x_1 : \tau_1 \vdash_{ml} e_2 : T \tau_2 } {x :\tau \vdash_{ml} let_T x_1 \Leftarrow e_1 in e_2 : T \tau_2}$$

$e_1$ und$e_2$ werden explizit als Terme von$T \tau_1, T\tau_2$ typisiert , um zu markieren, dass sie wirksam sind. Jeder wirksame Ausdruck ist wirklich ein reiner Begriff mit monadischem Typ. Dies ähnelt der Art und Weise, wie wir mit Monaden in Haskell programmieren, wobei Haskell die Rolle der Metasprache spielt und die Monade Effekte codiert, aber tatsächlich manipulieren wir immer "reine" Begriffe (ich setze "rein" in Anführungszeichen, da Haskell seine eigenen Divergenzeffekte hat und Fehler).

Wir können dies in der Semantik der Metasprache sehen: Ein Term $x:\tau \vdash_{ml} e : \tau'$ bezeichnet einen Morphismus $[\tau] \to [\tau']$ , die Monade entsteht nur, wenn wir ihn erwähnen.

Andererseits soll $\lambda_{pl}$ eine effektive Call-by-Value-Programmiersprache sein. Als solcher Term ist $x : \tau \vdash_{pl} e : \tau'$ ein möglicherweise wirksamer Term, der Werte vom Typ $\tau'$ zurückgibt , ähnlich wie Sprachen wie SML und OCaml. Deshalb wird in der Arbeit der Funktionstyp $\tau \rightharpoonup \tau'$ geschrieben , weil es sich um die Art der effektiven Funktionen handelt, nicht um reine Funktionen.

Vergleichen Sie hier die Bindungsregel (aus Abbildung 5 auf Seite 11):

$$\frac{x : \tau \vdash_{pl} e_1 : \tau_1 \quad x_1 : \tau_1 \vdash_{pl} e_2 : \tau_2 } {x :\tau \vdash_{pl} let x_1 \Leftarrow e_1 in e_2 : \tau_2}$$

$e_2$$x : \tau \vdash_{pl} e : \tau'$$[\tau] \to T[\tau']$

$\lambda_{pl}$ enthält einen expliziten Monadenkonstruktor$T$ , den SML und OCaml nicht als Konstruktor vom primitiven Typ haben, weil$T a$ äquivalent zuunit -> aweil->bedeutet effektive Funktion bedeutet.