Czy kontekstowa równoważność języka z `quote`-`eval` jest trywialna, czy nie?

W [1] Mitchell Wand wykazał, że dodanie fexprs do czystego rachunku lambda trywializuje teorię równoważności kontekstowej, co oznacza, że ​​dwa terminy są równoważne kontekstowo, jeśli są zgodne. Badając pokrewną pracę, stwierdził: „nasz wynik rozszerza starą obserwację Alberta Meyera [2] i czyni banalną równoważność kontekstową”. Ale odnosząc się do [2], można znaleźć tylko następujące oświadczenie Meyera:$\alpha$evalquote

Najpierw pomyślałem, że w językach z funkcją quote- evaltaką jak LISP [3] nie było rozróżnienia typów między obiektami składniowymi i wykonywalnymi. W rzeczywistości quote- evalwydaje się wystarczająco bezpieczny w LISP, ponieważ chociaż quotesyntaktycznie wygląda jak operator bona fi de, powiedzmy cond, tak naprawdę nie zachowuje się jak jeden (ma zachowanie tylko w czasie analizy, a nie w czasie wykonywania, np. Nie można przejść quotejako parametr procedury). Nadal jednak nie widziałem przekonujących przykładów, w których warto było skorzystać z funkcji quote- eval.

Niezależnie od jednej drobnej wady w tych komentarzach, która może wprowadzić czytelnika w błąd, aby wywnioskować, że condmożna go przekazać jako parametr procedury. Jeśli dobrze rozumiem, to, co powiedział Meyer „ quote- evalwydaje się wystarczająco bezpieczny” oznacza, że quote- evalmoże nie trywializować teorii równań, chociaż nie przedstawił dowodu.

EDYTOWAĆ:

Jak zasugerował Martin, ponieważ wszystkie trzy artykuły cytowały dotyczące języków rodzinnych LISP, postawmy pytanie w tym samym otoczeniu. Czy kontekstowa równoważność języka z quote- evalw szczególności LISP - na ziemi jest trywialna, czy nie?

[1] Różdżka Mitchella, teoria Fexprsa jest banalna . Lisp and Symbolic Computation 10 (3): 189-199 (1998).

[2] Albert Meyer, Warsztaty logiczne dotyczące programowania logicznego na temat formalnego tworzenia oprogramowania. 1984

[3] John McCarthy, rekurencyjne funkcje symbolicznego wyrazu i obliczeniach przez maszynę, część I . Komunikat ACM w kwietniu 1960 r.

Po pierwsze, zależy to całkowicie od tego, co uważasz za swój zestaw kontekstów. Jeśli (quote [])jest kontekstem, to równoważność kontekstowa jest równoważnością składniową.

Tradycyjnie kontekstami równoważności kontekstu są konteksty, w których mogą pojawiać się „wyrażenia” w dowolnym znaczeniu, jakie ma język. Wyklucza to takie konteksty "[]", w których kontekst umieszcza swój argument w dosłownym ciągu znaków. Tego rodzaju konteksty zostały również, IIRC, wykluczone przez Quine'a, gdy pierwotnie opisywał przejrzystość referencyjną.

Z tej perspektywy myślę, że (quote [])również nie jest kontekstem. Zamiast tego konteksty to miejsca, w których potencjalnie może nastąpić ocena wyrażenia, na przykład w treści funkcji lub w argumencie aplikacji.

Potencjalnie problematycznie oznacza to, że w programie Lisp z makrami (lub w programie Racket lub Scheme) nie wiesz, jakie są konteksty, dopóki nie uruchomisz potencjalnie niekończącego się procesu ekspansji makr, ponieważ nawet nie wiesz, gdzie są wyrażenia są. To, czy uważasz, że jest to problem, czy nie, jest głównie pytaniem filozoficznym, a nie technicznym.