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

[Ralph Becket]

Fergus Henderson, Friday, 13 February 2004:
> On 13-Feb-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > 
> > It's not obvious to me that the distinction is necessary; it's the
> > equality semantics that matter.  For instance, say I have a Herbrand
> > type and I reserve a particular data constructor v(int) to denote (bound
> > or unbound) variables, using ints as variable identifiers.  The truth of
> > v(3) = v(4), say, depends upon the constraint store, not on the integer
> > identifiers alone.
> 
> That's why I think the distinction is necessary!

Let me see if this makes my position any clearer.

The result of an ordinary Mercury program can be seen as equivalent to a
conjunction of unifications where equality is defined as structural
identity for most types and by type-specific predicate for non-canonical
types (i.e.  those with user-defined equality.)

The result of a constraint logic program can be seen as equivalent to a
conjunction of mutually consistent unifications and constraints (with
the same notion of equality as above.)

In each case, what the resulting variable bindings mean depends upon
one's interpretation.

For example, it seems reasonable to me to say that the following
programs are equivalent under their respective interpretations:

CASE 1

X = Y, Y = Z, Z = 42

CASE 2

X = 42, Y = 42, Z = 42

CASE 3

X = v(1), Y = v(2), Z = v(3), v(1) = v(2), v(2) = v(3), v(3) = 42
where v(N) names solver variable N and the solver type defines equality
appropriately.

As I see it, the constraint store is just a place to hold constraints
such as v(2) = v(3) and the solver type equality predicate ensures that
unifications only succeed if they are consistent with the constraint
store.

> 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?  That might help me
see where one of us is going wrong.

Cheers,
-- Ralph
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------