[mercury-users] Re: can one_solution/2 and unsorted_solutions/2 be det?

[Fergus Henderson]

Bart Demoen, you wrote:
> 
> > What is the declarative semantics of `random(N)'?
> 
> I don't know why I am answering this, because you know this: I learned
> it in this Mercury list, maybe even from you
> 
> the random/1 I meant is really a random/3: it has a hidden couple of
> arguments, representing the info needed to compute the next random
> number - initial input = seed - and blablabla
> is that enough ?
> why is my random not pure ?

random/3 (perhaps better named pseudo_random/3) can be pure, but random/1
is not.  Similarly, once/3 could be pure, but once/1 is not.

> now, why is my definition of once/1 with the hidden arguments for
> random not pure ? (modulo trivial rewrite in Mercury)

Because once/1 depends on and updates implicit global state, namely the
random number seed.

Furthermore, even if you use once/3 and thread state arguments through
the program, I think this approach still won't work.  It suffers from
practical problems similar to those suffered by the Hilbert-style choice
functions that Don Smith suggested.  The declarative semantics implies
that it always chooses the same pseudo-random number given the same seed. 
You can't replace pseudo-random choice with genuinely nondeterministic
choice (as would be needed for a concurrent implementation using
OR-parallelism) without breaking those semantics.
To make it sound, I think you'd have to record previous answers
to ensure that the answer didn't change on backtracking.


But in any case, this is all irrelevant, since there is no need to use
once/1 --- just use promise_one_solution/1 and user-defined equality instead.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.