[m-dev.] Re: [HAL-dev] Adding Herbrand types to Mercury
Ralph Becket
rafe at cs.mu.OZ.AU
Wed Dec 17 10:56:02 AEDT 2003
David Overton, Wednesday, 17 December 2003:
> On Tue, Dec 16, 2003 at 05:40:31PM +1100, Ralph Becket wrote:
> >
> > Since there is no extant documentation concerning these things, I
>
> There is some documentation, e.g.
>
> Mercury mode system, including `any' insts:
> http://www.cs.mu.oz.au/~dmo/dmo-phd-thesis.html
>
> HAL mode system:
> http://www.csse.monash.edu.au/~mbanda/hal/cl2000-hal.ps
>
> Implementation of Herbrand constraints in HAL:
> http://www.csse.monash.edu.au/~mbanda/hal/iclp99-hal.ps
>
> although none of these explicitly describe Mercury's
> `:- solver type' and `:- pragma reserve_tag' declarations.
>
> I've put an updated and expanded copy of the last of these papers on
> your desk at Monash. It addresses a lot of the issues you discuss in
> this email. I think it would be worth a look.
Much appreciated!
> > The reserve_tag pragma adds an extra data constructor (which I'll call
> > '$') to the type t and is roughly the same as saying
> >
> > :- solver type t
> > ---> '$'(herbrand_var(t))
> > ; f
> > ; g(t)
> > where equality is unify_t.
> >
> > where herbrand_var/1 is a private builtin type that might look like
> > this:
> >
> > :- type herbrand_var(T)
> > ---> free
> > ; bound(T).
>
> The `free' case here is really a reference to a PARMA pointer chain.
> The `bound(T)' case does not apply because once a variable of type `t'
> is bound it will be fully dereferenced.
True - I was thinking in terms of traditional Prolog alias structures
rather than PARMA pointer chains when I wrote the above. But either
option is good by me.
> > The effect of the solver modifier on the transformed type definition for
> > t is as follows:
> > - a solver type value with inst *any* is not free and may be any of the
> > data constructors for the type *including* '$';
> > - a solver type value with inst *ground* is not free and may be any of
> > the data constructors for the type *except* '$';
> > - the inst *any* is identical to the inst *ground* for non-solver
> > types.
>
> Not quite true, because a non-solver type could contain solver types.
> E.g.
>
> :- type foo ---> f(bar).
> :- solver type bar.
>
> inst `any' for type `foo' would be equivalent to `bound(f(any))'.
Okay, so in what I wrote above s/solver type value/solver type value or
a non-solver type value containing a solver type value/ and s/non-solver
types/non-solver types that do not contain a solver type value/. Would
you agree?
> > There would be a private builtin initialisation predicate that works for
> > all Herbrand types:
> >
> > :- pred init(<<any_herbrand_type>>).
> > :- mode init(free >> any) is det.
> >
> > init('$'(free)).
>
> The implementation of init/1 would need to initialise the pointer chain
> as a reference to itself.
Under the PARMA scheme.
> > The compiler would insert calls to init for every variable X or Y of
> > type t in order to ensure that
> > - X's inst is converted from free to any for calls that require it and
> > - at least one of X and Y has a non-free inst in a unification X = Y.
>
> I think you only want to add calls to init where it is actually required
> (i.e. where a variable has inst `free' and needs to have inst `any').
> Otherwise you incur unnecessary efficiency penalties. E.g. in a
> unification `X = Y' if you init both X and Y then you get a PARMA chain
> with 2 elements after the unification. If only one of X and Y is inited
> and the other is `free' then you only need a single element chain.
Sorry, that was what I was trying to say (the same line goes for
traditional Prolog alias chains.)
> It is reasonably easy to check where inits need to be inserted during
> mode analysis. In fact the Mercury mode checker already does this,
> although it assumes the init predicate will be called <type>_init_any/1.
> (See modes.m line 2111.)
Righto. I presume the <type>_init_any/1 predicate is defined in the
same module as <type>?
> > There would be a private builtin dereferencing function that works for
> > all Herbrand types:
> >
> > :- func deref(<<any_herbrand_type>>).
> > :- mode deref(any) = any is det.
> >
> > deref(X) = ( if X = '$'(bound(Y)) then deref(Y) else X ).
>
> OK, what you're describing is more of a WAM style variable
> representation. HAL uses PARMA bindings at the moment, do you have a
> good reason for Mercury to use WAM bindings instead?
Not off hand. WAM style is just easier to describe. It's not clear to
me that it makes a huge difference which technology you use behind the
scenes (although my intuition prefers PARMA style.)
> > A special unification predicate for t would be constructed
> > automatically:
> >
> > :- pred unify_t(t, t).
> > :- mode unify_t(in(any), in(any)) is semidet.
> >
> > unify would make use of deref/1 and have (safe) side effects if either
> > of its arguments is bound to '$' or values containing '$'. Its
> > semantics are just what you'd expect. Any side effects due to unify_t
> > are trailed and will be undone on backtracking.
>
> The HAL system also generates special construct and deconstruct
> predicates for each data constructor of each type. I assume this is
> mainly for efficiency reasons -- we want to avoid having to do a general
> unification if we have more specific information about the form of the
> term.
Indeed.
> > * SWITCHES
> >
> > Any disjunction "switching" on a Herbrand value with inst any will be
> > multi if the switch is exhaustive (i.e. tests for every data constructor
> > except '$') and nondet if the switch is not exhaustive (i.e. misses
> > tests for one or more of the data constructors other than '$').
>
> I think this will require modification to switch detection and/or
> determinism analysis to detect the `multi' case.
It's not clear to me that this is a high priority. On the other hand,
it doesn't sound too hard to arrange.
> > * QUESTION ABOUT OTHER SOLVERS
> >
> > It seems to me that the herbrand_var type could be usefully extended to
> > include a hook for other constraints (e.g. for finite domains.) Is it
> > the case that *all* other solver types should (reasonably) also be
> > Herbrand types or not?
>
> Most other solvers will _not_ be Herbrand types. Often, a solver
> variable is an integer representing an index into some sort of global
> table. E.g. see hal1/src/lib/cfloat.m for an example of an interface to
> a CLP(R) solver, and hal1/src/solvers/domain.hal for an example of an
> implementation of a FD solver.
Understood.
> > Once we've got this hammered out, I'm tempted to start working on it.
>
> Ok. Looking forward to it!
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
--------------------------------------------------------------------------
More information about the developers
mailing list