[m-dev.] Determinism assertions, and functions whose forward mode fails

[Fergus Henderson]

On 23-Aug-2003, Peter Moulder <pmoulder at mail.csse.monash.edu.au> wrote:
> On Mon, Aug 11, 2003 at 02:17:28AM +1000, Fergus Henderson wrote:
> 
> > There are certainly important practical advantages to [throwing an
> > exception in functions that are undefined for the given arguments].
> > But the declarative semantics with this approach are surprising.
> > For example, in Mercury the goal 
> > 
> > 	some [X `with_type` integer, Y `with_type` integer]
> > 		((X * Y) / Y \= X)
> > 
> > is true.  The same is the case for the analagous goal in Goedel.
> > This is because the although the operational semantics says that
> > 0 / 0 will throw an exception, the declarative semantics says that
> > 0 / 0 has some unspecified value.
> 
> That seems to be a problem with the use of error/exceptions with any det
> procedure, not just functions.

Sure.

> However, I may be misunderstanding
> Fergus' reasons for saying that "the declarative semantics says that
> 0 / 0 has some unspecified value".
> 
> 
> I believe there's a problem with the following sentence of the reference
> manual (node Determinism categories):
> 
> # An annotation of `det' or `multi' is an assertion that for every value
> # each of the inputs, there exists at least one value of the outputs for
> # which the predicate is true, or (in the case of functions) for which
> # the function term is equal to the result term.
> 
> Possibly the sentence should be changed to have some exclusion on inputs
> that don't terminate, like paragraph 2 of the node.

I don't think so.

> However, I don't
> know whether or not one could usefully make such a modification, i.e.
> whether the sentence would still say anything if one did add such an
> exclusion.
> 
> Taking this sentence as it is and by itself, I would be fairly confident
> that the declaration
> 
>   :- mode p(in, in, ..., out, out, ...) is {det or multi}.
> 
> implies:
> 
>   all[In1] all[In2] ... some[Out1] some[Out2] ...
>     p(In1, In2, ..., Out1, Out2, ...).

Yes, that's the intent.

> Picking a random det/multi predicate from the standard library that
> includes a call to error:
> 
>   :- pred string__index_det(string, int, char).
>   :- mode string__index_det(in, in, uo) is det.
>   string__index_det(String, Int, Char) :-
> 	( string__index(String, Int, Char0) ->
> 		Char = Char0
> 	;
> 		error("string__index_det: index out of range")
> 	).
> 
> The corresponding determinism assertion from above:
> 
>   all[String, Int] some[Char] string__index_det(String, Int, Char).
> 
> Considering the case String = "", Int = 5 (i.e. values where the
> string__index call fails), the definition of string__index_det gives
> 
>   all[Char] string__index_det("", 5, Char) <=> (
>     ( false -> ... ; error("...") )
> 
> which simplifies to
> 
>   all[Char] string__index_det("", 5, Char) <=> error("...")
> 
> while the determinism assertion becomes
> 
>   some[Char] string__index_det("", 5, Char)
> 
> Substituting such a value of Char into the previous, we get
> 
>   true <=> error("...")
> 
> which I believe means that compilers are allowed to replace the error
> call with `true' even for values of String,Int like "",5 such that the
> string__index call fails.

That's correct.  However, such a substitution will only be mode-correct
in a context in which the variable 'Char' is not used.

> This makes the error/1 call useless other than in strict sequential
> semantics and other low optimization settings.

Replacing calls to deterministic procedures whose outputs are not used
with 'true' is known as "lazy evaluation", and it was a quite deliberate
design decision to _permit_ this.

The call to error/1 is certainly not useless; without it, the code
would not be mode- or determinism-correct.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------