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

[Peter Moulder]

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.  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.  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, ...).

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.

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

Similarly for most other uses of error/1 in det/multi procedures.

require.require/2 is an interesting case.  If we accept the predicate
argument as an input, then given:

  :- pred require(pred, string).
  :- mode require((pred) is semidet, in) is det.

it would seem that the declarative semantics of

  require(P, "...")

is simply

  true

even if P is false.

Currently, the definition of require/2 is:

  require(Goal, Message) :-
        ( call(Goal) ->
                true
        ;
                error(Message),
                fail
        ).

Declaratively (eliding type fluff):

  all[Goal, Message] (
     require(Goal, Message) <=>
     (
	call(Goal)
     ;
        not(call(Goal)),
        error(Message),
        false
     )
  ).

Consider the case where Goal = false.  Then we have:

  all[Message] (
    require(false, Message) <=>
    (
      error(Message),
      false
    )
  )

However, applying the paragraph from the reference manual, we also have

  all[Goal, Message] require(Goal, Message)

because we've declared require(in,in) is det.  Substituting into the
above, we get

  all[Message] (
    true <=> (..., false)
  )

which simplifies to simply

  false

so it seems that the standard library is inconsistent.  [Ah, no wonder my
programs don't behave!]

If we were to change the definition of require/2 to remove the `fail'
conjunct, we'd get a different problem when considering Goal = false:

  all[Message] (
    true <=> error(Message)
  )

i.e.

  all[Message] error(Message)

which I believe means that compilers would be allowed to replace all
calls to error/1 with simply `true'.

pjm.

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