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

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 ﬁrst 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 ﬁde 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.

• I would suggest to consider if you could make the question more specific: there are different ways of implementing eval/quote like constructs, and various options in designing contextual equivalences for such calculi. An interesting recent related publication is Reasoning About Multi-Stage Programs by Inoue, Taha. Nov 1 '12 at 22:06
• The key distinction is between CTMP (compile-time meta-programming, as exemplified by Template Haskell, Lisp/Scheme/Racket and Converge, and RTMP (run-time meta-programming such as Javascript's eval, or MetaOCaml). Another parameter is typing. Here is an overview talk I gave a few months back on this subject, quite shallow I'm afraid. Regarding contextual equivalences, little work has been done, mostly owning to the fluid state of programming support for meta-programming. Nov 2 '12 at 11:44
• @ plmday: BTW, the idealised programming language Wand formalises in the The Theory of Fexprs Is Trivial is quite different from the meta-programming Lisp does. The former is RTMP, the latter (depending on concrete implementations) is not. Nov 2 '12 at 13:22
• @MartinBerger: Can you post your talk as pdf? Nov 2 '12 at 13:35
• @ Dave Clarke, sure, here it is! Feedback welcome. Nov 2 '12 at 13:57

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.

• I do think there is one way to exclude (quote []), rather than wishful thinking, as a context: dismissing the idea of treating 'datum as syntactic sugar for (quote datum), then '[], as "[]" is no longer a context. Scheme macros have obscured quote anyway.
– day
Mar 23 '14 at 13:30
• I don't understand your comment, @day. Why does the relationship between 'datum and (quote datum) change anything? Mar 23 '14 at 19:34
• If quote is a language construct and 'datum desugars to (quote datum), people will more likely argue that (quote []) is a context. If we remove quote from the core language, but support the literal 'datum syntax, then they will less likely argue so because the similar "[]" is well known to be not a context.
– day
Mar 23 '14 at 21:33
• @day, this is a misunderstanding. There's no one right definition of "context". It's just that different contexts support different notions of contextual equivalence. For example, whitespace is semantically significant in the "[]" context, but not in the (quote []) context. What "people" might argue is neither here nor there. Mar 23 '14 at 22:03
• I agree that there is no one right definition of context. But there is one traditional definition based on abstract syntax, the one that Wand uses in his paper and Meyer uses in his article, to question the status of contextual equivalence of Lisp. What you suggested is replacing traditional definition of context with evaluation context. What I suggested is keeping the traditional definition of context, removing quote from the abstract syntax, but supporting the (concrete) literal syntax of (space-insignificant) quotation. From what I can see, both ways lead to "No" to the original question.
– day
Mar 23 '14 at 22:26