BEGIN in Scheme's Abstract Syntax

[ramsdell@linus.mitre.org]

In R3RS, the formal semantics of Scheme contains BEGIN forms as part
of its abstract semantics, and the body of LAMBDA expressions are
restricted to contain exactly one form.  In R3.99RS, the formal
semantics of Scheme does not contain BEGIN forms as part of its
abstract semantics, and the body of LAMBDA expressions may contain one
or more expressions.

I propose that we return to the abstract syntax of R3RS.  The major
reason is that when doing proofs about Scheme programs, it is nice to
have one piece of syntax that captures the notion of sequencing which
is independent from the three forms of LAMBDA expressions.

Another potential benefit of this change is one could simplify the
semantics of Scheme by omitting the valuation function for commands,
and define BEGIN in terms of script E as follows.

E[[(BEGIN e)]]        = E[[e]]
E[[(BEGIN e1 e* e2)]] = \rk. E[[e1]] r \v*. E[[(BEGIN e* e2)]] r k

John