[m-dev.] Re: [HAL-dev] Solver types reloaded
Ralph Becket
rafe at cs.mu.OZ.AU
Fri Feb 20 17:51:27 AEDT 2004
[This is a repost from earlier in the week that mysteriously didn't
appear on the mercury-developers mailing list.]
Peter Stuckey, Tuesday, 17 February 2004:
>
> > The old proposition was that we write something like
> >
> > :- solver type t
> > ---> varrep(varrep_type `with_inst` varrep_inst)
> > ; f(...)
> > ; g(...)
> > where initialisation is init_t, equality is equal_t, etc.
> >
> > and that
> >
> > - a construction X = varrep(R) would require R to have inst varrep_inst
> > and would result in X having inst any;
> >
> > - a deconstruction varrep(R) = X would require X to have inst any and
> > would result in R having inst varrep_inst.
> >
> > One major problem with this idea is that, as Fergus pointed out, it
> > breaks referential transparency by conflating solver *values* with
> > *representations of solver values*. Logic requires that if S is the set
> > of values that unify with X, then for all Y and Z in S, it must be the
> > case that Y and Z also unify with each other. This doesn't work in the
> > above suggestion for varrep(_) that are as-yet unbound (i.e. are in the
> > solver equivalent of being `free').
> >
> >
> >
> > The new proposition.
> >
> > After a meeting with Fergus and Zoltan, we came up with the following
> > suggestion (as before, the syntax is up for argument once we have the
> > denotational and operational semantics nailed down.)
> >
> > The new proposition is that t would be defined thus:
> >
> > :- solver type t
> > ---> f(...)
> > ; g(...)
> > where constrained is varrep(varrep_type `with_inst` varrep_inst),
> > initialisation is init_t,
> > equality is equal_t,
> > etc.
> >
> > The `constrained is varrep(varrep_type `with_inst` varrep_inst)'
> > fragment defines the reserved tag constructor. This constructor
> > definition is just like other constructors in that it may include
> > multiple, optionally named, fields, although the inst for non-free
> > values of each field must also be provided.
> >
> > [Why would we want to specify the insts for these fields? The canonical
> > justification is if we wanted to define a constrained complex number
> > type as a pair of constrained floats. In this case the subfields
> > for the real and imaginary components would need to have inst any rather
> > than ground. This information has to appear somewhere.]
> >
> > Note that the discriminated union part of the definition `---> f(...) ;
> > g(...)' is optional. If it is omitted, then the type t has just a
> > single constructor, varrep. This may be useful for types like cint and
> > cfloat where other constructors are not needed.
> >
> > The varrep constructor is not usable directly by the solver implementor,
> > however. Instead, the implementor must use the two compiler generated
> > functions
> >
> > % Used for deconstruction.
> > %
> > :- impure func match_varrep(varrep_type :: out(varrep_inst)) = (t :: in(any
> > ))
> > is semidet.
> >
> > % Used for construction.
> > %
> > :- impure func make_varrep(varrep_type :: in(varrep_inst)) = (t :: out(any)
> > )
> > is det.
> >
> > These functions are impure because they should not be reordered with
> > respect to pure goals that may or may not affect the constraint store.
> > (See the referential transparency problem described for the old
> > proposition.) Since they are impure, they have no declarative semantics
> > and the problem with referential transparency goes away: it's the solver
> > implementor's responsibility to ensure purity and include the
> > appropriate promise_pure declarations; we don't need to damage the
> > semantics of pure Mercury to support solver types.
> >
> > A pass in the compiler, occurring after mode analysis and before switch
> > detection (and hence also before determinism analysis) converts calls to
> > match_varrep and make_varrep into the corresponding unifications with
> > the constructor varrep. This means that match_varrep can appear as a
> > unification branch in switches.
> >
> > The discussion continued on to cover issues of groundness and
> > floundering, but as I've been working since 7am I think I'll summarise
> > those items tomorrow morning! (And I'll be providing sample code using
> > the new proposition.)
>
> We need to have some HAL people at these meetings, since
> we have built more solver types.
This was an impromptu meeting that started as a casual chat with Fergus.
But I think it would be useful to have a formal meeting in the near
future with everybody present.
> Three examples, of how they are actually represented
>
>
> Herbrand solvers
>
> :- solver type hlist(T) --->
> []
> ; [T|list(T)]
> ; vartag(cpointer)
>
> Perhaps Herbrand solvers are so special, we dont care to make it
> uniform (in fact I think most of the problems with the discussion
> come from starting with Herbrand solvers)
> Simple external solver
>
> :- solver type bcplex ---> cplex(int)
>
> The int is cplex column number for the variable
Under the new proposal:
:- solver type bcplex
where constrained is cplex(int `with_inst` ground),
initialisation is init_bcplex,
equality is equal_bcplex,
etc.
This has pretty much the same effect as what you wrote except that
access to the constrained constructor cplex/1 must be via the
compiler constructed functions match_cplex and make_cplex.
> More complex external solver
>
>
> :- solver type mcplex ---> var(int) ; val(float)
Under the new proposal:
:- solver type mcplex ---> val(float)
where constrained is var(int `with_inst` ground),
etc.
> we allow simple constants also in the type so that when
> X = 3.0 + Y + 3 * Z
> is mapped to
> N = 3.0, plus(N,Y,T), *(3.0,Z,Z3), plus(T,Z3,X)
> The N = 3 code is simply compiled to N = val(3.0)
Didn't we discuss automatic coercion and decide it wasn't a good idea
(or, at least, that we don't yet know how to make it work well)?
Under the new proposal (without automatic coercion) one would write
X = val(3.0) + Y + val(3.0) * Z
which would map to something like
Tmp1 = val(3.0) + Y, % + is a function
Tmp2 = val(3.0) * Z, % * is a function
Tmp3 = Tmp1 + Tmp2, % + is a function
X = Tmp3 % Solver unification
> A more complex interface solver type
>
> :- solver type icplex --->
> var(int)
> ; val(int)
> ; +(cplex,cplex)
> ; -(cplex,cplex)
> ; x(float,cplex)
Under the new proposal:
:- solver type icplex
---> val(int)
; +(cplex,cplex)
; -(cplex,cplex)
; *(float,cplex)
where constrained is var(int `with_inst` ground),
etc.
And
X = val(3.0) + Y + val(3.0) * Z
would map to something like
Tmp1 = val(3.0) + Y, % +/2 construction
Tmp2 = val(3.0) * Z, % */2 construction
Tmp3 = Tmp1 + Tmp2, % +/2 construction
X = Tmp3 % Solver unification, responsible for
% flattening the constraint
> plus(N,Y,T) :- T = +(N,Y).
> *(F,Z,Z3) :- Z3 = x(F,Z).
>
> and the "eq" constraint flattens the resulting expressions, before
> creating the equality.
>
> Now semantically each of these things has a clear meaning
> (they represent expressions over floats)
> and syntactically also.
>
> The 2 views DO NOT NEED TO ACCORD, as long as the semantic view
> is upheld by the "outside" view of the type!
The "solver magic" is handled in the definition of equality (and,
optionally, comparison) for the solver type.
> My points is that in the last type
> (a) there is no unique way of representing a "variable" value expression
> var(3) and +(var(4),var(6)) can take multiple values
I can't see a problem there.
> (b) the constructors +, - , x are not meaningful in the semantic view
> as constructors, they actually represent functions
> + on floats, - on floats, etc.
Can't the view of "+ as an operator" and "+ as a constructor interpreted
by the equality relation" be shown to be equivalent?
> Now maybe someone can explain how the new formalism does fit with this.
> Maybe I am misunderstadning something.
I'm afraid I'm not clear on the sticking point. Shall we hammer this
out on Thursday?
-- 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