[m-dev.] Re: [HAL-dev] Adding Herbrand types to Mercury

[Ralph Becket]

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