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.
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.
> 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.
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.
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.
> 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.
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...
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
> 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.
John Cowan <johnwco...@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
> John Cowan <johnwco...@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.
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.
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
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.
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.
> 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?
John Cowan <johnwco...@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.
-- Nils M Holm < n m h @ t 3 x . o r g > www.t3x.org
