[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)

[Ian MacLarty]

On 15 Dec 2005, at 11:35, Mark Brown wrote:

> On 15-Dec-2005, Ian MacLarty <maclarty at cs.mu.OZ.AU> wrote:
>> On Thu, Dec 15, 2005 at 04:06:54PM +1100, Mark Brown wrote:
>>
>>> + at item @code{infer_purity @var{Goal}}
>>> +Introduces a scope within which the purity of all goals is inferred
>>> +by the compiler.
>>
>> I don't like this sentence.  It seems to suggest that the compiler
>> doesn't infer the purity of goals not in an infer_purity scope (which 
>> it
>> must in order to prove the code is pure).
>
> Okay.  Actually, I'll go through the whole change and make sure this
> implicit purity thing is dealt with consistently, since I don't think 
> the
> semantics chapter deals with it very well as it stands.
>
> Incidentally, should that scope perhaps be named "implicit_purity" 
> instead?
> I was undecided which one was better when I originally wrote it, but 
> given
> the objection above I think "infer_purity" is probably the poorer 
> choice.
> It just seemed to be more consistent with "--infer-types" and
> "--infer-modes".
>
> Another alternative is a set of scopes which allow implicit purity, 
> but which
> also assert what the purity of the scope actually is.  That is, these 
> scopes
> would be "pure_implicit", "semipure_implicit" and "impure_implicit", 
> and
> they would be similar to the "promise_*_implicit" scopes that have been
> removed, except that they wouldn't be making any promises.  Come to 
> think of
> it, I like these scopes better, but I'd be happier if I could think of
> better names for them.
>

I also prefer that idea.  What about just having impure( goals...) or 
semipure( goals...), so it's the same as having impure or semipure 
before a call, but you can have them around an arbitrary goal?

>>
>>>  @table @dfn
>>>  @item pure
>>> -For pure procedures, the set of solutions depends only on the
>>> -values of the input arguments.
>>> -They do not interact with the ``real'' world (i.e., do any
>>> -input/output) without taking an io.state (@pxref{Types}) as input 
>>> and
>>> -returning one as output, and do not change the value of any data
>>> -structure that will not be undone on backtracking (unless the data
>>> -structure would be unreachable on backtracking).  Note that equality
>>> -axioms are important when considering the value of data structures.
>>> +For pure predicates and functions, there must exist a declarative 
>>> semantics
>>> +(that is, a set of ground solutions) which, given the bindings of
>>> +arguments when called, fully determines all possible bindings at 
>>> exit.
>>> +All pure functions must be referentially transparent in the sense 
>>> that
>>> +any two expressions which are syntactically equal must be 
>>> semantically
>>> +equal.
>>> +
>>
>> Can you leave the sentence "For pure procedures, the set of solutions
>> depends only on the values of the input arguments." in?  In my 
>> (humble)
>> opinion it's easier to understand than what you've replaced it with.
>
> I removed it because I found it objectionable on a couple of grounds:
>
> 	- It isn't really procedures that are pure, it is predicates and
> 	  functions that are.  All of the procedures (i.e., modes) of a
> 	  predicate or function must agree on the declarative semantics
> 	  for it to be pure, but that first sentence doesn't impose this
> 	  requirement.
>
> 	- When you have partially instantiated data (e.g., solver variables),
> 	  it doesn't make much sense to talk about input and output arguments.
> 	  They tend to be all inputs, and they don't really have a value as
> 	  such -- they have a domain (i.e., set of values) at entry and a
> 	  possibly smaller domain at exit.
>

Good points.

> How does the following sound:
>
> 	For pure predicates and functions, the set of solutions depends
> 	only on the initial bindings of the arguments (including the return
> 	value in the case of functions).  That is, there must exist a
> 	declarative semantics (a set of ground solutions) which, given...
>

Yes that makes for easier reading.

Ian.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------