[m-dev.] semantics with any insts

[Peter Stuckey]

On 29/03/2006, at 12:19 PM, Peter Schachte wrote:

> Hi all,
>
> Any insts in Mercury cause some real problems for its previously clean
> semantics.  Before we think about adding some new determinisms as
> Peter has suggested, I think we should agree on what the semantics of
> the current ones are.
>
> Prior to any insts, it was pretty simple.  Ignoring types (and
> committed choice determinisms, and bound(...) insts) for the purposes
> of this discussion, the semantics of a free variable could be thought
> of as the universal set of terms, and the semantics of a ground
> variable is a singleton set (or the empty set).  So a mode then
> identifies some arguments as being limited to a singleton set of
> possibilities on call, and the determinism of a mode says how many
> tuples of values could satisfy the goal given that initial inst.  All
> nice and clean.
>
> Now we add any insts.  So free still describes the universal set of
> terms, ground a singleton or empty set, and any describes any set at
> all.  That seems OK.  But now the old determinisms don't make any
> sense semantically.  Usually tell constraints have determinism
> semidet, which indicate that the set of possible solutions is empty or
> a singleton.  But, eg, it's nonsense to say that X < Y has at most one
> solution; it has an infinite number.  So in Mercury with any insts,
> determinisms are purely an operational concept describing backtracking
> behaviour, and have no denotational semantics at all.  If a mode has a
> final inst of any for any of its arguments, it seems fair to argue
> that its semantic determinism can only be nondet.  There may be some
> obscure case where it could be multi, but I can't think of one.  So
> since the determinism carries no semantic information where any insts
> are involved, can't we just omit determinism from any modes?  Or at
> least we should be declaring such modes to be nondet.
>

An answer in CLP (with any insts) is a set of constraints not known to 
be false, and determinism tells you
how many sets of constraints you can have.  This is the S semantics for 
LP/CLP.

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