[m-dev.] Partially instantiated data structures

[Zoltan Somogyi]

On Mon, 8 Oct 2018 08:40:48 -0400, Charlie McGee <c4cypher at gmail.com> wrote:
> My lack of academic background may be biting me here, but in a general (not
> mercury specific) sense, isn't a logic program with that has ungrounded
> variables in it's extensional database (left hand side :-) unsound?

Negating a goal that contains unbound variables is unsound if (and only if)
the execution of that goal binds any of those variables.

Executing non-negated goals containing variables is (or at least can be) sound,
though this soundness is wrt a logic that is more complicated than the logic
that applies to goals that contain no variables.

> I know
> I'm probably futzing my semantics here, but I know the MMC pitches a fit if
> it can't properly ground all the terms in a data constructor.

Some of the error messages that mmc generates for nonground data
are required by theory for the preservation of soundness, but some others
are caused only by limitations in the compiler. The main limitation is that
at present, it cannot keep track of the relationship between different
occurrences of the same variable. This means that if some goal binds X,
it does not know that all the *other* occurrences of X, in other goals
or even in the same goal, have also become bound. To avoid the problems
that this could cause, the compiler rejects such code, even though the
unsoundness is in the compiler, not (necessarily) in the code.
The post that triggered this thread was asking about the lifting
of this limitation.

Zoltan.