Scheme's Formal Semantics

[jar@cs.cornell.edu (Jonathan Rees)]

   Date: Thu, 11 Mar 93 15:11:55 EST
   From: John D. Ramsdell <ramsdell@linus.mitre.org>

   MEMORY EXHAUSTION: The official semantics always tests whether the
   store is out of memory (fully allocated) before it allocates a new
   location.  We recommend removing these tests and introduce the
   assumption that the store is infinite.

When this last came up on rrrs-authors, there was no objection.  The
change wasn't made for R4RS because all changes were being held
hostage to macros.  I advise the R5RS editor to just go ahead and make
the change for R5RS.

   LETREC EXPRESSIONS AND TAGS ON PROCEDURE VALUES: A procedure object is
   treated in the semantics as a pair, consisting of a store location and
   a functional value. ...

The tags-on-procedures problem was discussed extensively while the
R3RS was being prepared, and the group came down definitively on the
side of being able to do EQV? on procedures in the manner specified in
the report.  So I don't think we need to discuss it again.

The formal semantics differs from the informal semantics in specifying
that (eqv?  (lambda (x) x) (lambda (x) x)) must be false.  Perhaps we
can relax the formal semantics a bit to capture the informal semantics
better, along the lines of the permute/unpermute hack.  I'm not sure
exactly how to do this, however.  You would need a variant of "new"
that might return an already-allocated location belonging to an
"equivalently behaving" procedure.  (The correct constraint involves
an uncomputable condition, but that implies nothing about any
inability to conform to the constraint.)  Making this change would
certainly broaden the set of program transformations and compilation
strategies that are consistent with the formal semantics.  Would that
help in your situation?

Jonathan