Re: mathematical models

[Matthias Blume <blume@CS.Princeton.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