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

Re: BEGIN in Scheme's Abstract Syntax



>> I propose that we return to the abstract syntax of R3RS.  ...
I misremembered the R3RS abstract syntax.  In R3RS, Both BEGIN
expressions and LAMBDA expression bodies many contain more than one
expression.  Let me restate my proposal.

				 ***

I propose that the abstract syntax of Scheme be amended to include a
BEGIN form and restrict the body of all forms of LAMBDA expressions so
that they contain exactly one expression.  The concrete syntax of
LAMBDA expressions containing more than one expression would be
derived syntax.  In other words, this proposal makes no change to
Scheme's concrete syntax.

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

				 ***

The formal semantics predicts that the application of a function to a
very large number of arguments will never generate a storage error if
the evaluation of each argument allocates no storage.  Yet, all real
implementations will generate some error.  Given the fact that this
and other issues of finiteness of implementations are ignored by the
Scheme semantics, I find it odd that the formal semantics specifies
behavior when the store is finite.  Since the formal semantics does
not specify behavior for all of the case relating to the finiteness of
implementations, I believe it should specify none of these cases.  I
propose that the semantics be rewritten so as to assume that the store
is infinite, which means that for all stores, the new function always
produces a location.

John