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

<p>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 <code>"[]"</code>, 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.</p>

<p>From this perspective, I think <code>(quote [])</code> 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. </p>

<p>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.</p>

CC BY-SA 3.0
2014-03-23T13:30:59.033Z
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
CC BY-SA 3.0
2014-03-23T19:34:42.663Z
I don't understand your comment, @day. Why does the relationship between `'datum` and `(quote datum)` change anything?
Sam Tobin-Hochstadt
CC BY-SA 3.0
2014-03-23T21:33:36.120Z
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
CC BY-SA 3.0
2014-03-23T22:03:34.200Z
@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.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2014-03-23T22:26:30.553Z
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
CC BY-SA 3.0
2014-03-24T02:31:27.980Z
@day, the definition Wand gives is the same as the one I suggest.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2014-03-24T10:30:06.670Z
Are you sure? I rechecked the paper. What I see is context $C$ used in contextual equivalence is different from reduction context $R$.
day
CC BY-SA 3.0
2014-03-26T02:21:49.367Z
Right, $C$ is different than $R$, and $C$ is what I described in my answer.  The important difference is whether holes appear under $\lambda$, which I specifically mentioned in my answer.
Sam Tobin-Hochstadt
CC BY-SA 3.0
2014-03-22T22:06:07.457Z
2014-03-22T22:06:07.457Z
Sam Tobin-Hochstadt
<p>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 <code>eval</code>and <code>quote</code> render contextual equivalence trivial".  But referring to [2], what could be found is only the following statement by Meyer: </p>

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

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

<p><em><strong>EDIT:</strong></em></p>

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

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

<p>[2] Albert Meyer, <em>Puzzles in Programming Logic</em>  Workshop on Formal
Software Development. 1984</p>

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

CC BY-SA 3.0
2012-11-01T22:06:42.783Z
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](http://dl.dropbox.com/u/17132045/p/publications/conference/esop12.pdf)
by Inoue, Taha.
Martin Berger
CC BY-SA 3.0
2012-11-02T09:10:44.013Z
Thanks for your comment, Martin.  Maybe you can inform us a bit "the different ways of implementing `eval`/`quote` and the various options in designing contextual equivalences"?
day
CC BY-SA 3.0
2012-11-02T11:44:22.567Z
The key distinction is between CTMP (compile-time meta-programming, as exemplified by Template Haskell, Lisp/Scheme/Racket and [Converge](http://convergepl.org), and RTMP (run-time meta-programming such as Javascript's eval, or MetaOCaml). Another parameter is typing. [Here](http://www.sussex.ac.uk/Users/mfb21/pepm12-talk.key) 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.
Martin Berger
CC BY-SA 3.0
2012-11-02T13:22:37.607Z
@ 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.
Martin Berger
CC BY-SA 3.0
2012-11-02T13:35:24.217Z
@MartinBerger: Can you post your talk as pdf?
Dave Clarke
CC BY-SA 3.0
2012-11-02T13:57:02.207Z
@ Dave Clarke, sure, [here](http://www.sussex.ac.uk/Users/mfb21/pepm12-talk.pdf) it is! Feedback welcome.
Martin Berger
CC BY-SA 3.0
2012-11-02T14:23:47.163Z
@MartinBerger: If I remember correctly, some Lisp dialects have both macros and fexprs (or called `nlambda`s), which means they support both CTMP and RTMP.  The question is to which `quote`/`eval` does belong.  The answer seems to me to depend on the availability of `quote`, which is already suggested in Meyer's remark.  If `quote` is available only at compile-time, it seems it is indeed safe enough.  If it is also available at run-time, it seems it would actually cause trouble.
day
CC BY-SA 3.0
2012-11-02T14:40:36.040Z
@ plmday: Lisp's macro mechanism evolved over a long period of time. Meta-programming is a confusing concept, took a while to get it right.
Martin Berger
CC BY-SA 3.0
2012-11-02T14:51:40.400Z
[Cont.] In particular, I am not quite sure about the status of `quote` in Scheme.  According to the language report, it is part of the core syntax.  But in the given semantics, there are rules to eliminate `quote`, specifically, `(quote (x . y)) = (cons (quote x) (quote y))`.  If I understand correctly, these rules are applied before evaluation, which renders `quote` almost a macro, though not completely since eventually there would still be quoted variables (a.k.a symbols) left.  I would say the status of `quote` in Scheme is really messy.
day
CC BY-SA 3.0
2012-11-02T15:49:53.553Z
@ plmday I'm not sure, as I'm not following the Lisp/Scheme/Racket development closely. D. Herman, a student of M. Wand's, recently completed his dissertation [_A Theory of Typed Hygienic Macros_](http://www.ccs.neu.edu/home/dherman/research/papers/dissertation.pdf) which is loosely about formalising and improving the macro mechanisms in the Scheme family of languages. That's probably a good place to start looking. But in general meta-programming is not well-understood theoretically, despite working well in practise. Even worse, implementations also have plenty of rough edges.
Martin Berger
CC BY-SA 3.0
2012-11-02T19:53:14.853Z
It would be helpful if the question were stated more technically. What are the assumptions here? Is a program allowed to examine the structure of a `quoted`-expression? If so, then we trivially have trivial observational equivalence.
Andrej Bauer
CC BY-SA 3.0
2012-11-03T09:43:57.693Z
@AndrejBauer: Is it that trivial?  I thought it depends on whether `quote` is available at run-time.  If it is not, then it seems impossible to construct a context that can distinguish two observationally-equivalent terms.  In the case of Scheme, one can examine the structure of a `quote`d-expression (which after `quote`-elimination remains a list of symbols or constants), but one can not construct an evaluation context to distinguish two observationally-equivalent terms (say `(+ 1 2)` and `(+ 2 1)`) since `quote` is no longer there.
day
CC BY-SA 3.0
2012-11-03T13:04:52.927Z
Why are you talking about "runtime"? Two programs $p$ and $q$ are observationally equivalent iff for every context $C$ of ground type $C[p]$ and $C[q]$ either both diverge or both evaluate to the same value. In our case we can just use the context in which $p$ and $q$ are placed insude a `quote`, then examine them. This is why I am asking for a bit more explanation on what is really being asked.
Andrej Bauer
CC BY-SA 3.0
2012-11-03T14:36:35.720Z
@ Andrej Bauer. Contextual equivalences for rich programming languages tend to be complicated. For example for concurrent calculi, there are multiple and distinct ways of defining the concept (e.g. barbed congruence vs reduction congruence), although they collapse for sequential calculi. For meta-programming languages, programs evaluate in different stages with different operational semantics (e.g. compile time vs run-time, but conceivably more). What's a context or an evaluation at compile time is not the same thing as a context/an evaluation at run-time.
Martin Berger
CC BY-SA 3.0
2012-11-04T18:33:35.503Z
@MartinBerger: these remarks of yours must surely constitute an answer...
Neel Krishnaswami
CC BY-SA 3.0
2012-11-04T23:59:36.413Z
@MartinBerger: yes, precisely, that is why I would like to find out  what "contextual equivalence" means in this particular question. It seems to me that the answer is not going to be hard once we find out what the question is.
Andrej Bauer
CC BY-SA 3.0
2012-11-05T11:59:32.337Z
@NeelKrishnaswami, well, what would my answer be other than "it's complicated"?
Martin Berger
CC BY-SA 3.0
2012-11-05T12:01:47.560Z
@AndrejBauer: I agree with you that making precise the question is the hard part. It requires reading the Lisp/Scheme/Racket implementation, because it's not been formalised otherwise. Not a particularly joyous task.
Martin Berger
<pl.programming-languages><lisp><scheme>
Is contextual equivalence of a language with `quote`-`eval` trivial or not?
day
# Is contextual equivalence of a language with `quote`-`eval` trivial or not?

(Asked by: username_0 on 2012-11-01)

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 `eval`and `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.

**Tags:** pl.programming-languages, lisp, scheme

> **Comments:**
> **username_1**: 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](http://dl.dropbox.com/u/17132045/p/publications/conference/esop12.pdf) by Inoue, Taha.  
> **username_0**: Thanks for your comment, Martin.  Maybe you can inform us a bit "the different ways of implementing `eval`/`quote` and the various options in designing contextual equivalences"?  
> **username_1**: The key distinction is between CTMP (compile-time meta-programming, as exemplified by Template Haskell, Lisp/Scheme/Racket and [Converge](http://convergepl.org), and RTMP (run-time meta-programming such as Javascript's eval, or MetaOCaml). Another parameter is typing. [Here](http://www.sussex.ac.uk/Users/mfb21/pepm12-talk.key) 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.  
> **username_1**: @ plmusername_0: 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.  
> **username_2**: @MartinBerger: Can you post your talk as pdf?  
> **username_1**: @ username_2, sure, [here](http://www.sussex.ac.uk/Users/mfb21/pepm12-talk.pdf) it is! Feedback welcome.  
> **username_0**: @MartinBerger: If I remember correctly, some Lisp dialects have both macros and fexprs (or called `nlambda`s), which means they support both CTMP and RTMP.  The question is to which `quote`/`eval` does belong.  The answer seems to me to depend on the availability of `quote`, which is already suggested in Meyer's remark.  If `quote` is available only at compile-time, it seems it is indeed safe enough.  If it is also available at run-time, it seems it would actually cause trouble.  
> **username_1**: @ plmusername_0: Lisp's macro mechanism evolved over a long period of time. Meta-programming is a confusing concept, took a while to get it right.  
> **username_0**: [Cont.] In particular, I am not quite sure about the status of `quote` in Scheme.  According to the language report, it is part of the core syntax.  But in the given semantics, there are rules to eliminate `quote`, specifically, `(quote (x . y)) = (cons (quote x) (quote y))`.  If I understand correctly, these rules are applied before evaluation, which renders `quote` almost a macro, though not completely since eventually there would still be quoted variables (a.k.a symbols) left.  I would say the status of `quote` in Scheme is really messy.  
> **username_1**: @ plmusername_0 I'm not sure, as I'm not following the Lisp/Scheme/Racket development closely. D. Herman, a student of M. Wand's, recently completed his dissertation [_A Theory of Typed Hygienic Macros_](http://www.ccs.neu.edu/home/dherman/research/papers/dissertation.pdf) which is loosely about formalising and improving the macro mechanisms in the Scheme family of languages. That's probably a good place to start looking. But in general meta-programming is not well-understood theoretically, despite working well in practise. Even worse, implementations also have plenty of rough edges.  
> **username_3**: It would be helpful if the question were stated more technically. What are the assumptions here? Is a program allowed to examine the structure of a `quoted`-expression? If so, then we trivially have trivial observational equivalence.  
> **username_0**: @AndrejBauer: Is it that trivial?  I thought it depends on whether `quote` is available at run-time.  If it is not, then it seems impossible to construct a context that can distinguish two observationally-equivalent terms.  In the case of Scheme, one can examine the structure of a `quote`d-expression (which after `quote`-elimination remains a list of symbols or constants), but one can not construct an evaluation context to distinguish two observationally-equivalent terms (say `(+ 1 2)` and `(+ 2 1)`) since `quote` is no longer there.  
> **username_3**: Why are you talking about "runtime"? Two programs $p$ and $q$ are observationally equivalent iff for every context $C$ of ground type $C[p]$ and $C[q]$ either both diverge or both evaluate to the same value. In our case we can just use the context in which $p$ and $q$ are placed insude a `quote`, then examine them. This is why I am asking for a bit more explanation on what is really being asked.  
> **username_1**: @ username_3. Contextual equivalences for rich programming languages tend to be complicated. For example for concurrent calculi, there are multiple and distinct ways of defining the concept (e.g. barbed congruence vs reduction congruence), although they collapse for sequential calculi. For meta-programming languages, programs evaluate in different stages with different operational semantics (e.g. compile time vs run-time, but conceivably more). What's a context or an evaluation at compile time is not the same thing as a context/an evaluation at run-time.  
> **username_4**: @MartinBerger: these remarks of yours must surely constitute an answer...  
> **username_3**: @MartinBerger: yes, precisely, that is why I would like to find out  what "contextual equivalence" means in this particular question. It seems to me that the answer is not going to be hard once we find out what the question is.  
> **username_1**: @NeelKrishnaswami, well, what would my answer be other than "it's complicated"?  
> **username_1**: @AndrejBauer: I agree with you that making precise the question is the hard part. It requires reading the Lisp/Scheme/Racket implementation, because it's not been formalised otherwise. Not a particularly joyous task.  

---

## 1 answers

### Answer by username_5 on 2014-03-22. Score: 2 | Accepted answer

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.

> **Comments:**
> **username_0**: 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.  
> **username_5**: I don't understand your comment, @username_0. Why does the relationship between `'datum` and `(quote datum)` change anything?  
> **username_0**: 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.  
> **username_5**: @username_0, 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.  
> **username_0**: 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.  
> **username_5**: @username_0, the definition Wand gives is the same as the one I suggest.  
> **username_0**: Are you sure? I rechecked the paper. What I see is context $C$ used in contextual equivalence is different from reduction context $R$.  
> **username_5**: Right, $C$ is different than $R$, and $C$ is what I described in my answer.  The important difference is whether holes appear under $\lambda$, which I specifically mentioned in my answer.  

---

