Re: Scheme's Formal Semantics

[John D. Ramsdell <ramsdell@linus.mitre.org>]

> 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 Vlisp research suggests that providing the extra expressivity of
LETREC expressions with side-effect semantics and an equality
predicate for procedures based on a tag directly conflicts with
efforts to formally verify program transformations used in optimizing
Scheme compilers.  Given the lack of interest in verification by most
members of this list, I would be surprized if I could convince members
to reduce the expressivity of Scheme for the sake of formal methods.
When the decision was made to allow comparisons of procedures and
define LETREC expressions in terms of assignment, I was unclear on its
impact on the usefulness of the formal semantics.  I believe the Vlisp
project has made the trade-off quite clear.

> 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.  ....
.....
> .... Would that
> help in your situation?

I do not understand how this change would help to prove the kind of
transformations that are verified for the Vlisp PreScheme compiler.
The compiler proofs make extensive use of the fact that the denotation
of a LAMBDA expression is independent of the store.  I would be very
eager to hear from you if you have a particular technique in mind so
that your suggested change to the semantics would help in those
proofs.  It seems that the extra expressivity of the features
described above preclude verification of the equivalent
transformations.  I have no proof of this statement, and I would be
happy to be shown wrong.

For those with little knowledge of PreScheme, let me fill in a few
details.  PreScheme is a systems programming subset of Scheme used to
implement Scheme48, a byte-code interpreter based Scheme by Jonathan
Rees and Richard Kelsey.  It differs from Scheme mainly in that all
PreScheme programs must be able to be transformed into a form which
requires only a C-like run-time system, i.e. no garbage collection and
no type discrimination at run-time.  Richard has done the bulk of the
work of PreScheme, and is quick to point out that PreScheme could be
used for general systems programming tasks including implementing
operating systems.

In PreScheme, LAMBDA bound variables cannot be modified, procedures
cannot compared, LETREC expression initializers must all be LAMBDA
expressions, and all procedures return exactly one value.  With the
exception of the requirement on the number of return values, all of
the above properties of PreScheme facilitate the verification of
transformation rules for Vlisp PreScheme expressions, though Jonathan
and Richard did not seem to have verifiability as a design goal for
PreScheme.

Vlisp PreScheme is much like PreScheme except that rather than
inheriting its formal semantics from Scheme, its formal semantics are
given in a form that is closer to Muchnik and Pleben's semantics for
Scheme from the 1980 Lisp Conference.  The result is a language with a
useful formal semantics.

John