[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: wand@ccs.neu.edu*Subject*: Re: mathematical models*From*: Matthias Blume <blume@CS.Princeton.EDU>*Date*: Wed, 04 Jun 1997 10:10:54 -0400*Cc*: Qobi@research.nj.nec.com, rrrs-authors@martigny.ai.mit.edu, hbaker@netcom.com, jgm@cs.cornell.edu, shriram@cs.rice.edu, ramsdell@linus.mitre.org, feeley@iro.umontreal.ca, kelsey@research.nj.nec.com, will@ccs.neu.edu*In-Reply-To*: Your message of "Wed, 4 Jun 1997 09:30:53 -0400 (EDT)"*References*: <199706041330.JAA20338@delphi.ccs.neu.edu>

From: Mitchell Wand <wand@ccs.neu.edu> Subject: Re: mathematical models Date: Wed, 4 Jun 1997 09:30:53 -0400 (EDT) > The R3RS denotational semantics and the ML definition both contain incomplete > or informal specifications of the constants of the language. For example, the > initial dynamic basis in SML (Appendix D of the definition) describes the > arithmetic operations only in an informal way. It does not specify sizes of > integers, what a "real" is, etc. The Scheme number specification is far more > sophisticated. I wouldn't call such a language specification "incomplete". It simply is parameterized over the specification of the initial basis. Of course, one could say that this is a tautology, as we can abstract from every incompleteness in a specification. However, it is fairly common practice not to talk about the constants, because this usually is tedious and has little educational value. (Mind you, there are very interesting aspects to it, and it took a long time for the SML guys to come up with a very good initial basis. Incidentally, this basis is no longer part of the language definition proper; the revised language standard does not contain it. Instead, it has basically assumed the status of a (mandatory) library.) Now, having said all this it should also be noted that Scheme's mathematical definition (the denotational semantics section) is not only incomplete but also wrong. The mistake in it is later "fixed" using English, which is no good when you want to prove something. What I am talking about is the order of argument evaluation. In R4RS there is this funny "function" _permute_ together with _unpermute_ that is supposed to express the fact that the order is unspecified. As it stands using the semantics of R4RS one could prove properties that in reality do not exist. The missing specification only prevents us from proving things that are true, which is a mere incompleteness and not an outright mistake. Of course, getting this right is hairy, which presumably is why nobody has done it. (I would simply fix the order, which also has a couple of other advantages -- such as not having to explain the potential of unspecified behavior.) Regards, -Matthias

**Follow-Ups**:**Re: mathematical models***From:*hbaker@netcom.com (Henry G. Baker)

**References**:**Re: mathematical models***From:*Mitchell Wand <wand@ccs.neu.edu>

- Prev by Date:
**Re: mathematical models** - Next by Date:
**Re: mathematical models** - Prev by thread:
**Re: mathematical models** - Next by thread:
**Re: mathematical models** - Index(es):