I don't have Tennent's book handy either. But Neal's post claims:
"The principle dictates that an expression or statement, when wrapped in a
closure and then immediately invoked, ought to have the same meaning as it did
before being wrapped in a closure."
And IIRC, when you look it up in Tennent's book, it really doesn't say that. I
think if you squint you can sort of see a connection, but it's not obvious.
But the particular program equivalence Neal was talking about (which Tennent
does not specifically mention in his book) is as old as the lambda calculus
(we're talking 1930's here). It's a special case of what's known as
beta-equivalence (or often "beta-conversion" or "beta-reduction" or
"beta-substitution") in the lambda calculus. For what's known as the
call-by-value lambda calculus [1] it can be stated roughly like:
(lambda(x1, ..., xn) expr)(v1, ..., vn) = expr[x1 := v1, ..., xn := vn]
Using substitution (the "x := v" notation, meaning "substitute v into the
expression wherever you see a reference to x") doesn't exactly work for JS,
because it doesn't model the heap, but it doesn't much matter for the
zero-argument case.
More generally, the idea of using program equivalences for reasoning about and
designing languages is "bread and butter" for PL researchers. It's weird to see
it attributed to a tiny passage of a book from the 80's.
Dave
[1] If you don't know what call-by-value means here, don't worry about it. It
has nothing to do with call-by-reference, just an unfortunate overloading of
terminology. Nothing to see here, move along.
On Apr 9, 2011, at 10:24 AM, Wes Garland wrote:
> On Sat, Apr 9, 2011 at 12:47 PM, David Herman <dher...@mozilla.com> wrote:
> When people say "Tennent's correspondence principle" to mean something like
> "beta-conversion is semantics-preserving" I believe this post is where they
> got the impression that it has to do with Tennent. For better or worse, it
> seems to have stuck.
>
>
> I haven't got the faintest clue what beta-conversion is, but Neal's post
> seems consistent with what I took away from that (extremely short) discussion
> in Tennent's book. I'd look it up now, but it's at my office and this is the
> weekend. :) What am I missing?
>
> Wes
>
> --
> Wesley W. Garland
> Director, Product Development
> PageMail, Inc.
> +1 613 542 2787 x 102
_______________________________________________
es-discuss mailing list
es-discuss@mozilla.org
https://mail.mozilla.org/listinfo/es-discuss
