Is contextual equivalence of a language with quote and eval, like Scheme, trivial or not?

[DAY]

Hi,


In [1], Mitchell Wand demonstrated that adding fexprs to the pure lambda calculus trivializes the theory of contextual equivalence: two terms are contextually equivalent iff they are α-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 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.

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 and eval, like Scheme, 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.

[John Cowan]

On Saturday, November 10, 2012 8:15:26 AM UTC-5, DAY wrote:

> Is contextual equivalence of a language with quote and eval,
> like Scheme, trivial or not?

I think not, but not for the reasons given. Scheme's `eval` is not intertwingled with the evaluation of the main program, because it has no access to the main program's binding of any variables. In Common Lisp, it has access to the main program's global bindings but not its local ones; however, Common Lisp's SET and PROGV already allow programmatic access to those bindings, so EVAL doesn't really make things worse.

[Pascal Costanza]

In Common Lisp, SET and PROGV also allow access only to global bindings
(or better: dynamic bindings, but not lexical bindings). Lexical
bindings can be fully compiled.

Pascal

--
My website: http://p-cos.net
Common Lisp Document Repository: http://cdr.eurolisp.org
Closer to MOP & ContextL: http://common-lisp.net/project/closer/
The views expressed are my own, and not those of my employer.

[John Cowan]

On Saturday, November 10, 2012 2:58:06 PM UTC-5, Pascal Costanza wrote:

> In Common Lisp, SET and PROGV also allow access only to global bindings
> (or better: dynamic bindings, but not lexical bindings). Lexical
> bindings can be fully compiled.

Just so. In Scheme, there isn't even access to the program's global bindings, unless they are made in the interaction environment and `eval` was passed the
value of `(interaction-environment)` as its second argument.

[Pascal Costanza]

Dynamic binding is not so problematic as you seem to want to make it
appear. It's easy to add dynamic binding to Scheme as a library, and
will apparently be part of R7RS as well. This doesn't affect the rest of
the language in negative ways, neither in Scheme, nor in Common Lisp.

Dynamic binding as the default binding mechanism is problematic, but
modern Lisp dialects don't do that anymore...

[John Cowan]

On Sunday, November 11, 2012 9:26:02 AM UTC-5, Pascal Costanza wrote:

> Dynamic binding is not so problematic as you seem to want to make it
> appear. It's easy to add dynamic binding to Scheme as a library, and
> will apparently be part of R7RS as well. This doesn't affect the rest of
> the language in negative ways, neither in Scheme, nor in Common Lisp.

It's not whether bindings are dynamic or static (though it happens that in Common Lisp all global bindings are dynamic). It's that CL EVAL sees certain bindings of the running program and therefore can affect it in unknown ways. In Scheme this is not true, unless both the program and `eval` are using the interaction environment. Otherwise, there is a complete firewall between a Scheme program and anything `eval` can do: in principle, `eval` could compile and run a program in a completely separate address space, as long as it had a copy of the existing dynamic environment.

R7RS support for dynamic binding involves first-class objects; all variables remain lexically bound. Note that R7RS parameters, unlike SRFI ones, aren't mutable, so it is transparent whether they are shared or copied by threads or subprocesses.

--
Normally I can handle panic attacks on my own; John Cowan <co...@ccil.org>
but panic is, at the moment, a way of life. http://www.ccil.org/~cowan
--Joseph Zitt

[Pascal Costanza]

On 11/11/2012 15:52, John Cowan wrote:
> On Sunday, November 11, 2012 9:26:02 AM UTC-5, Pascal Costanza wrote:
>
>> Dynamic binding is not so problematic as you seem to want to make it
>> appear. It's easy to add dynamic binding to Scheme as a library, and
>> will apparently be part of R7RS as well. This doesn't affect the rest of
>> the language in negative ways, neither in Scheme, nor in Common Lisp.
>
> It's not whether bindings are dynamic or static (though it happens
> that in Common Lisp all global bindings are dynamic).

That's also incorrect: Macro bindings, symbol macro bindings and
function bindings are not dynamic. Especially symbol macros allow you to
implement global lexical variables.

> It's that CL EVAL
> sees certain bindings of the running program and therefore can affect it
> in unknown ways.

Sure.

> In Scheme this is not true, unless both the program and
> `eval` are using the interaction environment. Otherwise, there is a
> complete firewall between a Scheme program and anything `eval` can do:
> in principle, `eval` could compile and run a program in a completely
> separate address space, as long as it had a copy of the existing dynamic
> environment.

OK.

> R7RS support for dynamic binding involves first-class objects; all
> variables remain lexically bound. Note that R7RS parameters, unlike SRFI
> ones, aren't mutable, so it is transparent whether they are shared or
> copied by threads or subprocesses.

This means you don't have the equivalent of SET, but it still means you
have the equivalent of PROGV.

[Nils M Holm]

John Cowan <johnw...@gmail.com> wrote:
> It's not whether bindings are dynamic or static (though it happens that
> in Common Lisp all global bindings are dynamic).

I'd argue that global Scheme bindings are dynamic, too.
Even the R6RS explanation using a global LETREC* is merely
dynamic scoping in disguise.

--
Nils M Holm < n m h @ t 3 x . o r g > www.t3x.org

[Pascal Costanza]

On 11/11/2012 16:29, Nils M Holm wrote:
> John Cowan <johnw...@gmail.com> wrote:
>> It's not whether bindings are dynamic or static (though it happens that
>> in Common Lisp all global bindings are dynamic).
>
> I'd argue that global Scheme bindings are dynamic, too.
> Even the R6RS explanation using a global LETREC* is merely
> dynamic scoping in disguise.

When discussing dynamic scoping, I always have the definition from CLtL2
in mind, as given at
http://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node43.html - that is, a
combination of indefinite scope and dynamic extent.

If you are referring to the same definition, then I'd be interested to
know how you can argue this. If you are not referring to the same
definition, I'd be interested to know which definition you are referring to.


Thanks,

[John Cowan]

On Sunday, November 11, 2012 10:21:12 AM UTC-5, Pascal Costanza wrote:

> > It's not whether bindings are dynamic or static (though it happens
> > that in Common Lisp all global bindings are dynamic).
>
> That's also incorrect: Macro bindings, symbol macro bindings and
> function bindings are not dynamic. Especially symbol macros allow you to
> implement global lexical variables.

I was speaking, of course, of variable bindings only.

> > Note that R7RS parameters, unlike SRFI
> > ones, aren't mutable, so it is transparent whether they are shared or
> > copied by threads or subprocesses.
>
> This means you don't have the equivalent of SET, but it still means you
> have the equivalent of PROGV.

Quite so; indeed, `progv` can be implemented by a trivial syntax-rules macro that rearranges (progv (param ...) (value ...) expr ...) into (parameterize ((param value) ...) expr ...). This is of course modulo the fact that the dynamically bound objects are parameters rather than symbols.

--
John Cowan http://www.ccil.org/~cowan co...@ccil.org
Uneasy lies the head that wears the Editor's hat! --Eddie Foirbeis Climo

[John Cowan]

On Sunday, November 11, 2012 10:29:51 AM UTC-5, Nils M Holm wrote:

> I'd argue that global Scheme bindings are dynamic, too.
> Even the R6RS explanation using a global LETREC* is merely
> dynamic scoping in disguise.

Can you explain this in more detail? A further binding of a global variable is an ordinary lexical binding and behaves as such.

--
My confusion is rapidly waxing John Cowan
For XML Schema's too taxing: co...@ccil.org
I'd use DTDs http://www.ccil.org/~cowan
If they had local trees --
I think I best switch to RELAX NG.

[Nils M Holm]

Pascal Costanza <p...@p-cos.net> wrote:
> On 11/11/2012 16:29, Nils M Holm wrote:
> > I'd argue that global Scheme bindings are dynamic, too.
> > Even the R6RS explanation using a global LETREC* is merely
> > dynamic scoping in disguise.
>
> When discussing dynamic scoping, I always have the definition from CLtL2
> in mind, as given at
> http://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node43.html - that is, a
> combination of indefinite scope and dynamic extent.

Ah, thanks for clarifying this! Alright, global Scheme bindings
are lexical. Sorry about the confusion.

Move along, nothing to see here.

[Pascal Costanza]

On 11/11/2012 17:19, John Cowan wrote:
> On Sunday, November 11, 2012 10:21:12 AM UTC-5, Pascal Costanza wrote:
>
>>> It's not whether bindings are dynamic or static (though it happens
>>> that in Common Lisp all global bindings are dynamic).
>>
>> That's also incorrect: Macro bindings, symbol macro bindings and
>> function bindings are not dynamic. Especially symbol macros allow you to
>> implement global lexical variables.
>
> I was speaking, of course, of variable bindings only.

Global lexical variables, no matter how they are implemented, are also
variables.

Functions are also variables in Common Lisp. They only differ from other
variables in that they are stored in a different namespace.

>>> Note that R7RS parameters, unlike SRFI
>>> ones, aren't mutable, so it is transparent whether they are shared or
>>> copied by threads or subprocesses.
>>
>> This means you don't have the equivalent of SET, but it still means you
>> have the equivalent of PROGV.
>
> Quite so; indeed, `progv` can be implemented by a trivial
> syntax-rules macro that rearranges (progv (param ...) (value ...)
> expr ...) into (parameterize ((param value) ...) expr ...). This
> is of course modulo the fact that the dynamically bound objects are
> parameters rather than symbols.

Why does that matter? If you are referring to the fact that parameters
are first class, there is no real difference here, because symbols are
first class in Common Lisp as well. If you are referring to something
else, then what is it?

[Nils M Holm]

John Cowan <johnw...@gmail.com> wrote:
> Can you explain this in more detail? A further binding of a
> global variable is an ordinary lexical binding and behaves as such.

Of course you are right! I was a bit too quick here.