Is contextual equivalence of a language with `quote`-`eval` trivial or not?

Question

In [1], Mitchell Wand demonstrated that adding fexprs to the pure lambda calculus trivializes the theory of contextual equivalence, meaning two terms are contextually equivalent iff they are $\alpha$-congruent. When exploring related work, he went "our result extends an old observation of Albert Meyer [2] that evaland quote render contextual equivalence trivial". But referring to [2], what could be found is only the following statement by Meyer:

I first thought that in languages with a quote-eval feature such as LISP [3] there was no type distinction between syntactic and executable objects. In fact quote-eval seems safe enough in LISP because, although quote syntactically looks like a bona fide operator, like say cond, it really doesn’t behave like one (it only has behavior at parse time, not run time, e.g., one can't pass quote as a parameter to a procedure). Still, I have yet to see convincing examples where the quote-eval feature was worthwhile.

Regardless of one minor flaw in these comments that may mislead the reader to infer that cond could be passed as a parameter to a procedure. If I understand correctly, what Meyer said "quote-eval seems safe enough" means that quote-eval may not trivialize the equational theory, although he did not offer a proof.

EDIT:

As suggested by Martin, since all the three papers cited dealing with LISP family languages, let's put the question under this same setting. Is contextual equivalence of a language with quote-eval, in particular LISP, on earth trivial or not?

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

[2] Albert Meyer, Puzzles in Programming Logic Workshop on Formal Software Development. 1984

[3] John McCarthy, Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I. Communications of the ACM in April 1960.

Answer 1

First, this entirely depends on what you take to be your set of contexts. If (quote []) is a context, then contextual equivalence is syntactic equivalence.

Traditionally, contexts for contextual equivalence are taken to be contexts in which "expressions", in whatever meaning that has in the language, can appear. This rules out contexts like "[]", where the context places its argument inside a string literal. These kinds of contexts were also, IIRC, ruled out by Quine when he originally described referential transparency.

From this perspective, I think (quote []) is also not a context. Instead, the contexts are the places where expression evaluation could potentially happen, such as in the body of a function or in the argument of an application.

Potentially problematically, this means that in a Lisp program with macros (or a Racket or Scheme program) you don't know what the contexts are until you run the potentially-nonterminating macro expansion process, because you don't even know where the expressions are. Whether you think this is a problem or not is mostly a philosophical question rather than a technical one.