[m-dev.] Re: [HAL-dev] Solver types reloaded

[Ralph Becket]

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