[HAL-dev] Re: [m-dev.] Solver types in Mercury - meeting notes and comments

[Fergus Henderson]

On 13-Feb-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> it seems reasonable to me to say that the following
> programs are equivalent under their respective interpretations:
>
> [example deleted]

Your example is reasonable.  But in that example, you only are only
considering one constraint store, the one that contains the final
(ground) answers.  The problems that I see come because the constraint
store is mutable, or because some terms represent non-ground values,
neither of which was present in your example.

> > You are using functional notation for `cf', as if it was a function from
> > int to cfloat, but `cf' is in fact not a mathematical function from int
> > to cfloat.  It is a function from int to "cfloat representation", but if
> > you consider the result type of `cf' to be just cfloat, then it no longer
> > has all of the properties expected of mathematical function, and so using
> > functional notation for it is going to break some of the nice logical
> > properties that we want to be able to rely on.
> 
> I'm using cf as a data constructor: it's part of the language (in a
> logical sense) defined by the program and for which the program
> predicates are defined.
> 
> Can you give me an example illustrating your point?

OK, consider the following procedure.

	:- pred p is semidet.
	p :- 1 >= list.length(std_util.solutions(
		(pred(X::out) is nondet :- Term = f(c), q(X)))).

	... assume suitable definitions of f/1, c/0, and q/1 ...

The laws of logic mean that there can only be at most one value of Term
for which Term = cf(x), which means that the list of solutions can have
length at most one, so a Mercury implementation is permitted to replace
the body of p/0 with `true'.  But your definition of cf/1 does not satisfy
those laws of logic, and so applying the optimization for cf/1 would be
unsound.  If they wanted to preserve soundness, Mercury compilers would
no longer be able to apply optimizations based on the laws of logic.

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