[HAL-dev] Re: [m-dev.] Solver types in Mercury - meeting notes and comments
Fergus Henderson
fjh at cs.mu.OZ.AU
Fri Feb 13 18:05:14 AEDT 2004
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
--------------------------------------------------------------------------
More information about the developers
mailing list