Ist die kontextuelle Äquivalenz einer Sprache mit `quote`-`eval` trivial oder nicht?

In [1] demonstrierte Mitchell Wand, dass das Hinzufügen von fexprs zum reinen Lambda-Kalkül die Theorie der kontextuellen Äquivalenz trivialisiert, was bedeutet, dass zwei Terme kontextuell äquivalent sind, wenn sie kongruent sind. Als er verwandte Arbeiten untersuchte, ging er davon aus, dass "unser Ergebnis eine alte Beobachtung von Albert Meyer [2] erweitert und die kontextuelle Äquivalenz trivial macht". Unter Bezugnahme auf [2] konnte jedoch nur die folgende Aussage von Meyer gefunden werden:$\alpha$evalquote

Ich dachte zuerst, dass es in Sprachen mit einer quote- evalFunktion wie LISP [3] keine Typunterscheidung zwischen syntaktischen und ausführbaren Objekten gibt. Tatsächlich quote- evalscheint in LISP sicher genug zu sein, da es, obwohl es quotesyntaktisch wie ein vertrauenswürdiger Operator aussieht cond, sich wirklich nicht wie einer verhält (es hat nur Verhalten zur Analysezeit, keine Laufzeit, z. B. kann man nicht übergeben quoteals Parameter zu einer Prozedur). Trotzdem habe ich noch überzeugende Beispiele gesehen, bei denen sich die quote- evalFunktion gelohnt hat.

Unabhängig von einem kleinen Fehler in diesen Kommentaren, der den Leser irreführen condkönnte, daraus zu schließen, dass er als Parameter an eine Prozedur übergeben werden könnte. Wenn ich richtig verstehe, bedeutet das, was Meyer sagte " quote- evalscheint sicher genug", dass quote- evaldie Gleichungstheorie möglicherweise nicht trivialisiert wird, obwohl er keinen Beweis angeboten hat.

BEARBEITEN:

Da sich alle drei Papiere mit den Sprachen der LISP-Familie befassen, wollen wir die Frage, wie von Martin angeregt, unter denselben Umständen stellen. Ist die kontextuelle Gleichwertigkeit einer Sprache mit quote- evalinsbesondere LISP - auf der Erde trivial oder nicht?

[1] Mitchell Wand, The Theory of Fexprs ist trivial . Lisp and Symbolic Computation 10 (3): 189-199 (1998).

[2] Albert Meyer, Puzzles in Programming Logic Workshop zur formalen Softwareentwicklung. 1984

[3] John McCarthy, rekursive Funktionen der symbolischen Ausdrucksformen und deren Berechnung von Maschinen Teil I . Mitteilungen der ACM im April 1960.

Erstens hängt dies ganz davon ab, was Sie als Ihre Kontexte ansehen. Wenn (quote [])es sich um einen Kontext handelt, ist die Kontextäquivalenz die syntaktische Äquivalenz.

Traditionsgemäß werden Kontexte für kontextuelle Äquivalenz als Kontexte verstanden, in denen "Ausdrücke" in jeder in der Sprache vorhandenen Bedeutung auftreten können. Dies "[]"schließt Kontexte wie aus , in denen der Kontext sein Argument in ein String-Literal einfügt. Diese Art von Kontexten wurde auch von Quine ausgeschlossen, als er ursprünglich referentielle Transparenz beschrieb.

Aus dieser Perspektive denke ich (quote [])ist auch kein Kontext. Stattdessen sind die Kontexte die Stellen, an denen möglicherweise eine Ausdrucksbewertung stattfinden kann, z. B. im Hauptteil einer Funktion oder im Argument einer Anwendung.

Potenziell problematisch bedeutet dies, dass Sie in einem Lisp-Programm mit Makros (oder einem Racket- oder Scheme-Programm) die Kontexte erst kennen, wenn Sie den potenziell nicht abschließenden Makroerweiterungsprozess ausführen, da Sie nicht einmal wissen, wo die Ausdrücke sind sind. Ob Sie dies für ein Problem halten oder nicht, ist eher eine philosophische als eine technische Frage.