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

*To*: Christian.Queinnec@inria.fr*Subject*: Re: evaluation order for combinations*From*: "John D. Ramsdell" <ramsdell@linus.mitre.org>*Date*: Wed, 30 Mar 1994 11:54:15 -0500*Cc*: rrrs-authors@martigny.ai.mit.edu, ramsdell@linus.mitre.org, anglade@chambord.univ-orleans.fr, lacrampe@chambord.univ-orleans.fr*In-Reply-To*: Your message of "Mon, 21 Mar 1994 11:51:21 +0100." <199403211051.AA14410@cornas.inria.fr>

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.

**References**:**evaluation order for combinations***From:*Christian Queinnec <Christian.Queinnec@inria.fr>

- Prev by Date:
**evaluation order for combinations** - Next by Date:
**quasiquote vs. cons & friends** - Prev by thread:
**evaluation order for combinations** - Next by thread:
**quasiquote vs. cons & friends** - Index(es):