Need help understanding "R5RS Domains"
Kevin Hostelley
am having a really hard time understanding what people are talking
about. I'm rather new to functional languages but I've been
programming for about 16yrs. I was a math major in college but that
was also about 16 yrs ago. Could someone suggest a path of reading to
take me from the equivalent of a freshman in college (math wise) to
someone who could intelligently discuss the topic in the "R5RS
Domains" thread?
Any help would be appreciated. Thanks.
Thant Tessman
> [...] Could someone suggest a path of reading to
> take me from the equivalent of a freshman in college (math wise) to
> someone who could intelligently discuss the topic in the "R5RS
> Domains" thread?
What he said. The books mentioned in the thread seem to be out of print.
-thant
Erann Gat
kevin_h...@keybank.com (Kevin Hostelley) wrote:
I second the question, and I'd like to make it more specific. Much of the
discussion has been about the distinction between operational semantics
and denotational semantics. I understand the difference between the two,
but what I'd like to know is what practical advantage is there to
denotational semantics? If I take the time to learn about denotational
semantics, how will I be able to use that to improve my code? Or is it
merely an intellectual exercise?
Thanks,
Erann Gat
g...@jpl.nasa.gov
Stephen J. Bevan
> What he said. The books mentioned in the thread seem to be out of print.
Schmidt has put his book online :-
ftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/DenSem.tar.gz
Also Andrew Pitts has put his lecture notes on denotational semantics
online at :-
http://www.cl.cam.ac.uk/Teaching/Lectures/dens/
I haven't read the following but from the look of the sample pages it
covers domains in more depth than anything else I've read (note I've
not read Scott's original papers) :-
Domains and Lambda Calculi
Roberto M. Amadio and Pierre-Louis Curien
1998
http://www.amazon.com/exec/obidos/ASIN/0521622778/qid=1026237411/sr=1-7/ref=sr_1_7/102-1511207-0510516
All of the following books have sections on domains and some of them
should still be in print :-
@book
{ Allison:pids:1986
, author= "Lloyd Allison"
, title= "A practical introduction to denotational semantics"
, publisher= "Cambridge University Press"
, year= 1988
, pages= 306
, refs= 66
, source= "own"
, checked= 19951227
, cr= "8807-0478"
, isbn= "0-521-31423-2"
, blurb= "This textbook is an introduction to denotational
semantics and its applications to programming languages. Dr Allison
emphasises a practical approach and the student is encouraged to
write and test denotational definitions.
The first section is devoted to the mathematical foundations of the
subject and sufficient detail is given to illustrate the fundamental
problems. The remainder of the book covers the use of denotational
semantics to describe sequential programming languages such as
Algol, Pascal and c. Throughout, numerous exercises, usually in
Pascal, will help the student practise writing definitions and carry
out simple applications. The book culminates in discussing an
executable semantics of the logic-programming language Prolog.
Being an introduction, advanced undergraduates in computer science
and graduates new to the subject will find this readily accessible
account of one of the central topics of computer science."
, sjb= "Like Schmidt~\cite{Schmidt:ds:1986} gives an example of
a while loop that is defined in terms of itself as the motivation
for introducing fixed points and domains. However, once it is done,
he continues to use the self-referential version in later chapters
rather than the version using fixed points."
, reffrom= McDonald:Allison:bcs:cj:1989
}
@book
{ Watt:plss:1991
, author= "David A. Watt"
, title= "Programming Language Syntax and Semantics"
, publisher= "Prentice-Hall"
, year= 1991
, refs= 58
, source= "own"
, checked= 19960310
, isbn= "0-13-726274-4"
, blurb= "Programming Language Syntax and Semantics introduces
methods for formaly specifying the syntax and semantics of programming
languages.
Chapter 2 introduces the topic of syntax, covering both context-free
grammars and regular expressions. Chapters 3-5 introduce denotational
semantics, the most commonly used method for specifying semantics.
Chapter 6 introduces algebraic semantics, applying it to specify new
data types. Chapters 7-8 introduce action semantics, a new method
that promises to make semantic specifications unusually readable. the
text concentrates on practical specification techniques, but the
underlying theory is briefly covered where appropriate.
Numerous examples, exercises, and case studies support the text."
}
@book
{ Gunter:splst:1992
, author= "Carl A. Gunter"
, title= "Semantics of programming languages: structures and techniques"
, email= "gun...@cis.upenn.edu"
, publisher= "MIT Press"
, year= 1992
, series= "Foundations of computing"
, pages= 419
, source= "own"
, cr= "9305-0276"
, checked= 19940103
, errata= "file://ftp.cis.upenn.edu/pub/papers/gunter/SPL_errata.ps"
, errata= "file://ftp.cis.upenn.edu/pub/papers/gunter/SPL_errata.dvi"
, errata= "file://research.att.com/dist/carl/SPL_errata.dvi"
, errata= "file://research.att.com/dist/carl/SPL_errata.ps"
, sjb= "The errata are for the first edition"
, blurb= "This book expounds the basic motivations and
philosophy underlying the applications of semantic techniques in
programming language theory. There is an emphasis on the structures
used in semantics and the techniques that have been developed for
relating various approaches to the semantics of programming languages,
particularly for languages with higher-order functions. Type systems
are the central organizational theme of the discussion.
The book is designed as a text for upper-level and graduate-level
students from all areas of computer science; it should also be useful
to anyone needing an easily accessed description of fundamental
results and calculi from the semantics of programming languages. Some
of the primary topics covered here include models of types,
operational semantics, category theory, domain theory, fixed-point
(denotational) semantics, full abstraction and other semantic
correspondence criteria, relationships between types and evaluation,
type checking and inference, subtypes, and parametric polymorphism.
As a set of general prerequisites for the book I assume familiarity
with the basic concepts of programming languages such as variable
binding and scope, evaluation, and parsing. Some familiarity with
interpreters and compilers is also expected. Ideally, a multi-lingual
student should know something about Lisp (or Scheme), Prolog, and an
imperative language such as Pascal or C. Knowledge of a language
based on the typed lambda-calculus such as ML or Haskell would be
helpful (especially for Chapter 7) but it is not assumed. The text by
Paulson (``ML for the Working Programmer'', Cambridge University
Press,
1991) is a representative discussion of ML programming. For computer
science students, this book can serve as an introduction to the
mathematical techniques used in the study of programming languages.
Some mathematical sophistication is essential, but I have limited the
prerequisites to what a student should have encountered already in an
undergraduate course on logic or abstract algebra. In summary,
general familiarity with a representative from each of the following
groups of texts forms an ideal background:
\begin{enumerate}
\item Compilers and interpreters
\begin{itemize}
\item Aho, Sethi, and Ullman, ``Compilers: Principles, Techniques, and
Tools'', Addison Wesley, 1985;
\item Fischer and LeBlanc, Crafting a Compiler with C, Benjamin/Cummings,
1991.
\end{itemize}
\item Comparative programming languages
\begin{itemize}
\item Sethi, ``Programming Languages: Concepts and Constructs'', Addison
Wesley, 1989;
\item Kamin, ``Programming Languages: An Interpreter Based Approach'',
Addison Wesley, 1990;
\item Friedman, Wand, and Haynes, Essentials of Programming Languages,
MIT Press, 1992.
\end{itemize}
\item Logic
\begin{itemize}
\item Boolos and Jeffrey, ``Computability and Logic'', Cambridge University
Press, second edition, 1980;
\item Lewis and Papadimitriou, ``Elements of the Theory of Computation'',
Prentice-Hall, 1981.
\end{itemize}
\end{enumerate}
In general, the content of the book is self-contained with enough
information that a diligent reader can derive full proofs of all the
results with enough time, pencils, and paper. A wide selection of
exercises have been provided at the ends of the sections in which the
definitions and methods they draw upon are stated. At the end of each
chapter there is a section of notes in which references to work
related to the topic of the chapter are given."
, reffrom= Ferreira:Hennessy:Jeffrey:acm:icfp:1996
}
@book
{ Winskel:fspl:1993
, author= "Glynn Winskel"
, title= "The Formal Semantics of Programming Languages"
, publisher= "MIT Press"
, year= 1993
, reffrom= Thompson:Hill:fple:1995
, reffrom= Kirkerud:pls:1997
}
@book
{ Kirkerud:pls:1997
, author= "Bj{\/o}rd Kirkerud"
, title= "Programming Language Semantics: Imperative and Object
Oriented Languages"
, publisher= "Thomson"
, year= 1997
, refs= 32
, pages= 347
, source= "own"
, checked= 19970201
, cost= "UKP 23.95"
, isbn= "1-85032-273-2"
, blurb= "{\em Programming Language Semantics} is designed to
provide a formal introduction to the semantics of programming
languages for readers with little or no prior experience of the
subject. Focusing mainly on denotational semantics, the author also
explains operational and axiomatic semantics.
The book explains how to define semantics of imperative programming
languages. A chapter on objects and clsses is also included,
providing the formal definitions of the semantics of object oriented
languages. The functional language ML is used to implement some of
the formal definitions given in the book."
}
@book
{ Reynolds:tpl:1998
, author= "John C. Reynolds"
, title= "Theories of Programming Languages"
, publisher= "Cambridge University Press"
, year= 1998
, pages= 500
, source= "own"
, checked= 20001022
, cost= "CDN$ 74.95"
, isbn= "0-521-59414-6"
, blurb= "This textbook is a broad but rigorous survey of the
theoretical basis of the design, definition, and implementation of
programming languages, and of systems for specifying and proving
program behavior. Both imperative and functional programming are
covered, as well as the ways of integrating these aspects into more
general langauges. Recognizing a unity of technique beneath the
diversity of research in programming languages, the author presents
an integrated treatment of the basic principles of the subject. He
identifies the relatively small number of concepts, such as
compositional semantics, binding structure, domains, transition
systems, and iference rules, that serve as the foundation of the
field.
The basic concepts and their properties are described with
mathematical rigor, but the mathematical development is balanced by
numerous examples of applications, particularly of program
specification and proof, concurrent programming, functional
programming (including the use of continuations and lazy
evaluation), and type systems (including subtyping, polymorphism,
and modularization).
Assuming only knowledge of elementary programming and mathematics,
this text is perfect for advanced undergraduate and beginning
graduate courses in programming language theory, and also will
appeal to researchers and professionals in desgining or implementing
computer languages."
}
Thant Tessman
[...denotational semantics references...]
Thank you! And I promise not to try to build a free-energy machine with
whatever I manage to learn.
-thant
Daniel C. Wang
ste...@dino.dnsalias.com (Stephen J. Bevan) writes:
> Thant Tessman <th...@acm.org> writes:
> > What he said. The books mentioned in the thread seem to be out of print.
>
> Schmidt has put his book online :-
>
> ftp://ftp.cis.ksu.edu/pub/CIS/Schmidt/DenSem.tar.gz
>
I'd also recommend Schmidt's survey paper in CACM as a good start too.
Schmidt, D.A. Programming language semantics. In CRC Handbook of Computer
Science, Allen Tucker, ed., CRC Press, Boca Raton, FL, 1996. Summary
version, ACM Computing Surveys 28-1 (1996) 265-267.
Also available from his home page
http://www.cis.ksu.edu/~schmidt/papers/CRC.chapter.ps.Z
It covers all the major semantics technqiues and discuses their advantages
and disadvantages without getting lost in too much math.
Bill Richter
Much of the [R5RS Domains] discussion has been about the
distinction between operational semantics and denotational
semantics. I understand the difference between the two, but what
I'd like to know is what practical advantage is there to DS?
I think the answer is that the DS folks know how to do things about
"arbitrary reduction order" that I don't know how to do with OpS, and
that this is good for compiler design.
Think of OpS as being like the syntax of the Lambda Calculus (LC).
I'll assume you understand the rudiments of LC, otherwise read Hankin.
The great thing about LC is arbitrary reduction order: You can
beta-reduce your LC expression in any order you like. There's a
specified order to reduce an LC expression, and that's given by the
standard reduction function
SR: LC expressions ---> { beta-normal forms }_bottom
The point is that SR is like the usual Scheme evaluation "algorithm",
and that you don't have to use it! But in Scheme, we normally think
you have to follow the rules for evaluation.
But with R5RS DS you can do something like arbitrary reduction order:
You can "reduce" a procedure or a continuation "out of order" because
the procedures & continuations are no longer syntax that have to wait
their turn. Now procedures & continuations are actual functions
proc: E* x K x S -> A
cont: E* x S -> A
So by definition we can reduce them out of order, because they're
"already reduced" to functions! I think that's what Matthias B said.
So my aim is to understand these "out of order reductions" are that
R5RS DS gives, and to explain them syntactically (more or less), which
is maybe what folks here call OpS. I'm sure lots about this is known.
Now the `R5RS Domains' discussion about whether OpS could be called DS
if you wrote it as a function, or whether DS functions had to be
defined by structural induction... that's all pretty silly and not
worth taking to a new newsgroup. I was obviously right about these
points (after I "hit my stride"), but it's not important. What's
important is all the "out of order reductions" you can get from DS.
--
Bill
<http://www.math.nwu.edu/~richter>
Matthias Blume
<sigh>
I haven't got the slightest idea what you are talking about. And
neither have you, obviously. Bill, please, refrain from answering
questions that you don't know the answer to.
Your characterization of operational semantics is so out of whack, it
is not even funny. You clearly have no understanding at all of what
"denotational semantics" or "operational semantics" means to the rest
of the world.
(You were also not at all right about any of the points above, no
matter how many times you say otherwise.)
</sigh>
David Rush
> > What he said. The books mentioned in the thread seem to be out of print.
>
> Schmidt has put his book online :-
.
.
.
Lovely list! Can this go up on readscheme.org?
david rush
--
Einstein said that genius abhors consensus because when consensus is
reached, thinking stops. Stop nodding your head.
-- the Silicon Valley Tarot
Joe Marshall
"Kevin Hostelley" <kevin_h...@keybank.com> wrote in message
news:b669caa1.02070...@posting.google.com...
I thought `Denotational Semantics: The Scott-Strachey Approach to
Programming Languages Theory' by Joe E. Stoy, MIT Press,
Cambridge MA, 1977 was very good. I don't know if it is still in
print.
Kevin Hostelley
Thanks for the exhaustive list. I mean exhaustive in the sense that
I'll probably be near death by the time I'm finished reading :-).
Thanks again!
ozan s yigit
> { Allison:pids:1986
> , author= "Lloyd Allison"
> , title= "A practical introduction to denotational semantics"
> , publisher= "Cambridge University Press"
> , year= 1988
> , pages= 306
> , refs= 66
> The first section is devoted to the mathematical foundations of the
> subject and sufficient detail is given to illustrate the fundamental
> problems. The remainder of the book covers the use of denotational
> semantics to describe sequential programming languages such as
> Algol, Pascal and c. Throughout, numerous exercises, usually in
> Pascal, will help the student practise writing definitions and carry
> out simple applications. The book culminates in discussing an
> executable semantics of the logic-programming language Prolog.
i have this slim volume, and i think it is the most helpful DS book
i own. sort of like strunk&waite for DS. :) if it is still in print,
i would highly recommend it. [the part on prolog is especially
interesting to those familiar with the language]
oz
---
Never let your job get in the way of your work.
-- Sir Isaac Newton, Master of the Royal Mint
Erann Gat
<matt...@shimizu-blume.com> wrote:
[In response to Bill Richter's response to my question]:
> <sigh>
>
> I haven't got the slightest idea what you are talking about. And
> neither have you, obviously. Bill, please, refrain from answering
> questions that you don't know the answer to.
Don't worry, Matthias, I've got a pretty good bullshit filter, and I've
learned a while ago not to pay much attention to Bill.
(Bill, in case you're wondering, what finally convinced me that you
haven't got a freakin' clue is this post:
http://groups.google.com/groups?selm=fqznx88ewh.fsf%40artin.math.northwestern.edu&output=gplain
> In hindsight, it seems pretty obvious. c is bound to the "escape
> continuation", and when we evaluate
>
> (0 (c 1))
>
> first 0 & (c 1) are evaluated, before the DS checks that 0 isn't a
> function, and then c applies the "escape continuation" to 1. Cool.
I consider myself pretty clueless when it comes to theory, but I learned
how continuations work ten years ago. If you are only now figuring this
out then you must be about as clueless as I was ten years ago, and that's
pretty clueless. This post sounds kind of like, "Hey, look everyone, I
just figured out that you can define a function in terms of itself!
Cool!" Yes, it is cool, but it's old, old, old news.)
E.
Bill Richter
> In hindsight, it seems pretty obvious. c is bound to the "escape
> continuation", and when we evaluate
>
> (0 (c 1))
>
> first 0 & (c 1) are evaluated, before the DS checks that 0 isn't
> a function, and then c applies the "escape continuation" to 1.
> Cool.
Yes, it is cool, but it's old, old, old news.
Erann, I'm confused. I'm certainly no call/cc expert, but I hadn't
thought folks here thought Al P's exercise
(call/cc (lambda (c) (0 (c 1)))) => 1
was `old, old, old news.' I thought it was considered startling
enough to prove Al's exercise in R5RS DS. I missed what Al & Thomas B
posted about the DS, but Will C's R5RS DS proof runs 500 lines on his
web page, and Will doesn't give an explanation. I gave a much shorter
proof than Will's, with my "shortcut formulas", and I also supplied an
explanation. I don't see how that's evidence of my cluelessness.
--
Bill <http://www.math.nwu.edu/~richter>
Bill Richter
matter how many times you say otherwise.)
Matthias, I'm so certain I'm right that I don't want to talk about it
any more. If I figure out how to K-ify my simple (UxK -> ExS) DS, and
get some "out of order" reductions for procedures and continuations,
I'll post on c.l.ml, per Shriram & Will's suggestion.
--
Bill
<http://www.math.nwu.edu/~richter>
Matthias Blume
> Erann Gat replies to me:
>
> > In hindsight, it seems pretty obvious. c is bound to the "escape
> > continuation", and when we evaluate
> >
> > (0 (c 1))
> >
> > first 0 & (c 1) are evaluated, before the DS checks that 0 isn't
> > a function, and then c applies the "escape continuation" to 1.
> > Cool.
>
> Yes, it is cool, but it's old, old, old news.
>
> Erann, I'm confused. I'm certainly no call/cc expert, but I hadn't
> thought folks here thought Al P's exercise
>
> (call/cc (lambda (c) (0 (c 1)))) => 1
>
> was `old, old, old news.' I thought it was considered startling
> enough to prove Al's exercise in R5RS DS.
FYI, it is a very old hat. Anyone who does not understand the above
can safely be assumed to not understand continuations at all.
Before you ask, this has nothing to do with the long -- and, once
again, at times unfortunate -- discussion of whether or not preserving
the RnRS-prescribed behavior at all costs is necessary or even "good".
I publicly stated that I do not think so. In fact, I championed a
language change that syntactically rules out all literals in operator
position.
With such a change the above expression would be rejected by the
compiler (well before any part of the program that contains it would
start executing). However, such a language change has conceptually
nothing to do with continuations as it would also affect completely
call/cc-free code such as (if #t 1 (0)) etc.
Matthias Blume
> If I figure out how to K-ify my simple (UxK -> ExS) DS, and
> get some "out of order" reductions for procedures and continuations,
> I'll post on c.l.ml, per Shriram & Will's suggestion.
In case you didn't get it: Shriram's suggestion is a cruel joke at
c.l.ml's expense.
Al Petrofsky
> Erann, I'm confused. I'm certainly no call/cc expert, but I hadn't
> thought folks here thought Al P's exercise
>
> (call/cc (lambda (c) (0 (c 1)))) => 1
>
> was `old, old, old news.' I thought it was considered startling
> enough to prove Al's exercise in R5RS DS.
To anyone with a good command of the scheme language, it was quite
obvious that the expression is either an error or evaluates to 1.
When people referred to the informal section of r5rs to check which it
is, they were confronted with ambiguity. If they then turned to the
formal specification, it became clear that the result is 1. To those
familiar with the denotational semantics, it was a simple matter of
checking the formula for combinations.
> I missed what Al & Thomas B posted about the DS
We just said that the DS unambiguously specify that the result is 1.
> Will C's R5RS DS proof runs 500 lines on his web page, and Will
> doesn't give an explanation. I gave a much shorter proof than
> Will's, with my "shortcut formulas", and I also supplied an
> explanation.
Will proved what the result is in the language formally defined in
r5rs. You may have proved what the result is in the language defined
by your own private formulas, but nobody cares about that language.
> I don't see how that's evidence of my cluelessness.
A vicious aspect of being extremely clueless is that it makes it
nearly impossible to see your own cluelessness. The first and most
difficult step is to admit that you have a problem, and submit to a
higher authority. As long as you insist on seeing yourself as a
teacher with something to offer, before you have been a student, you
will never learn, much less teach, anything.
-al
P.S. Because Bill is such a poor student, people have become less and
less inclined to waste their time pointing out his errors. It's been
almost a month since I stopped following up to his posts, but I
decided to post one more time just to make it explicit that I am
biting my tongue. Please assume that he continues to be wrong about
almost everything, and that statements like "I was obviously right
about these points" do not mean (as they would coming from an ordinary
person) that anybody has actually come to agree that he was right
about those points.
Bill Richter
> > some "out of order" reductions for procedures and continuations,
> > I'll post on c.l.ml, per Shriram & Will's suggestion.
>
> In case you didn't get it: Shriram's suggestion is a cruel joke at
> c.l.ml's expense.
Thanks, Matthias. I think the joke is at my expense. I went to
c.l.ml and was dumb-founded to see almost no posts! Basically it's
just Joe Well's job listing (which I saw on plt-scheme) that I'm
clearly unqualified for.
Anyway, c.l.ml is fine for now, because I'm a long way from posting!
I've got serious improvements to make before I post, and maybe it
won't happen at all, I'm hustling to join the Fall Math jobmart.
Bill Richter
> > Erann, I'm confused. I'm certainly no call/cc expert, but I
> > hadn't thought folks here thought Al P's exercise
> >
> > (call/cc (lambda (c) (0 (c 1)))) => 1
> >
> > was `old, old, old news.' I thought it was considered startling
> > enough to prove Al's exercise in R5RS DS.
>
> FYI, it is a very old hat. Anyone who does not understand the above
> can safely be assumed to not understand continuations at all.
Thanks, Matthias. I'm really confused: why the DS discussion at all?
Why did Will C post such a long thorough R5RS DS proof?
I give myself credit for figuring out the super-obvious fact. As a
call/cc novice, I figured it out & posted it even, and figured out
where in the DS it happens (the "bad procedure" error message has to
wait in the continuation till it's too late), and said how to change
the DS so it doesn't happen (replace single by my single-F).
> Before you ask, this has nothing to do with the long -- and, once
> again, at times unfortunate -- discussion of whether or not
> preserving the RnRS-prescribed behavior at all costs is necessary or
> even "good". I publicly stated that I do not think so. In fact, I
> championed a language change that syntactically rules out all
> literals in operator position.
That's the part of the thread I remember! The part when Al's exercise
was actually being done in R5RS DS is lost in google-land :)
And I objected to your change, because there's no real good reason why
a procedure can't be a literal, and then you'd be wrong. From R5RS:
3.3 External representations
Many objects have standard external representations, but some, such
as procedures, do not have standard representations (although
particular implementations may define representations for them).
So if lots of "particular implementations" started defining
representations for procedures, then you couldn't rule out a literal
procedure. Of course this is pretty impractical.
> With such a change the above expression would be rejected by the
> compiler (well before any part of the program that contains it would
> start executing). However, such a language change has conceptually
> nothing to do with continuations as it would also affect completely
> call/cc-free code such as (if #t 1 (0)) etc.
Thanks for reminding me, I missed that.
--
Bill <http://www.math.nwu.edu/~richter>
Erann Gat
<ric...@birkhoff.math.northwestern.edu> wrote:
> Erann Gat replies to me:
>
> > In hindsight, it seems pretty obvious. c is bound to the "escape
> > continuation", and when we evaluate
> >
> > (0 (c 1))
> >
> > first 0 & (c 1) are evaluated, before the DS checks that 0 isn't
> > a function, and then c applies the "escape continuation" to 1.
> > Cool.
>
> Yes, it is cool, but it's old, old, old news.
>
> Erann, I'm confused.
Yes, I know.
> I'm certainly no call/cc expert,
Yes, I know that too.
> but I hadn't thought folks here thought Al P's exercise
>
> (call/cc (lambda (c) (0 (c 1)))) => 1
>
> was `old, old, old news.'
It isn't. But that has absolutely nothing to do with what you wrote. The
fact that you don't understand this is further evidence of your
cluelessness.
> I thought it was considered startling
> enough to prove Al's exercise in R5RS DS. I missed what Al & Thomas B
> posted about the DS, but Will C's R5RS DS proof runs 500 lines on his
> web page, and Will doesn't give an explanation. I gave a much shorter
> proof than Will's, with my "shortcut formulas", and I also supplied an
> explanation. I don't see how that's evidence of my cluelessness.
Your shortcut explanation is a complete non-sequitur. It has nothing
whatsoever to do with the topic at hand. It's akin to someone
participating in a discussion of literature proudly announcing, "Hey guys,
I just discovered that there's this great thing called Cliff Notes, which
are much shorter than the originals, and so let you get the gist of the
work in 1/10th the time. (Hey, and they're yellow too! Cool!)" Your
comments shed about as much light on a discussion of denotational
semantics as a gleeful announcement of the discovery of Cliff Notes would
shed on a discussion of symbolism in the works of Shakespeare.
Here's a clue (not that I think it will do much good given your history):
forget all the fancy math. The fact that you use the words "when" and
"before" in your 'shortcut' show that you don't get it. There is no
"when" in denotational semantics; that's the whole point. Understand that
and you will have taken your first step towards enlightenment.
E.
David Rush
> > > If I figure out how to K-ify my simple (UxK -> ExS) DS, and get
> > > some "out of order" reductions for procedures and continuations,
> > > I'll post on c.l.ml, per Shriram & Will's suggestion.
> >
> > In case you didn't get it: Shriram's suggestion is a cruel joke at
> > c.l.ml's expense.
Only a little bit, I think. Shriram certainly appears to have a high
level of respect for the ML crowd.
> I went to c.l.ml and was dumb-founded to see almost no posts!
Yes, they have a very high S/N ratio. It's actually a really good
newsgroup for detailed technical answers. SML is a language which
really punishes sloppy thinking. This is both an advantage and a
disadvantage (No, this is not flame-bait...)
Bill Richter
> > Erann, I'm confused. I'm certainly no call/cc expert, but I
> > hadn't thought folks here thought Al P's exercise
> >
> > (call/cc (lambda (c) (0 (c 1)))) => 1
> >
> > was `old, old, old news.' I thought it was considered startling
> > enough to prove Al's exercise in R5RS DS.
>
> To anyone with a good command of the scheme language, it was quite
> obvious that the expression is either an error or evaluates to 1.
Thanks, Al. That's a very different statement than "it's old old news
that your expression evaluates to 1." Settling 1 or error is worth a
DS calculation.
> > Will C's R5RS DS proof runs 500 lines on his web page, and Will
> > doesn't give an explanation. I gave a much shorter proof than
> > Will's, with my "shortcut formulas", and I also supplied an
> > explanation.
>
> Will proved what the result is in the language formally defined in
> r5rs. You may have proved what the result is in the language
> defined by your own private formulas
Wrong. My proof is 99% as rigorous as Will's. My "private formulas"
are derived from the R5RS DS formulas. The 1% lack of rigor comes
from my tossing out error handling that didn't seem significant to me
the 1st time through. One thing I really liked about your exercise is
that it uncovered a bug of mine in error handling. But once I fixed
that bug, the calculation went fine. Thanks for the cool exercise!
> statements like "I was obviously right about these points" do not
> mean (as they would coming from an ordinary person) that anybody has
> actually come to agree that he was right about those points.
Good point. I know I'm right even though nobody has agreed with me.
That's the way Math is. Remember in Orwell's 1984 and the `hero'
Winston writes, "Someday the Party will declare that 2 + 2 = 5, and
everyone will believe them. [...] Freedom amounts to being able to say
that 2 + 2 = 4, all else follows."
--
Bill <http://www.math.nwu.edu/~richter>
Bill Richter
good newsgroup for detailed technical answers. SML is a language
which really punishes sloppy thinking. This is both an advantage
and a disadvantage (No, this is not flame-bait...)
Thanks, David, and so I will post there, should I finish my project,
no sure thing even if I had time. If it's not the right group,
someone can redirect me, maybe the moderator. I'd like to learn SML.
I do think that Shriram & Will showed good leadership in ending the
crazy discussion, even if c.l.ml isn't the perfect newsgroup for DS.
Bill Richter
> "Hey guys, I just discovered that there's this great thing called
> Cliff Notes, which are much shorter than the originals, and so let
> you get the gist of the work in 1/10th the time. (Hey, and they're
> yellow too! Cool!)"
That's funny, Erann! We're all working on our standup routines :)
> The fact that you use the words "when" and "before" in your
> 'shortcut' show that you don't get it. There is no "when" in
> denotational semantics; that's the whole point. Understand that and
> you will have taken your first step towards enlightenment.
What are you talking about??? Here's my 'shortcut' post again, and
there's no mention of "when" and "before":
More details of Al's exercise (call/cc (lambda (c) (0 (c 1)))) => 1:
First, some formulas:
applicate: E x E* x K x S ---> A
(applicate f l kappa sigma) = (if (in-F? f)
(f l kappa sigma)
(wrong "bad procedure" sigma))
where wrong: X x S ---> A sends error message (AFAIK not using sigma).
For simplicity I'm getting rid of permute/unpermute. I'll simplify S
to (L -> E), getting rid of the boolean flag, and drop the
L-coordinate for procedure values (only used by eqv?), so that's
F = E* x K x S -> A
I'm consistently "un-currying" the R5RS DS definitions to what I think
is a more sensible Scheme convention, as in these 3 examples and also
curly-E: Expressions ---> (U x K x S -> A)
Simplest formulas we need are are
(curly-E[[ nu ]] rho kappa sigma) = (kappa <nu> sigma)
(curly-E[[ (I nu) ]] rho kappa sigma) = (phi <nu> kappa sigma)
if (sigma (rho I)) = phi in F.
for a number nu and a variable I. We have a general formula for a
1-arg combination:
(curly-E[[ (A B) ]] rho kappa sigma)
= (curly-E[[ A ]] rho single(lambda (f s)
(curly-E[[ B ]] rho single(lambda (e s)
(applicate f <e> kappa s)) s)) sigma)
Restricting to a non-procedure 1st arg, say Al's 0, we have
(curly-E[[ (0 B) ]] rho kappa sigma)
= (curly-E[[ B ]] rho kappa_1 sigma)
kappa_1 = single(lambda (e s) (wrong "bad procedure" s))
That's basically Al's formula in a nutshell: instead of returning the
error message "bad procedure", we stick it in the continuation, which
we never reach, since call/cc replaces it with the original cont.
Now we'll do call/cc for a 1-arg 1-body-form lambda expression:
(curly-E[[ (cwcc (lambda (x) B)) ]] rho kappa sigma)
= (curly-E[[ B ]] rho_1 kappa sigma_1)
where rho_1 & sigma_1 are extensions of rho & sigma with
x -rho_1--> (new sigma) -sigma_1--> phi_kappa
where phi_kappa is the procedure value (lambda (l k s) kappa l s).
Now we're ready for Al's formula. For kappa the initial continuation,
which prints out values, we have:
(curly-E[[ (cwcc (lambda (c) (0 (c 1)))) ]] rho kappa sigma)
= (curly-E[[ (0 (c 1)) ]] rho_1 kappa sigma_1)
c -rho_1--> (new sigma) -sigma_1--> phi_kappa
phi_kappa = (lambda (l k s) kappa l s) in F
= (curly-E[[ (c 1) ]] rho_1 kappa_1 sigma_1)
kappa_1 = single(lambda (e s) (wrong "bad procedure" s))
= (phi_kappa <1> kappa_1 sigma_1)
= (kappa <1> sigma_1) = 1
Great work, Al! "For 59 years I've put up with it now!
I must stop Xmas from coming, but how?" --Ted G
I'm sure Will is doing the same thing, but I couldn't follow his
proof. I've forgotten what hold, lookup, tievals etc even mean.
But now instead let's use my single-F, for which I'll give a better
definition today:
single-F: (F x S -> A) ---> (E* x S -> A)
single-F(psi) = (lambda (l s) (if (= (length l) 1)
(if (in-F? (car l))
(psi (car l) s)
(wrong "bad procedure" s))
(wrong "wrong number args" s)))
Then we have a new formula for a 1-arg combination:
(curly-E[[ (A B) ]] rho kappa sigma)
= (curly-E[[ A ]] rho single-F(lambda (f s)
(curly-E[[ B ]] rho single(lambda (e s)
(f <e> kappa s)) s)) sigma)
And then if we have 0 in the 1st position, we get
(curly-E[[ (0 B) ]] rho kappa sigma)
= (wrong "bad procedure" sigma)
and so we'd get instead
(curly-E[[ (cwcc (lambda (c) (0 (c 1)))) ]] rho kappa sigma)
= (curly-E[[ (0 (c 1)) ]] rho_1 kappa sigma_1)
c -rho_1--> (new sigma) -sigma_1--> phi_kappa
phi_kappa = (lambda (l k s) kappa l s) in F
= (wrong "bad procedure" sigma_1)
= "bad procedure"
But I suspect no one will want to adopt this new definition of
curly-E[[ (A B) ]] because it rejects the arbitrary order of
evaluation.
--
Bill <http://www.math.nwu.edu/~richter>
Erann Gat
<ric...@conley.math.northwestern.edu> wrote:
> > The fact that you use the words "when" and "before" in your
> > 'shortcut' show that you don't get it. There is no "when" in
> > denotational semantics; that's the whole point. Understand that and
> > you will have taken your first step towards enlightenment.
>
> What are you talking about???
This:
> In hindsight, it seems pretty obvious. c is bound to the "escape
> continuation", and when we evaluate
^^^^
>
> (0 (c 1))
>
> first 0 & (c 1) are evaluated, before the DS checks that 0 isn't a
^^^^^^
> function, and then c applies the "escape continuation" to 1. Cool.
E.
Matthias Blume
> Yes, [c.l.ml has] a very high S/N ratio. It's actually a really
> good newsgroup for detailed technical answers. SML is a language
> which really punishes sloppy thinking. This is both an advantage
> and a disadvantage (No, this is not flame-bait...)
>
> Thanks, David, and so I will post there, should I finish my project,
> no sure thing even if I had time. If it's not the right group,
> someone can redirect me, maybe the moderator. I'd like to learn SML.
People have already redirected you. Comp.theory is one option that
was offered. C.l.ml is *definitely* the wrong group to post
denotational semantics-related stuff as denotational semantics are
completely out-of-fashion there. (Moreover, there is no call/cc in ML
- except for one particular implementation of SML that offers it as an
extension.)
> I do think that Shriram & Will showed good leadership in ending the
> crazy discussion, even if c.l.ml isn't the perfect newsgroup for DS.
There is another, much simpler way of ending this discussion: actually
ENDing it.
Matthias Blume
> Settling 1 or error is worth a DS calculation.
No, it is not. Scheme's denotational semantics specifies the
language's dynamic aspects. Nobody claimed that a dynamic error
should be the outcome. There were a few people who agreed with me
that a *static* error would be acceptable (and perhaps desirable, but
definitely something not required, endorsed, or tolerated by a strict
interpretation of the current standard).
> Good point. I know I'm right even though nobody has agreed with me.
> That's the way Math is.
No, that's the way delusions are. Most reasonable people would start
to question their own thinking when there is *nobody* who agrees with
them and everybody, including known experts, who has voiced any
opinion at all disagrees with them. Just by invoking the word "Math"
does not make one right. In particular not when one has repeatedly
shown to make major mistakes in one's "Math" all the time.
> Remember in Orwell's 1984 and the `hero'
> Winston writes, "Someday the Party will declare that 2 + 2 = 5, and
> everyone will believe them. [...] Freedom amounts to being able to say
> that 2 + 2 = 4, all else follows."
Sure, freedom also amounts to being able to say that 2 + 2 = 3. You
have become quite good at exercising this sort of freedom.
(Just because the "Party" declared X to be true does not mean that X
has to be false. Not to mention that your comparing us to an
Orwellian "Party" is yet another of your rather unbelievable insults.)
Lauri Alanko
> Erann, I'm confused. I'm certainly no call/cc expert, but I hadn't
> thought folks here thought Al P's exercise
>
> (call/cc (lambda (c) (0 (c 1)))) => 1
>
> was `old, old, old news.'
It wasn't, but the issue had nothing to do with continuations. The question
raised (and answered) by Al was whether, during the evaluation of an
application, the check that the operator is a procedure had to be done after
all the operands were evaluated, or if an implementation was free to do the
check even before that. The informal semantics of R5RS didn't say anything
about the check, but the formal DS did.
The question could as well have been whether (0 (display "foo")) should
display "foo" before raising an error. But side effects are icky, so Al's
test case that used call/cc was just something it's easier to try out on
one's implementation.
Lauri Alanko
l...@iki.fi
Thant Tessman
> [...] C.l.ml is *definitely* the wrong group to post
> denotational semantics-related stuff as denotational semantics are
> completely out-of-fashion there. [...]
Aie! One of the reasons I wanted to learn about DS is because some day
I'd like to be able to read _The Definition of Standard ML_ and actually
understand it. I thought what was in that book was DS. Is it something else?
-thant
Stephen J. Bevan
> Aie! One of the reasons I wanted to learn about DS is because some day
> I'd like to be able to read _The Definition of Standard ML_ and actually
> understand it. I thought what was in that book was DS. Is it something else?
Yes, Natural Semantics. Schmidt's paper that Daniel Wang recommended
is a good place to start since it covers Structured Operational
Semantics, Denotational Sematics and Natural Semantics. Some of the
programming language semantics books I mentioned also cover all three
e.g. Gunter. If you can get hold of it then [Kahn:tacs:1987] is worth
a read as is [Mitchell:edinburgh:lfcs:311:1994].
@inproceedings
{ Kahn:tacs:1987
, author= "G. Kahn"
, title= "Natural Semantics"
, crossref= "tacs:1987"
, reffrom= Attali:Chazarain:agata:1990
, reffrom= Grosch:Snelting:plilp:1990
, reffrom= Snelting:acta:1991
, reffrom= Odersky:acm:toplas:1993
, reffrom= Kirkerud:pls:1997
}
@proceedings
{ tacs:1987
, editor= "F.J. Brandenburg and G. Vidal-Naquet and M. Wirsing"
, title= "Proceedings of Theoretical Aspects of Computer Software"
, booktitle= "Proceedings of Theoretical Aspects of Computer Software"
, publisher= "Springer Verlag"
, volume= 247
, series= lncs
, year= 1987
}
@techreport
{ Mitchell:edinburgh:lfcs:311:1994
, author= "Kevin Mitchell"
, title= "Concurrency in a Natural Semantics"
, institution= "Laboratory for the Foundations of Computer Science, University
of Edinburgh"
, year= 1994
, number= "ECS-LCFS-94-311"
, source= "http://www.lfcs.informatics.ed.ac.uk/reports/94/ECS-LFCS-94-311/ECS-LFCS-94-311.ps"
, abstract= "Natural Semantics, a form of operational semantics,
can be used to give a concise description of the evaluation of many
sequential programming languages. However, concurrent languages
present a problem for this approach as it is difficult to express
the interaction between parallel processes. For such languages an
approach such as Plotkin's structural operational semantics is
usually preferred. Unfortunately such semantics are frequently
verbose and may contain an unnecessary amount of detail about the
evaluation. In this paper we show how the relational approach at the
heart of Natural Semantics can be extended to handle concurrent
languages and explore the relationship between these two semantic
approaches in such a setting."
}
Al Petrofsky
> Bill Richter <ric...@conley.math.northwestern.edu> writes:
[Regarding (call/cc (lambda (c) (0 (c 1))))]
> > Settling 1 or error is worth a DS calculation.
>
> No, it is not. Scheme's denotational semantics specifies the
> language's dynamic aspects. Nobody claimed that a dynamic error
> should be the outcome. There were a few people who agreed with me
> that a *static* error would be acceptable (and perhaps desirable, but
> definitely something not required, endorsed, or tolerated by a strict
> interpretation of the current standard).
Actually, there were two questions of what the standard says, one
static and one dynamic, to which someone reasonably familiar with the
standard might not be certain of the answer without pulling the
standard out to check. I think you implemented it as a static error
without explicitly realizing at the time that you were deviating from
the standard. I could imagine an implementor doing that, anyway.
Similarly, I think Dybvig implemented it as a dynamic error in chez
scheme without realizing that this was nonstandard.
To settle the question of whether a dynamic error is an allowable
outcome, one does indeed have to check the DS, because the informal
specification of combinations is vague about this. "Calculation" is
not required, though. Simply reading the combination formula and the
applicate formula is sufficient. Clinger's lengthy derivation was not
intended to persuade anybody of anything (and it doesn't prove
anything in general, just the result of one particular expression).
It was intended to help people interested in learning about DS to see
in detail how r5rs assigns meaning to an expression.
-al
Bill Richter
Sorry, Erann, I realized what you meant after logging off.
> > What are you talking about???
>
> This:
>
> > In hindsight, it seems pretty obvious. c is bound to the "escape
> > continuation", and when we evaluate
> ^^^^
> >
> > (0 (c 1))
> >
> > first 0 & (c 1) are evaluated, before the DS checks that 0 isn't a
> ^^^^^^
> > function, and then c applies the "escape continuation" to 1.
> > Cool.
>
> E.
You're complaining about me on confusing OpS with DS. I'm not the
only one who engages in this confusion, I'd call it an allowable
`abuse of notation'. Oleg K & Joe M talked about "reductions" in R5RS
DS, and Joe even called them "beta reductions". Technically, you
shouldn't say "beta reduction" unless you're working in the syntax of
LC, and I did even tweak Joe on this, but everyone (including me)
understood what he meant.
But more importantly, the chasm between OpS and DS isn't as wide as
you guys seem to think. Here's something Will wrote on May 28:
ces...@qnci.net (William D Clinger) replies to me:
> > My impression is that R5RS DS rewrites full Scheme into LC_v (pure
> > Scheme) no doubt with extra constants or something, and not LC
> > (with the same extra constants). I don't know this is true.
>
> Actually, both are true. The R5RS DS is written in LC (with extra
> constants) in a stylized way (CPS) that has the property that it
> doesn't matter whether you use the unrestricted beta rule or the
> restricted beta-value rule. This is a feature.
Will seems to be saying that we can make a DS for Scheme with the R5RS
DS formulas by mapping Scheme expressions to some LC with constants
(which maybe will involve Scott models) and then use the term model
for this LC with constants, and that means to just beta-reduce an
expression until we reach a beta-normal forms. And Will is saying
there's an LC_v version of this too.
So I see Will as giving a very interesting way in which R5RS DS could
be thought of in an OpS way.
At least, I tend to think of any LC syntax as being OpS. I don't
actually know the def of OpS. The def of OpS in Schmidt didn't seem
very precise to me, just sounded like `OpS = sequence of reductions',
which is fine, and doesn't rule out OpS being turned to DS by making a
nice mathematical (total) function out of it.
--
Bill <http://www.math.nwu.edu/~richter>
Bill Richter
Thanks, Lauri. I hesitate to say this, but I think the informal R5RS
is either crystal clear (return 1 & not error) or it's just wrong:
4.1.3 Procedure calls
syntax: (<operator> <operand1> ...)
[...] The operator and operand expressions are evaluated (in an
unspecified order) and the resulting procedure is passed the
resulting arguments.
call/cc makes the last clause false. If evaluating the operands pulls
in the escape continuation, then it's not true that the
`procedure is passed the resulting arguments'.
I'd say this was comparable to a discussion of do loops in a Fortran
manual, one could write:
in the do loop below,
do i = 1, 10
body
end do
the body is evaluated 10 times, with i incremented each time.
But that's false if there's a goto statement in the body!
Everyone knows that goto statement mess up loops, so maybe this
wouldn't really be an error for the Fortran manual. Let's take this
same attitude about R5RS: we should understand that it really says:
[...] The operator and operand expressions are evaluated (in an
unspecified order) and the resulting procedure is passed the
resulting arguments unless a call/cc escape continuation jumps us
away for the procedure call, just like a Fortran goto statement.
That's lousy prose, but you guys understand what I should've written.
In that case, R5RS is unambiguously saying
(call/cc (lambda (c) (0 (c 1)))) => 1
Because clearly R5RS is saying the operands are evaluated _before_
passing the argument values to the procedure value. Why would you get
a "bad procedure" error message without trying to plug arguments into
a non-procedure (like 0)?
I suppose people said this while the discussion was going on, and I'm
sorry I missed it. The real point is that the informal R5RS just
isn't precise enough to chop the words apart like I'm doing, so you
gotta take these cases to the DS. More applause for Al!
--
Bill <http://www.math.nwu.edu/~richter>
Bill Richter
> Just by invoking the word "Math" does not make one right.
Sure, Matthias! Especially if I'm the invoker, since as you say:
> In particular not when one has repeatedly shown to make major
> mistakes in one's "Math" all the time.
No, I'm just the only one who admitted my mistakes, and I learned from
them! I'm sure you guys are the same way with programming. Nobody
writes (or posts) perfect code, but you debug it, you get it right.
> (Just because the "Party" declared X to be true does not mean that X
> has to be false.
Right.
> Not to mention that your comparing us to an Orwellian "Party" is yet
> another of your rather unbelievable insults.)
Sorry, I didn't mean to compare you. I mean though that the truth or
falseness of mathematical assertions doesn't depend on what you guys
(or the Party) say. It's a matter of proof. I'm satisfied with my
proofs, and I didn't see that anyone refuted me, and I thought my
`non-refuters' made errors themselves.
But it ain't all Math. There's are important non-Math question like:
what is DS good for, how do the cultures of DS & OpS differ, and
what's the best way's way to write a good fast correct compiler?
I don't know much about these questions, and more reading would help.
Stephen's list looks good. I don't htink it will settle my question.
About ENDing it, I'm just hanging around to see if I'll get a comment
on my calculation of Al's cool formula.
My DS `shortcut formulas' have nothing to do with my (scorned &
possibly false) views about defining semantic functions. My shortcuts
are formulas I figured long ago, before you & Will clued me in on
Scott domains and defining semantic functions. I merely simplified
things out like tievals & hold & send.
R5RS DS is pretty careful about error messages, and in fact Al's
formula hinged on the handling of the error message "bad procedure".
And I blew that myself, and had to debug my code. But e.g. if we do
calculations with the right number of arguments, we can ignore the
error message "wrong number of arguments".
As to the DS disputes about defining semantic functions, I'm sure I'm
right but I don't think it matters. when you guys say "Richter is
wrong", I think you mean "Richter's DS is so weak, so who cares
whether he's right or wrong." That's fine. When you say "you must
define semantic functions the way Schmidt does" I think you really
mean "that's the only way we're gonna worry about!" That's fine.
The real point is that I've got a lot of respect for you guys, you
clued me in on some really interesting Math that I completely missed
in _my_ baseless scorn, but I've got a lot more respect for Felleisen,
who did not jeer at me like y'all have, but he didn't find me a job
either. So I've puzzled over the question: Why did MF bother to spend
so much time teaching me LC_v? And I think the answer is that Math
dept are the right place to continue researching LC_v etc. CS dept
have more money, but they have to earn it, with applications, one
after the next. Math depot are on a more relaxed pace, nobody cares
what they're doing, and so why shouldn't they study LC_v? I'll give
it a shot when I get back on the gravy train. My chances went up a
little last night when I computed the cycle
e_0 = lambda_{8333} + lambda_{4517} + lambda_{3833}
in the 16 stem of the 4-line of the Lambda algebra. My boss predicted
I would mis-compute this element but I didn't :)
--
Bill <http://www.math.nwu.edu/~richter>
Feuer
from this discussion. The rest have been listening to Will, Blume,
et al. and learned _something_.
David
Bill Richter
combination formula and the applicate formula is sufficient.
Daniel C. Wang
Bill Richter <ric...@poincare.math.northwestern.edu> writes:
{stuff deleted}
> But more importantly, the chasm between OpS and DS isn't as wide as
> you guys seem to think. Here's something Will wrote on May 28:
> At least, I tend to think of any LC syntax as being OpS. I don't
> actually know the def of OpS. The def of OpS in Schmidt didn't seem
> very precise to me, just sounded like `OpS = sequence of reductions',
> which is fine, and doesn't rule out OpS being turned to DS by making a
> nice mathematical (total) function out of it.
These are two mutually contradictory statements. How can you make claims
about the properties of OpS vs. DS and in the same breath say you don't
really understand the difference! As someone pointed out it's the difference
between a compiler and an interpreter!
Go read the survey paper I pointed you too. You're last statment is utter
garbage, and really makes it clear how poor a grasp you have about the
differences between the two.
Alf Petrofsky
Thanks for including me in that list, but did you mean to say "al.*",
or have you only been listening to my three-letter variations?
-al
William D Clinger
> I know I'm right even though nobody has agreed with me.
Bertrand Russell had several things to say about this:
...when the experts are agreed, the opposite opinion cannot be held
to be certain;
The opinions that are held with passion are always those for which
no good ground exists; indeed the passion is the measure of the
holder's lack of rational conviction.
There is something feeble and a little contemptible about a man
who cannot face the perils of life without the help of comfortable
myths.
There are infinite possibilities of error, and more cranks take up
unfashionable errors than unfashionable truths.
(All of these epigrams can be found on pages 15 and 16 of "The
Basic Writings of Bertrand Russell", Simon and Schuster, 1961, to
which I refer readers for citations.)
For the record, let me remind latecomers that this is not about
whether an operational semantics can be viewed as denotational
if you stand on your head and squint, nor is it even about whether
a denotational semantics must be compositional. There is room for
differences of opinion on those things, and the experts know that.
This is not a matter of opinion, but a matter of mathematics, and
very simple math at that: whether Richter's formulation of his own
semantics is compositional. Richter has continued to insist that
it is, despite heroic efforts by many here to explain the concepts
of compositionality and induction to Richter.
If that were all there were to it, I would just ignore Richter.
But Richter has been trying to use his flimsy credentials as a
mathematician to intimidate and to insult those who have been so
unwise as to respond to Richter's own requests for help in
understanding the mathematical foundations of programming language
semantics. That is an affront to all mathematicians.
Will
Feuer
Daniel C. Wang
A mini-tutorial on the various semantic technqiues and their differences
for those who actually care. Ask questions, and I'm sure the experts can
help out. Those who have a better grasp of the literature feel free to add
some relevant citations. This mini-tutorial basically summarizes several
decades of progress and experience in this area.
The next time I get an infinite amount of free time, maybe I'll write up a
tutorail about establishing type soundness and formulating type systems for
the various systems. Oh, I forgot this wasn't comp.lang.ml.....
Bill Richter goes in my kill file until I receive answer to all the exercies.
Syntax for boolean expressions
------------------------------------------------------------------------
e ::= true | false | (not e) | (or e1 e2) | (and e1 e2)
Note: No recursion to avoid any issues with fix points!
------------------------------------------------------------------------
Denotational Semantics
------------------------------------------------------------------------
Lets choose the semantic domain of natural numbers
[[true ]] = n > 0
[[false]] = 0
[[not e]] = if [[e]] = 0 then 1 else 0
[[(or e1 e2)]] = [[e1]] + [[e2]]
[[(and e1 e2)]] = [[e1]] * [[e2]]
Lets choose another semantic domain the domain of sets.
[[true ]] = {{}} (* set containing the empty set *)
[[false]] = {} (* the empty set *)
[[not e]] = [[e]] difference {{}}
[[(or e1 e2)]] = [[e1]] union [[e2]]
[[(and e1 e2)]] = [[e1]] intersect [[e2]]
Exercise: Show that [[(and (not true) false)]] \equiv [[false]] in both domains.
Exercise: Prove the following equations from each of domain
[[(or e1 e2)]] \equiv [[(or e2 e1)]]
[[(not(or e1 e2))]] \equiv [[(and (not e1) (not e2))]]
------------------------------------------------------------------------
Natural Operational Semantics (Big Step)
------------------------------------------------------------------------
Define a subset of expressions which we will call "values" to be
v ::= true | false
Define the relation (==>) between expressions inductively as follows
Read (e ==> v) as "e" evaluates to "v"
true ==> true
false ==> false
if (e ==> false) then ((not e) ==> true)
if (e ==> true) then ((not e) ==> false)
if (e1 ==> false) and (e2 ==> false) then ((or e1 e2) ==> false)
if (e1 ==> true) and (e2 ==> v) then ((or e1 e2) ==> true)
if (e1 ==> v) and (e2 ==> true) then ((or e1 e2) ==> true)
if (e1 ==> true) and (e2 ==> true) then ((and e1 e2) ==> true)
if (e1 ==> false) and (e2 ==> v) then ((and e1 e2) ==> false)
if (e1 ==> v) and (e2 ==> false) then ((and e1 e2) ==> false)
I've used "non-standard" notation for the above. "Gentze style" rules are the more
standard notation used.
hyp1 hyp2 ... hypn
------------------ = if hyp1 and hyp2 and hypn then concl
concl
(Please view the below with a fixed width font!)
So the rules above are rewritten and layouted nicely as
-------------- ----------------
true ==> true false ==> false
e ==> false e ==> true
-------------- ----------------
(not e) ==> true (not e) ==> false
e1 ==> false e2 ==> false e1 ==> true e2 ==> v e1 ==> v e2 ==> true
---------------------------- ---------------------------- ----------------------------
(or e1 e2) ==> false (or e1 e2) ==> true (or e1 e2) ==> true
e1 ==> true e2 ==> true e1 ==> false e2 ==> v e1 ==> v e2 ==> false
---------------------------- ---------------------------- ----------------------------
(and e1 e2) ==> true (and e1 e2) ==> false (and e1 e2) ==> false
Exercise: Show that (and (not true) false) ==> false
Exercise: Prove the following facts
(or e1 e2) ==> v iff (or e2 e1) ==> v
(not(or e1 e2)) ==> v iff (and (not e1) (not e2)) ==> v
------------------------------------------------------------------------
Small Step Operational Semantics
------------------------------------------------------------------------
Yet another variant of operational semantics. It's easier to specify
many more low level details such as evaluation order. The natural
semantics above do not specify any specific evaluation order. There are
several flavors of small steps semantics too.
Define a relation (|-->) from expressions to expressions and a subset of
expressions we will call values as
v ::= true | false
Read e |--> e' as "e steps to e'".
Define |--> as follows.
[local reductions]
------------------------- -------------------------
(not true) |--> false (not false) |--> true
---------------------------- --------------------------- --------------------------
(or false false) |--> false (or true v) |--> true (or v true) |--> true
---------------------------- --------------------------- --------------------------
(and true true) |--> true (and false v) |--> false (and v false) |--> false
[structural reductions]
e |--> e'
----------------------------- where (e is not a value)
(not e) |--> (not e')
e1 |--> e1'
----------------------------- where (e1 is not a value)
(or e1 e2) |--> (or e1' e2)
e2 |--> e2'
----------------------------- where (e2 is not a value)
(or v1 e2) |--> (or v1 e2')
e1 |--> e1'
----------------------------- where (e1 is not a value)
(and e1 e2) |--> (and e1' e2)
e2 |--> e2'
----------------------------- where (e2 is not a value)
(and v1 e2) |--> (and v1 e2')
So now we define a new function |-->* to be the our multi-step evaluation relation.
e1 |-->* e2 e2 |--> e3
----------------------- --------------
e1 |-->* e3 v |-->* v
Now our |-->* acts like our previously defined relation ==> relation but we encode many
more details of the actually computation.
Exercise: Show that (and (not true) false) |-->* v
How many steps does it take?
Exercise: Prove the following facts
(or e1 e2) |-->* v iff (or e2 e1) |-->* v
(not(or e1 e2)) |-->* v iff (and (not e1) (not e2)) |-->* v
Exercise: Redefine the semantics above to "short circuit" evaluation for the
boolean operators. e.g. (and false (not(or true true))) |-->* false
Should take one step to evaluate.
Question: Can you formulate "short circuit" evaluation in a natural or denotational
semantics?
------------------------------------------------------------------------
Small Step Operational Semantics
------------------------------------------------------------------------
The last five non-local reductions can be more elegantly expressed by
introducing the notion of an "evaluation context" which is a set of
expressions with a "hole".
E ::= [] | (not E) | (and E e1) | (and v E) | (or E e) | (or v E)
Also define E[e] to be the evaluation context with the "hole" filled in.
e.g.
Given the evaluation context
[][e] = e
(not [])[e] = (not e)
(not (and true (or [] (not (not true)))))[e] = (not (and true (or e (not (not true)))))
Let us define a new relation for non-local reductions |-C->
e |--> e'
-------------------
E[e] |-C-> E[e']
Now define |-C->* in a similar way as we did for |--> and we get yet
another small-step semantics. Evaluation contexts are a bit more
concise and allow you to model things like first-class continuations
and exceptions in a small-step operational semantics. Encoding
exceptions and first-class continuations in the other semantics is
messy if not impossible to do.
Exercise: Show that (and (not true) false) |-C->* v
How many steps does it take?
Exercise: Prove the following
(or e1 e2) |-C->* v iff (or e2 e1) |-E->* v
(not(or e1 e2)) |-C->* v iff (and (not e1) (not e2)) |-C->* v
Exercise: Extend our language as follows
e ::= true | false | (not e) | (or e1 e2) | (and e1 e2) | (throw e)
so that (or e (throw v)) |-C->* v
Exercise: Think about how to do this in the other semantics.
------------------------------------------------------------------------
Bill Richter
> This is not a matter of opinion, but a matter of mathematics, and
> very simple math at that: whether Richter's formulation of his own
> semantics is compositional.
Thanks, Will. Sounds like you're dismissing the claim that the
semantic function must be defined by Schmidt's structural induction.
> Richter has continued to insist that it is, despite heroic efforts
> by many here [...] That is an affront to all mathematicians.
Then for the honor of Math, argue about it with me! Don't dismiss me.
I'll summarize my proof of compositionality:
[1] I've got a general inductive technique to construct semantic-like
functions, modeled on the standard reduction function of LC or LC_v.
[2] Using this technique, I constructed my (total) semantic function
curly-E: Expressions ---> (U x S -> E x S)_bottom
by concocting a set of `hybrid' expressions, Scheme expressions jazzed
up with environments & values. Nobody responded to this.
[3] Then I sketched a proof of compositionality, by constructing a
function Phi satisfying
curly-E[[ (A B) ]] = Phi( curly-E[[ A ]], curly-E[[ B ]] )
Obviously I need more than just this function Phi, and I also
constructed (after Joe M responded) a function Phi_0 satisfying
curly-E[[ (A) ]] = Phi_0( curly-E[[ A ]] )
That's not enough either, but that's where the `heroic efforts' were.
I don't think anyone's looked at my arguments yet. I think Matthias
dismissed [1] altogether, and assumed falsely that I was doing [2] &
[3] together, clearly a big error of structural induction. I vainly
tried to explain to him that having _first_ constructed curly-E, it
was perfectly legitimate to _then_ define Phi in terms of curly-E.
I say it's obvious that if my curly-E is a well-defined function, then
my DS is compositional. Because essentially
Compositionality is emphasized in SICP! Essentially. All I did was
use a SICP-ish definition of procedure values and switch over to the
simple non-call/cc DS mentioned in the intro of Cartwright-Felleisen.
So when folks claimed my DS wasn't compositional, I think they really
meant that I hadn't correctly defined curly-E, but instead just made a
huge error in structural induction. That's their error, not mine!
Back to you, Will:
> For the record, let me remind latecomers that this is not about
> whether an operational semantics can be viewed as denotational if
> you stand on your head and squint,
That was indeed an issue. But you seem to understand that squinting
can turn OpS into DS, although others here don't seem to. Thanks.
I say it like this: if you clarify the OpS reductions with sets &
functions, you've got a (not necessarily useful) DS semantic function
curly-E: Expressions ---> Some set
So you (Will) seem to be agreeing with my point [1] above, if not
point [2] as well, that it's legit to use the OpS-ish technique used
in the construction of the LC/LC_v standard reduction function.
> nor is it even about whether a denotational semantics must be
> compositional.
Good. I didn't think anyone was arguing about this.
I think you understand something I posted: Felleisen constructs in his
notes on LC_v a non-compositional DS for LC_v. A much more difficult
but compositional DS for LC_v is given later in Cartwright-Felleisen.
**** More details on [1] ****
Given a set X with a subset A and a set Y and a function
f: A ---> Y
and a partial function R: X ---> X, we define the partial functions
R^n (the iterative composites of R with itself) by induction, and
then define a total function
F: X ---> Y_bottom
F(x) = f(R^n(x)), if n is the least nonnegative integer such
that R^n(x) belongs to the subset A and all
R^i(x) are defined for 0 \le i \le n
bottom, otherwise.
Now Will, I take it from what you wrote above that you're agreeing
that my inductive scheme is a legit way to construct functions, even
though I'm not using structural induction.
On 28 Jun, I even constructed this F as a least-fixed point of the
selfmap Phi of (X -> Y_bottom) defined by by
Phi(G)(x) = f(x), if x in A
G(R(x)), if x in Domain(R)
bottom, otherwise.
No response ever. No response to this:
The term model of LC (which I'd call compositional) is mostly
described by a total well-defined mathematical function
SR: LC ---> { beta-normal forms }_bottom
and this standard reduction function is defined without any recourse
to CPOs or least fixed points. The induction that's needed to
construct SR is about the same induction that's needed to construct
the least fixed point (i.e. l.u.b. F^k( lambda x. bottom )).
> Bertrand Russell had several things to say about this:
>
> ...when the experts are agreed, the opposite opinion cannot be held
> to be certain;
nothing can `be held to be certain'. We know from Goedel & Cohen etc
that all our math depends on the unproven belief that a model of ZFC
exists. Plus, we all can & do make mistakes, so even if Math was on
firm foundations, we're fallible humans, so anything can be wrong.
> The opinions that are held with passion are always those for which
> no good ground exists; indeed the passion is the measure of the
> holder's lack of rational conviction.
Good quote. Anyone reading c.l.s. will see that I've been much more
polite and dispassionate than my opponents.
> There is something feeble and a little contemptible about a man who
> cannot face the perils of life without the help of comfortable
> myths.
Sure, like a belief in a ZFC model!
> There are infinite possibilities of error, and more cranks take up
> unfashionable errors than unfashionable truths.
Isn't that's a tautology, since cranks are by definition wrong?
I think that Bertrand was speaking about politics rather than math,
though. I've got a lot of respect for Russell's math & politics.
--
Bill <http://www.math.nwu.edu/~richter>
--
Bill
<http://www.math.nwu.edu/~richter>
David Rush
IIRC, it's Operational. Personally, I find OpS harder to read than DS,
but that could be just because I was exposed to them at different
stages of my development.
david rush
--
By loudly denouncing all bad things - war and hunger and date
rape - liberals testify to their own terrific goodness.
-- P. J. O'Rourke
Matthias Blume
> ces...@qnci.net (William D Clinger) writes:
>
> > This is not a matter of opinion, but a matter of mathematics, and
> > very simple math at that: whether Richter's formulation of his own
> > semantics is compositional.
>
> Thanks, Will. Sounds like you're dismissing the claim that the
> semantic function must be defined by Schmidt's structural induction.
>
> > Richter has continued to insist that it is, despite heroic efforts
> > by many here [...] That is an affront to all mathematicians.
>
> Then for the honor of Math, argue about it with me! Don't dismiss me.
>
> I'll summarize my proof of compositionality:
>
> [1] I've got a general inductive technique to construct semantic-like
> functions, modeled on the standard reduction function of LC or LC_v.
>
> [2] Using this technique, I constructed my (total) semantic function
>
> curly-E: Expressions ---> (U x S -> E x S)_bottom
>
> by concocting a set of `hybrid' expressions, Scheme expressions jazzed
> up with environments & values. Nobody responded to this.
>
> [3] Then I sketched a proof of compositionality, by constructing a
> function Phi satisfying
>
> curly-E[[ (A B) ]] = Phi( curly-E[[ A ]], curly-E[[ B ]] )
This is not a "proof" because you are "proving" the wrong objective.
I told you what compositionality really means. You did not believe
me, but that is your problem, not ours.
If you can show me a definition of Phi that does not mention or refer
to curly-E, then -- and only then -- have you succeeded in giving a
compositional definition.
> That was indeed an issue. But you seem to understand that squinting
> can turn OpS into DS, although others here don't seem to. Thanks.
No. Squinting can turn a DS into an OpS (because you can read it as if
it were some pure lambda calculus). The reverse transformation
OpS->DS is possible, but squinting alone won't do it.
> Given a set X with a subset A and a set Y and a function
>
> f: A ---> Y
>
> and a partial function R: X ---> X, we define the partial functions
> R^n (the iterative composites of R with itself) by induction, and
> then define a total function
>
> F: X ---> Y_bottom
>
> F(x) = f(R^n(x)), if n is the least nonnegative integer such
> that R^n(x) belongs to the subset A and all
> R^i(x) are defined for 0 \le i \le n
>
> bottom, otherwise.
Bill, would you, please, refrain from ever posting this again. I must
have seen this a hundred times by now. I am sick of it.
Why? Ponder this:
Let A = Y be the set of total functions from N to N, let f be the
identity function on A. Let X be the set of partial functions from N
to N. Let R(x) be the function that maps 0 to 1 and any other n to
the product of n and x applied to the predecessor of n. Let x0 be
the partial function from N to N that is nowhere defined.
According to your construction, your resulting F(x0) would be bottom.
In programming languages, we want it to be something else. (I leave
it as an exercise to you what the intended result is. Hint: It is
easy because it is a standard example.)
Bill Richter
refer to curly-E, then -- and only then -- have you succeeded in
giving a compositional definition.
I'm sure that's false, Matthias. I'm sure that compositionality means
exactly that this equation is true:
curly-E[[ (A B) ]] = Phi( curly-E[[ A ]], curly-E[[ B ]] )
If you think otherwise, can you give me a citation?
It's true that in Schmidt's structural induction technique, one must
give a `definition of Phi that does not mention or refer to curly-E'.
Back to Will:
But Richter has been trying to use his flimsy credentials as a
mathematician
Let's use MathSciNet <http://e-math.ams.org/mathscinet/search> to find
who's got more pubs. I bet Felleisen's got the most. I've got 7 or
so, which wasn't enough to stay on the Math gravy train, but I
wouldn't call that `flimsy'. My problem was that the other
topologists weren't interested my work. Doesn't mean my work was
lousy. I thought it was ahead (and before!) of it's time.
I was an NSF postdoc, which supposedly put me the top 20 or so
American Math/CS PhDs of my year.
to intimidate and to insult those who have been so unwise as to
respond to Richter's own requests for help in understanding the
mathematical foundations of programming language semantics.
It's true I requested help, and I received plenty! Will C was quite
helpful in the `vision' dept, telling me about program equivalences,
and that one can redo R5RS DS as LC (or LC_v!!!) with constants.
Stephen B was quite helpful with his quotes from Schmidt & Stoy, books
I had foolishly dismissed. Stephen explained enough of Schmidt to get
me to read it again, and then I learned the CPO least-fixed point
technique for constructing semantic functions.
You (Matthias) were the most helpful, and you were so helpful it's
hard to chronicle what I learned from you over the years.
Let A = Y be the set of total functions from N to N, let f be the
identity function on A. Let X be the set of partial functions from
N to N.
OK, A = Y = (N -> N), and X = partial(N -> N)
Let R(x) be the function that maps 0 to 1 and any other n to the
product of n and x applied to the predecessor of n.
OK, so x is an element of X = partial(N -> N), hence a partial
function
x: N -> N
R(x) must be either be bottom an element of X, i.e. a partial function
R(x): N ---> N
R(x)(n) = 1, if n = 0
n * x(n-1), if n > 1 and x(n-1) is defined
undefined, otherwise
So
R(x)(1) = 1 * x(0)
R(x)(2) = 2 * x(1)
sounds OK. Now I'm defining a function
F: X ---> Y_bottom
F(x) = f(R^n(x)), if n is the least nonnegative integer such
that R^n(x) belongs to the subset A and all
R^i(x) are defined for 0 \le i \le n
bottom, otherwise.
That means we take a partial function x and keep applying R to it
until it becomes a total function, and that's F(x), and otherwise we
get bottom.
So if x is undefined on a finite number of elements of N, then
applying R enough will push the undefined elements past zero, and then
we'll get a total function. Nice.
Let x0 be the partial function from N to N that is nowhere defined.
According to your construction, your resulting F(x0) would be
bottom.
I guess you're right! Since x0 is undefined everywhere,
R(x0) = x0
and so we see that R^n(x0) is never in A, for any n, so we set
F(x0) = bottom
In programming languages, we want it to be something else.
I'll take your word for it, but this by no means refutes my technique.
I've got a perfectly good inductive construction of functions, similar
to the way the standard reduction function in LC or LC_v is
constructed. I suppose you're saying that my technique isn't suitable
for all purposes. That's fine.
There's a general point here: just because you know more than I do
about DS doesn't mean the little I've figured out is false.
(I leave it as an exercise to you what the intended result is.
Hint: It is easy because it is a standard example.)
I have no idea, but I'll look in Schmidt. Thanks for the exercise!
--
Bill
<http://www.math.nwu.edu/~richter>
Matthias Blume
> If you can show me a definition of Phi that does not mention or
> refer to curly-E, then -- and only then -- have you succeeded in
> giving a compositional definition.
>
> I'm sure that's false, Matthias. I'm sure that compositionality means
> exactly that this equation is true:
>
> curly-E[[ (A B) ]] = Phi( curly-E[[ A ]], curly-E[[ B ]] )
>
> If you think otherwise, can you give me a citation?
>
> It's true that in Schmidt's structural induction technique, one must
> give a `definition of Phi that does not mention or refer to curly-E'.
Forget about the word "compositional". The fact is that what I
describe is what's required. If you want to call it something else
than "compositional", more power to you.
> Back to Will:
>
> But Richter has been trying to use his flimsy credentials as a
> mathematician
>
> Let's use MathSciNet <http://e-math.ams.org/mathscinet/search> to find
> who's got more pubs. I bet Felleisen's got the most. I've got 7 or
> so, which wasn't enough to stay on the Math gravy train, but I
> wouldn't call that `flimsy'. My problem was that the other
> topologists weren't interested my work. Doesn't mean my work was
> lousy. I thought it was ahead (and before!) of it's time.
Sure! Your work on denotational semantics is also way ahead of its
time, obviously. Actually, the reason that we all fight you so hard
is that we are secret members of the SSTDS (Society for the
Suppression of the Truth about Denotational Semantics), founded by
Dana Scott himself to hide the fact that he made an unnecessarily
complicated model for the pure lambda calculus (which, had the truth
come out, would have tainted his reputation of a Turing Award winner).
Bill, get a grip!
> There's a general point here: just because you know more than I do
> about DS doesn't mean the little I've figured out is false.
True. I did not say that your construction doesn't construct anything
at all. However, the something that it does construct is not
something that would be very useful in the context of this discussion.
As far as facts go, you could as well keep telling us about your
recent insight that 2 + 2 = 4. It is true, but it does not help.
> (I leave it as an exercise to you what the intended result is.
> Hint: It is easy because it is a standard example.)
>
> I have no idea [ ... ]
^^^^^^^^^^^^^^
Very telling...
David Rush
Do you have any idea how many entries in my BBDB specify you? I'm
writing a whole new tool (in Scheme) just to cope...
david rush
--
Scheme: Because it *is* the red pill...
-- Anton van Straaten (the Scheme Marketing Dept from c.l.s)
David Rush
> Matthias Blume wrote an obtuse definition of a function that every
> CS major has writeen at last once and then said:
> > (I leave it as an exercise to you what the intended result is.
> > Hint: It is easy because it is a standard example.)
>
> I have no idea, but I'll look in Schmidt. Thanks for the exercise!
Bill, it's the factorial function.
david rush
--
Both CL and Scheme have excellent pros to learn from found in either
c.l.l and c.l.s and both are not without cons. I guess you cdr saw
that one coming...
-- George Demmy (on comp.lang.scheme)
William D Clinger
> Actually, the reason that we all fight you so hard
> is that we are secret members of the SSTDS (Society for the
> Suppression of the Truth about Denotational Semantics), founded by
> Dana Scott himself to hide the fact that he made an unnecessarily
> complicated model for the pure lambda calculus (which, had the truth
> come out, would have tainted his reputation of a Turing Award winner).
Matthias, Matthias. You know the penalty for revealing that to
a real mathematician. We'll miss you.
Will
Matthias Blume
Yes. I am expecting the black helicopters to show up any minute now. :(
Bill Richter
> > If you can show me a definition of Phi that does not mention or
> > refer to curly-E, then -- and only then -- have you succeeded
> > in giving a compositional definition.
> >
> > I'm sure that's false, Matthias. I'm sure that compositionality
> > means exactly that this equation is true:
> >
> > curly-E[[ (A B) ]] = Phi( curly-E[[ A ]], curly-E[[ B ]] )
> >
> > If you think otherwise, can you give me a citation?
> >
> > It's true that in Schmidt's structural induction technique, one
> > must give a `definition of Phi that does not mention or refer to
> > curly-E'.
>
> Forget about the word "compositional". The fact is that what I
> describe is what's required. If you want to call it something else
> than "compositional", more power to you.
That sounds like a huge admission, Matthias! Thanks! Let's be sure,
though, let's go back to Will letter of 12 Jul:
This is not a matter of opinion, but a matter of mathematics, and
very simple math at that: whether Richter's formulation of his own
semantics is compositional. [...] That is an affront to all
mathematicians.
Sounds like you're saying my definition is compositional, and that
means we've got nothing to argue about, there's no affront. Right?
But, then I think you're saying that simple DS is useless, since I
didn't use Scott models. And I can believe that, I've never argued
otherwise. In particular, you & Will no how to make lots of program
equivalences that I don't. That's where the action is, I think.
> > My problem was that the other topologists weren't interested my
> > work. Doesn't mean my work was lousy. I thought it was ahead
> > (and before!) of it's time.
>
> Sure! Your work on denotational semantics is also way ahead of its
> time, obviously.
No, of course not. At best, it's like my simpler proof of the
standard reduction theorem in LC & LC_v: a simpler proof for simpler
minds! My topology I'll make a stronger defense of :)
> > There's a general point here: just because you know more than I do
> > about DS doesn't mean the little I've figured out is false.
>
> True. I did not say that your construction doesn't construct
> anything at all. However, the something that it does construct is
> not something that would be very useful in the context of this
> discussion.
That's fine, I'll take uselessness. But I gotta start somewhere!!!
> > I have no idea [ ... ]
> ^^^^^^^^^^^^^^
>
> Very telling...
I'll take that :) That was dumb of me, and I've corrected it.
--
Bill <http://www.math.nwu.edu/~richter>
Bill Richter
> > > (I leave it as an exercise to you what the intended result is.
> > > Hint: It is easy because it is a standard example.)
> >
> > I have no idea, but I'll look in Schmidt. Thanks for the
> > exercise!
>
> Bill, it's the factorial function.
Thanks, David, I figured that out. Here was my error:
According to your construction, your resulting F(x0) would be
bottom.
I guess you're right! Since x0 is undefined everywhere,
R(x0) = x0
Bah.
R(x)(0) = 1 no matter what the function x in X = (N -> N_bottom) is.
So R^k(x0) is the factorial function on the subset {0,1,...,k-1} and
undefined on the infinite subset {k,k+1,...}. Back to me:
and so we see that R^n(x0) is never in A, for any n, so we set
F(x0) = bottom
Bah. The reason that F(x0) = bottom, as Matthias claimed, is that
R^k(x0) is never a total function, for any k.
So what Matthias seems to be saying, and David you seem to understand,
is that what you want is
least-upper-bound { R^n(x0) : n = 0,1,2,... }
and that's a total function, an element of A, the factorial function!
That's a good exercise. Why is this important in programming
languages? I prefer my answer of bottom, since that sounds like what
the LC/LC_v standard reduction function does... To pull off this
stunt, we'd need the sets A, X & Y to be CPOs, I hadn't considered
that. I was using the fact that (X -> Y_bottom) is a CPO, but that's
a pretty simple CPO.
--
Bill <http://www.math.nwu.edu/~richter>
Matthias Blume
> Matthias Blume <matt...@shimizu-blume.com> replies to me:
>
> > > If you can show me a definition of Phi that does not mention or
> > > refer to curly-E, then -- and only then -- have you succeeded
> > > in giving a compositional definition.
> > >
> > > I'm sure that's false, Matthias. I'm sure that compositionality
> > > means exactly that this equation is true:
> > >
> > > curly-E[[ (A B) ]] = Phi( curly-E[[ A ]], curly-E[[ B ]] )
> > >
> > > If you think otherwise, can you give me a citation?
> > >
> > > It's true that in Schmidt's structural induction technique, one
> > > must give a `definition of Phi that does not mention or refer to
> > > curly-E'.
> >
> > Forget about the word "compositional". The fact is that what I
> > describe is what's required. If you want to call it something else
> > than "compositional", more power to you.
>
> That sounds like a huge admission, Matthias! Thanks! Let's be sure,
> though, let's go back to Will letter of 12 Jul:
>
> This is not a matter of opinion, but a matter of mathematics, and
> very simple math at that: whether Richter's formulation of his own
> semantics is compositional. [...] That is an affront to all
> mathematicians.
>
> Sounds like you're saying my definition is compositional, and that
> means we've got nothing to argue about, there's no affront. Right?
I am not saying any such thing. I simply offered to avoid the word
"compositional" in the future -- in order to avoid having you further
insist on using it in a sense that is not the one intended.
By the way, notice that the operative phrase in what Will wrote is
"*formulation* ... is compositional". In other words, this is not
about whether or not a function is compositional, it is about whether
or not the *definition* of the function is compositional -- which in
this context means that the function has been defined by induction on
the structure of the language phrase that it is trying to give meaning
to.
Jim Bender
figure out whether it will rain?
"Bill Richter" <ric...@conley.math.northwestern.edu> wrote in message
news:fqr8i4v...@conley.math.northwestern.edu...
> David Rush <ku...@bellsouth.net> replies to me & Matthias:
>
> > > > (I leave it as an exercise to you what the intended result is.
> > > > Hint: It is easy because it is a standard example.)
> > >
> > > I have no idea, but I'll look in Schmidt. Thanks for the
> > > exercise!
> >
> > Bill, it's the factorial function.
>
> Thanks, David, I figured that out. Here was my error:
>
[... lots of "math" snipped...]
WSFP!
Bill Richter
> By the way, notice that the operative phrase in what Will wrote is
> "*formulation* ... is compositional". In other words, this is not
> about whether or not a function is compositional, it is about
> whether or not the *definition* of the function is compositional --
> which in this context means that the function has been defined by
> induction on the structure of the language phrase that it is trying
> to give meaning to.
Thanks, Matthias, but this is incorrect AFAIK. Cartwright and
Felleisen's "Extensible Denotational" paper on PLT says on p 6:
[The map from syntactic domains to semantic domains] satisfies the law
of compositionality: the interpretation of a phrase is a function of
the interpretation of the sub-phrases.
So it's the *function* curly-E that's supposed to satisfy the law of
compositionality. Not the *formulation*!
So if you guys define the notion of a compositional formulation (use
Schmidt's structural induction etc), then possibly I violate this
condition, but it's not something I've been arguing about!!!
Actually I've argued it once, and I repeat, since I didn't get a
response. Here's an edition of what I wrote to you on Jul 2:
Now let me claim, after the fact, that my f really can be
constructed by structural recursion!
Assume for now my claim that f & Phi can actually be constructed as
total mathematical function. Let's forget that f has been defined!
Now we can use this f/Phi equation above to define f by structural
induction. Of course we need lots of other such equations, such as
f [[ (A) ]] = Phi_0( f [[ A ]] )
but let's assume I have all these other function Phi_0. I can
certainly do the base cases, defining f on variables and constants,
numbers, literals etc. Now I've got a structural recursion
construction of f, and that's perfectly legitimate until somebody
restricts the class of Phi, as Boolos & Jeffrey do in a much
simpler context.
Thus, I firmly believe that the notion is that of a
compositional DS semantic function
and *not* a
compositional formulation of a DS semantic function.
Here's what Stephen B posted from Schmidt to get the ball rolling:
> "the meaning of a syntax phrase may only be defined in terms of the
> meanings of its proper subparts"
That's a quality of the semantic function and *not* it's formulation.
Just like Cartwright and Felleisen wrote.
But, I claim that any compositional semantic function can be hogtied
into the structural induction framework, just as I explained above.
I'm not positive about this, but it looks OK to me. Anyway, this
certainly isn't what we've been arguing about.
I thought we were arguing about whether my function curly-E was a
well-defined total mathematical function. And finally someone (you,
Matthias) responded to my inductive proof, but only to say that it's
not the greatest inductive function constructor since Swiss cheese.
Can you say whether you think it's correct, and whether my function
(and not it's formulation) is compositional?
> > > Forget about the word "compositional". The fact is that what I
> > > describe is what's required. If you want to call it something
> > > else than "compositional", more power to you.
> >
> > That sounds like a huge admission, Matthias! Thanks! Let's be
> > sure, though, let's go back to Will letter of 12 Jul:
> >
> > a matter of mathematics, and very simple math at that: whether
> > Richter's formulation of his own semantics is compositional.
> >
> > Sounds like you're saying my definition is compositional, and that
> > means we've got nothing to argue about, there's no affront.
> > Right?
>
> I am not saying any such thing. I simply offered to avoid the word
> "compositional" in the future -- in order to avoid having you
> further insist on using it in a sense that is not the one intended.
Matthias, I want to stop feuding. If you mean my curly-E is
compositional, but I "violated the spirit of compositionality", then
that's fine.
I'm just worried about the "letter of the law of compositionality".
Clearly that's what Will C is talking about. If it's simple math,
it's gotta be the letter of the law, not the spirit. If it's the
"letter of the law of the formulation of the law of compositionality"
then it's gotta be stated definitively somewhere. It can't be
folklore, or this is the way the culture of DS works... That would be
fine, but it wouldn't be "simple math".
--
Bill <http://www.math.nwu.edu/~richter>
Shriram Krishnamurthi
> Sounds like you're saying my definition is compositional, and that
> means we've got nothing to argue about, there's no affront. Right?
No, he's saying nothing of the sort. What he's saying, since it seems
impossible to do something so mere as give you a hint and hope you
will get it, is to indicate that it's simply not worth arguing about
this with you. He's even willing to concede something Matthias would
never ever concede in reasonable company, just to get this over with.
Bill, I thought you were heading off into the sunset to do your lambda
something calculations. It's a tribute to your genius that you've
managed to snooker this ng into another round of 100+ messages on a
topic that you yourself had lain to rest (or so we foolishly
imagined), but haven't you proven your point by now?
Shriram
Bill Richter
> Bill, I thought you were heading off into the sunset to do your
> lambda something calculations. It's a tribute to your genius that
> you've managed to snooker this ng into another round of 100+
> messages on a topic that you yourself had lain to rest (or so we
> foolishly imagined), but haven't you proven your point by now?
Shriram, that's funny! We ought to settle the charge Will raised:
This is a matter of very simple math: whether Richter's formulation
of his own semantics is compositional. ... flimsy credentials
... affront to all mathematicians.
Maybe this has all been a spectacular miscommunication. I've been
trying to prove that my simple DS function curly-E is compositional.
Matthias B said that Will meant my formulation was non-compositional.
I'm not even sure what it means for a formulation to be compositional,
and I certainly don't know how to express it in "simple math."
So maybe we've just been at cross purposes for 1000 posts. According
to Cartwright and Felleisen, compositionality is indeed a property of
DS functions, and not their formulations.
If someone can phrase formulation-compositionality in simple math,
then I bet I can show that any compositional DS function is can be
formulated compositionally. But that's a side issue for now.
> > Sounds like you're saying my definition is compositional, and that
> > means we've got nothing to argue about, there's no affront.
> > Right?
>
> No, he's saying nothing of the sort. What he's saying, since it
> seems impossible to do something so mere as give you a hint and hope
> you will get it, is to indicate that it's simply not worth arguing
> about this with you. He's even willing to concede something
> Matthias would never ever concede in reasonable company, just to get
> this over with.
That's not too polite, Shriram. We've been at loggerheads since your
long post about structural vs generative recursion. This is a similar
issue, and there's plenty of room for honest confusion. Even if there
is a simple mathematical distinction between structural vs generative
recursion (and Felleisen couldn't tell me what it was: he just sent me
to web sites & books), that's a matter of algorithms. We're talking
about functions now. So you're kinda saying that the `algorithm' that
defines the DS function should be structurally recursive? That's thin
ice. If I said it, folks would spank for confusing OpS & DS :)
--
Bill <http://www.math.nwu.edu/~richter>
William D Clinger
> I'm not even sure what it means for a formulation to be compositional,
> and I certainly don't know how to express it in "simple math."
I'm not sure I can use simple math to express the number of Schemers
who have defined "compositional" for Richter: it may take more than
10 fingers.
> If someone can phrase formulation-compositionality in simple math,
Sorry, we'd want to use the concept of induction.
> That's not too polite, Shriram. We've been at loggerheads since your
> long post about structural vs generative recursion. This is a similar
> issue, and there's plenty of room for honest confusion. Even if there
> is a simple mathematical distinction between structural vs generative
> recursion (and Felleisen couldn't tell me what it was: he just sent me
> to web sites & books), that's a matter of algorithms. We're talking
> about functions now. So you're kinda saying that the `algorithm' that
> defines the DS function should be structurally recursive? That's thin
> ice. If I said it, folks would spank for confusing OpS & DS :)
Mathematicians recognize the distinction between inductive definitions
and arbitrary circular definitions. Richter doesn't. He calls that
distinction "thin ice".
Riddle: What does Richter have in common with the non-fixed-point
operator that he defined?
Answer: Both discard information, which makes it hard to rise above
bottom.
Will
NJDSS Editorial Collective
Actually, there are dissident unemployed mathematicians here in Nepal
who are currently bidding on the Math Cabal enforcement contracts. As
a major academic publishing voice for the disenfranchised academicians
in the developing world, we at the Nepalese Journal for
Deconstructionist Sociologists and Sheep-herders have been asked to
help mediate the negotiations.
In short how would you feel about black attack-yaks?
david rush
--
(I just couldn't resist any longer)
David Rush
> Bah.
> Bah.
> is that what you want is
>
> least-upper-bound { R^n(x0) : n = 0,1,2,... }
>
> and that's a total function, an element of A, the factorial function!
>
> That's a good exercise. Why is this important in programming
> languages?
Because we regualrly write programs which compute the value of factorial
using almost exactly the formulation that Matthias so verbosely
presented. I didn't understand it in anything like the way that you
did. I could see the inductive structure in his description because I
have written code like this probably thousands of times.
> I prefer my answer of bottom, since that sounds like what
> the LC/LC_v standard reduction function does...
This is why it is *so* necessary to actually write code in order to
understand what we are doing. The purpose of DS is to reason about
real programs that we write, so Computer Scientists are more like
physicists than mathematicians (this is also why CPS is so important,
but that's not germaine to this discussion).
> To pull off this stunt, we'd need the sets A, X & Y to be CPOs,
Surprise!
david rush
--
Computers save time like kudzu prevents soil erosion.
-- Michael J. Fromberger (on comp.lang.scheme)
Bill Richter
> > That's a good exercise. Why is this important in programming
> > languages?
>
> Because we regualrly write programs which compute the value of
> factorial using almost exactly the formulation that Matthias so
> verbosely presented.
Wow!
> > I prefer my answer of bottom, since that sounds like what the
> > LC/LC_v standard reduction function does...
>
> This is why it is *so* necessary to actually write code in order to
> understand what we are doing. The purpose of DS is to reason about
> real programs that we write, so Computer Scientists are more like
> physicists than mathematicians (this is also why CPS is so
> important, but that's not germaine to this discussion).
Please say more, David. You're talking about DS uses that are beyond
me. Do you have a reference?
Bill Richter
> > I'm not even sure what it means for a formulation to be
> > compositional, and I certainly don't know how to express it in
> > "simple math."
>
> I'm not sure I can use simple math to express the number of Schemers
> who have defined "compositional" for Richter: it may take more than
> 10 fingers.
Maybe Will, but nobody's given a reference. Anyway, I was just
covering my butt on my claim that
I bet I can show that any compositional DS function can be
formulated compositionally.
I'm hedging here: let's get a precise definition and reference first.
I think you guys all blew the definition of compositionality. I think
you've replaced the definition of
compositional DS function
with a technique for producing such compositional DS functions.
In practice, maybe there's no real penalty for this confusion, because
I'm sure the best way to do DS functions is with this technique
(structural induction + Scott models). But still, that's an error.
To clarify, and to repeat myself, Cartwright and Felleisen's
"Extensible Denotational" paper on PLT says on p 6:
[The map from syntactic domains to semantic domains] satisfies the law
of compositionality: the interpretation of a phrase is a function of
the interpretation of the sub-phrases.
So it's the *function* curly-E that's supposed to satisfy the law of
compositionality. Not the *formulation*!
AFAIK nobody here understands this, because nobody's responded.
> > If someone can phrase formulation-compositionality in simple math,
>
> Sorry, we'd want to use the concept of induction.
:-D I think I understand induction better than you guys.
> Mathematicians recognize the distinction between inductive
> definitions and arbitrary circular definitions. Richter doesn't.
My definition of curly-E wasn't circular. But AFAIK nobody read my
proof, and this sounds like a false conjecture about what I did.
Since the one thing you guys understand is structural induction (and
it's a great technique!), I think you guys superimposed my proof
(which instead followed the standard reduction function construction)
onto structural induction, where it became a huge error. Maybe.
> Riddle: What does Richter have in common with the non-fixed-point
> operator that he defined?
>
> Answer: Both discard information, which makes it hard to rise above
> bottom.
Will, let's say this joke replaces your earlier charge of "affront to
all mathematicians". This one is funny, and I don't have to defend
myself against it, the honor of math isn't at stake. I suppose it's
even true, my simple DS function specifies non-call/cc Scheme, but not
using the Scott models must discard information. I'll believe that.
> Bill Richter says he still needs help:
Will, I like the way you doctor the 1st lines, maybe you got it from
me, but you're funnier, like "> Richter fantasized".
I'd put it like this: I've learned a lot from you guys, and I'm really
grateful, but we can't work together because you guys haven't learned
anything from me. Maybe you guys just don't have confidence in your
math skills to admit there's things you don't know, or possibly make
errors in public (as I have!). So rather than take a chance at making
a mistake, you shower me with contempt? Who knows. It's not working.
So I think we're done, thanks, goodbye, I'll be back if I ever build
some good program equivalences into my non-CPO DS (and K-ify it), but
I don't know when I'm gonna find time to work on, it just doesn't seem
like a productive way for me to spend my time. I just wanted to be
certain of that, and that's why I subjected c.l.s. to my theories for
the last month. I have a chance in the math biz yet, but it's a
longshot, so I wanted to rule out scheme first. Thanks.
--
Bill <http://www.math.nwu.edu/~richter>
Matthias Blume
> AFAIK nobody here understands this, because nobody's responded.
That's right. Satisfied? Now go away.
ozan s yigit
> > AFAIK nobody here understands this, because nobody's responded.
>
> That's right. Satisfied? Now go away.
what, you expect him to give up on these sharp c.l.s guys and the free
theory of computing and math education he's been getting, and instead
write up his crank math for a peer review? hope springs eternal... :)
oz
---
you take a banana, you get a lunar landscape. -- j. van wijk
Bill Richter
> > So what Matthias seems to be saying, and David you seem to
> > understand, is that what you want is
> >
> > least-upper-bound { R^n(x0) : n = 0,1,2,... }
> >
> > and that's a total function, an element of A, the factorial
> > function!
> >
> > That's a good exercise. Why is this important in programming
> > languages?
>
> Because we regualrly write programs which compute the value of
> factorial using almost exactly the formulation that Matthias so
> verbosely presented.
Thanks, David, and now I understand Matthias's original objection! I
didn't notice that his R was the fixed point operator for the
factorial function. But I like this! Matthias's R was a map
R: (N -> N_bottom) ---> (N -> N_bottom)
defined by
R(f)(n) = (if (= n 0)
1
(* n (f (- n 1)))))
and that's exactly what Schmidt would say to do in order to make a
function out of the factorial "procedure"
(define (f n)
(if (= n 0)
1
(* n (f (- n 1)))))
We all understand this, I've posted this several times, we take f_0 to
be the constant bottom function, and then
factorial = least-upper-bound{ R^k(f_0) : k = 0,1,2,... } in (N -> N)
Matthias misused my lemma and failed to get factorial, but that's
fine. Here's how you could get factorial out of my lemma. Let
X = (N -> N_bottom) x N
Y = N
with A the subset of X defined by
A = { (f,x): f(x) \ne bottom, i.e. f(x) defined }
Then there's the obvious map
alpha: A ---> Y
(f,x) |--> f(x)
and we define a reduction operator on X (I have to use a new letter)
rho: X ---> X
(f,x) |--> (R(f),x)
Now my induction lemma asserts there is a function
F: X ---> Y_bottom
F(p) = alpha(rho^n(p)), if n is the least nonnegative integer such
that rho^n(p) belongs to the subset A and
all rho^i(p) are defined for 0 \le i \le n
bottom, otherwise.
So F applies the fixed point operator R to f until x is defined:
F( (f,x) ) = R^n(f)(x) for the least nonnegative integer such
that R^n(f)(x) is defined, i.e.
(R^n(f))(x) \ne bottom
Now we get factorial to be the composite
N -G--> X -F--> Y = N
where G is the simple "startup" function
G(x) = (f_0, x) in X.
Notice the similarity to the usual Schmidt least fixed point game?
There's a way I can produce factorial with less CPO talk. My lemma
obviously sounds a lot like minimizing recursion, so if I can do my
lemma, I can do minimizing recursion, and Boolos & Jeffrey prove that
primitive recursion (like factorial) can be rephrased minimizing
recursion (plus composition, etc). Their proof of this looked pretty
thick, and I think I prefer the least fixed point approach above.
But let's deduce minimizing recursion from my lemma.
Suppose we have a function
beta: W x N ---> N_bottom
for any set W, and N = nonneg integers as usual, and we want to define
H: X ---> N_bottom
H(x) = least nonnegative integer n such that beta(x,n) = 0 and
beta(x,i) \ne bottom for 0 \le i \le n
This follows from my induction lemma in a more straightforward way.
Again, we set up the larger problem:
X = W x N x N
A = W x 0 x N subset X
Y = N
alpha: A ---> Y = N the third projection.
Now we define our reduction operator
rho: X ---> X_bottom
rho(x, n) = (x, beta(x,n+1), n+1)
Let's iterate this. For k \ge 0, we have
rho^k(x, n) = (x, beta(x,n+k), n+k)
My simple induction lemma now produces a map
F: X ---> Y_bottom
F(x,y,n) = n, if y = 0
n+k, if k > 0 is the least integer with beta(x,n+k) = 0, &
all beta(x,n+i) \ne bottom for 0 \le i \le n
bottom, otherwise.
Now as above, define G: W ---> X to be the simple startup function
G(x) = (x, beta(x,0), 0)
And now the composite
H: W -G--> X -F--> N_bottom
is our minimizing recursive function
H: X ---> N_bottom
H(x) = least nonnegative integer n such that beta(x,n) = 0 and
beta(x,i) \ne bottom for 0 \le i \le n
\qed
> I didn't understand it in anything like the way that you did.
Yeah, me neither :) I meant for R to be something like the LC standard
reduction function, which reduces the leftmost lambda `redex'
((lambda x. body) arg).
That's a long way (mentally) from Matthias's fixed point operator for
factorial, so I was plenny confused :) I thought Matthias was saying
the interpreter was supposed to calculate a limit of partial functions
and hopefully getting a total functions! That would've blown me away!
> I could see the inductive structure in his description because I
> have written code like this probably thousands of times.
Once you explained that, it clicked that it was really the simple
Schmidt game for factorial. So to some extent Matthias was making the
ridiculous assertion that the LC_v standard reduction function isn't
smart enough to calculate factorials. Anyway, all's fair in love &
usenet, and it was a helpful example. Thanks again, y'all!
--
Bill <http://www.math.nwu.edu/~richter>
Thien-Thi Nguyen
> My proof is 99% as rigorous as Will's.
rigor is not statistical.
thi
Bill Richter
> > My proof is 99% as rigorous as Will's.
>
> rigor is not statistical.
You have me there, Thi :) What's true is:
1] My formulas are merely simplifications/clarifications of the
opaque-looking R5RS DS code, and I think they're quite helpful.
2] There's some rigor problems with my code, in that I ignored error
R5RS DS messages, except insofar as I needed them. R5RS DS is quite
careful about error messages, `wrong number of args' etc. That's a
fixable problem, and Al* P's call/cc exercise flushed out one bug.
--
Bill <http://www.math.nwu.edu/~richter>
Joe Marshall
"Bill Richter" <ric...@hilbert.math.northwestern.edu> wrote in message
news:fqr8hgx...@hilbert.math.northwestern.edu...
> Thien-Thi Nguyen <t...@glug.org> replies to me:
>
> > > My proof is 99% as rigorous as Will's.
> >
> > rigor is not statistical.
>
> You have me there, Thi :) What's true is:
>
> 1] My formulas are merely simplifications/clarifications of the
> opaque-looking R5RS DS code, and I think they're quite helpful.
Many people in this newsgroup believe that the above statement
is wrong.
>
> 2] There's some rigor problems with my code, in that I ignored error
> R5RS DS messages, except insofar as I needed them. R5RS DS is quite
> careful about error messages, `wrong number of args' etc. That's a
> fixable problem, and Al* P's call/cc exercise flushed out one bug.
I don't think too many people have a problem with this statement,
though.
Bill Richter
> > 1] My formulas are merely simplifications/clarifications of the
> > opaque-looking R5RS DS code, and I think they're quite helpful.
>
> Many people in this newsgroup believe that the above statement is
> wrong.
Joe, some folks flamed me, but I don't think anybody thought about my
code. No flamers made any specific complaints, and I think they just
dismissed my DS code since others were attacking me for my CPO-less
DS. But there's no connection. My mods are completely derived from
the R5RS DS code, and are merely simplifications of the R5RS DS code.
Let's just look at my 1st formula. For a number nu, I claim that
(curly-E[[ nu ]] rho kappa sigma) = (kappa <nu> sigma)
Does somebody actually think this is false??? I'll prove it:
I'm writing curly-E in uncurried form as
curly-E: Expressions ---> (U x K x S -> A)
The number nu (0 for us) is a constant in our program, and R5RS says
at the beginning of sec 7.2.3 that for a constant L, we have
(curly-E[[ L ]] rho kappa sigma)
= send (curly-K[[ L ]]) kappa sigma
where curly-K: Constants ---> E is deliberately not defined, but we
can safely assume that
curly-K[[ nu ]] = nu in N = natural numbers subset E
where by abuse of notation, I'm writing nu for both the constant nu
and the natural number nu. Schmidt would want to write 0 and zero to
differentiate these 2 concepts. Send passes a single value to kappa:
send: E x K x S ---> A
(send e kappa sigma) = (kappa <e> sigma)
Thus,
(curly-E[[ nu ]] rho kappa)
= (send (curly-K[[ nu ]]) kappa sigma)
= (kappa <nu> sigma)
\qed
Note: I just think it's simpler to write/understand
(curly-E[[ nu ]] rho kappa sigma) = (kappa <nu> sigma)
than the equivalent R5RS version:
curly-E[[ L ]] = \rho kappa. send (curly-K[[ L ]]) kappa
send: E -> K -> C
send = \e kappa. kappa <e>
To me, the R5RS version is just hard to read/understand. I also think
it's simpler to write the domain K of continuations as
K = E* x S ---> A
I can see now that curly-E[[ nu ]] just ignores the environment
applies kappa to the one-element list <nu>, using the same store. I
imagine others can see that from the two R5RS formulas.
> > 2] There's some rigor problems with my code, in that I ignored
> > error R5RS DS messages, except insofar as I needed them. R5RS DS
> > is quite careful about error messages, `wrong number of args' etc.
> > That's a fixable problem, and Al* P's call/cc exercise flushed out
> > one bug.
>
> I don't think too many people have a problem with this statement,
> though.
I'm lost, Joe. If [2] is OK, what's `believed' to be `wrong' in [1]?
--
Bill <http://www.math.nwu.edu/~richter>
John Tobey
> This is mostly irrelevant to your points, Bill. Or is it? I'm too tired
> to tell...(I thought it was relevant when I started)
>
> Bill Richter <ric...@hilbert.math.northwestern.edu> writes:
>> Mathematically, numbers may be arranged into a tower of subtypes in
>> which each level is a subset of the level above it:
>>
>> number
>> complex
>> real
>> rational
>> integer
>
> Yes, but this ignores the lovely exact/inexact complication that Scheme
> makes in concession to real-world computational issues.
I would phrase that differently. "... that Scheme *permits* in
concession to real-world ..." R5RS defines a set of languages
parametrized by its optional features and implementation dependencies.
As I read it, R5RS-conforming Schemes need not even support negative
exact integers. How many natural numbers must be supported is
unclear, but I would estimate conservatively:
(string-length (symbol->string 'call-with-current-continuation))
== 30
I would be interested in some explanation of the R5RS formal semantics
notation (without having to order the book referenced therein), but I
do not consider inexactness, etc., essential to such an explanation.
-John