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

[Mark Brown]

(The following issue was discussed in person, but I wish to put it down
here so it's on record.)

On 13-Dec-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Index: doc/reference_manual.texi
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
> retrieving revision 1.340
> diff -u -r1.340 reference_manual.texi
> --- doc/reference_manual.texi	23 Nov 2005 05:11:41 -0000	1.340
> +++ doc/reference_manual.texi	9 Dec 2005 03:44:42 -0000
> @@ -2381,10 +2381,10 @@
>  Referential transparency can be violated if a non-local solver type variable
>  with inst @code{any} is used in a negated context (i.e., the body of a negated
>  goal or the condition of an if-then-else) or in a lambda expression.  Programs
> -are therefore required to place @code{impure} annotations on such goals or
> -lambda expressions, even if they would normally be considered pure.  This
> -impurity propagates through the enclosing goal structure as specified in
> - at ref{Impurity}.
> +are therefore required to place such goals inside a @code{promise_pure},
> + at code{promise_semipure}, or @code{promise_impure} scope, and to declare such
> +lambda expressions to be @code{impure}, even if they would normally be
> +considered pure.

The problem with binding variables in negations or conditions is not one of
referential transparency (at least, I don't see how it is) -- negations which
refer to non-local variables have a perfectly good declarative semantics.  The
real problem is that we implement negation with negation-as-failure, and NAF
is not sound if non-local variables can be bound inside the negation.  The
documentation should reflect this point here, and it would also probably be a
good idea to mention this kind of impurity in the place where we define
"impure".

Cheers,
Mark.

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------