Re: evaluation order for combinations

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

I read with interest your article for Lisp Pointers titled "Semantics
of Combinations in Scheme".  The successor to the Vlisp project has
attacked the closely related problem of modifying the formal semantics
of Scheme so as to correctly reflect the intended meaning of an
unspecified value.  (Actually, our efforts are focused on Vlisp
PreScheme, a dialect of Scheme which differs from Scheme in
inessential ways for the purposes of the current discussion.)

Just to refresh everyone's memory, the formal semantics currently
implies that there exists one expressed value other than UNDEFINED
that is used in place of UNSPECIFIED when attaching meaning to a
program.  As a result, the semantics erroneously specifies than

	(eqv? (if #f #f) (if #f #f)) ==> #t

when the intent of the authors is to allow implementations which
produce #f when presented with this expression.

In the standard semantics, the meaning function EE (script E) is
defined by a set of recursive equation.  The meaning of complex
expressions is defined by composing the meanings of the expressions
that make up its parts.

We considered several approaches to modifying the semantics.  For
example, one could define the meaning function as a relation instead
of a function so it could relate several denotations with each
expression.  However, this approach fails to capture the desired
semantics.  Another approach is to replace the answer domain by a set
or sequence of answers, similar to your approach.  However, we were
reluctant to change the denotational domains, and sets or sequences of
answers seemed like they might be messy when mixed with the other
denotational domains.

Leonard Monk suggested the approach we adopted.  Rather than *define*
EE, we *axiomatize* it.  The meaning function is constrained by a set
of recursive axioms.  The constraints on the meaning of a complex
expression is given in terms of the possible values associated with
the expressions that make up its parts.  As a result, there need not
be only one function EE that satisfies all the constraints.  In our
approach, an implementation is correct if the answer produced by a
program is consistent with that predicted by some EE which satisfies
the axioms.

What follows is the equation for one-armed if's which contributes to
the standard definition of EE, the function which associates a
denotation with an expression.

EE[[(if E0 E1)]] 
  = \rk.EE[[E0]] r (single \e.truish e -> 			(*)
				EE[[E1]]rk, 
                                send unspecified k)

I will illustrate our approach to specifying unspecified values with
a modification of this equation.

For all r k s, there exists an e0 such that
  EE[[(if E0 E1)]]rks
    = EE[[E0]] r (single \e.truish e -> 			(**)
			      EE[[E1]]rk, 
                              send e0 k) s

We call this approach the A E approach to unspecified values because a
universally quantified equation which contributes to the definition of
the function which relates expressions to their denotations is replaced
by an existentially quantified equation that axiomizes that function.

Another, completely equivalent method of stating (**) is to
specify that EE[[(if E0 E1)]]rks is a member of the set

{ EE[[E0]] r (single \e.truish e -> EE[[E1]]rk, send e0 k) s | e0 in EV }

where EV is the domain of expressed values.

We find the A E approach to unspecified values extremely useful
because it does not require any changes to the denotational domains.
It is likely that the correct semantics for the evaluation order of
combinations can specified using the same approach.

John

Christian, I will send comments on the text directly to you when time
permits.