On 01/02/2009, at 8:49 PM, Devin Mullins wrote:
I'm reading SPJ's "The Implementation of Functional Programming Languages," and on page 32, it defines the multiplication operator in its extended lambda calculus as: Eval[[ * ]] a b = a x b Eval[[ * ]] _|_ b = _|_ Eval[[ * ]] a _|_ = _|_
Is that complete? What are the denotational semantics of * applied to things not in the domain of the multiplication operator x, such as TRUE (in the extended lambda defined by this book) and functions (in normal lambda calc)? Do these things just eval to bottom? Or is this just to be ignored, since the extended calculus will only be applied to properly "typed" expressions in the context of this book?
Hi Devin, I don't think that the section of the book in question is intended to be rigorous. (page 30. "this account is greatly simplified"). As noted in the text, the domain of values produced by Eval is not specified, so it is hard to be precise (though there is a reference to Scott's Domain Theory). However, I agree with you that the equation for multiplication looks under-specified. Obviously any reasonable domain will include (non- bottom) values on which multiplication is not defined. Without any explicit quantification, it is hard to say what values 'a' and 'b' range over. It is possible that they range over the entire domain, or some proper subset. The text also assumes we all agree on the definition of the 'x' (multiplication) function. Though it ought to be specified in a more rigorous exposition. As you suggest, it may be possible to work around this by imposing some kind of typing restriction to the language, though this does not appear to be stated in this particular section of the book. Perhaps this is mentioned elsewhere; I have not checked. Another possible solution is to sweep it all into the definition of the 'x' function. But if that were so, why bother handling bottom explicitly, but not the other possible cases? I guess the best we can say is that the meaning of multiplication applied to non-bottom non-numeric arguments is not defined (in this section of the text). Cheers, Bernie.