[m-dev.] semantics with any insts

[Peter Schachte]

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.

-- 
Peter Schachte              Before you insult someone, you should walk a
schachte at cs.mu.OZ.AU        mile in their shoes. That way, when you insult
www.cs.mu.oz.au/~schachte/  them, you are a mile away, and you have their
Phone: +61 3 8344 1338      shoes. -- Frieda Norris 
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------