[m-dev.] Unique Modes and Transaction Logic

[Marcus Troyka]

I was reading through the section in the ref manual on unique modes and
I came to the conclusion that the proposed implementation isn’t really
sufficient. Incorporating side-effect semantics in a logically sound way
is by no means simple, but there are some basic ‘rules of thumb’ that
can be inferred from the literature on transaction logic and used to
reason about it.

Firstly, ‘unique input’ is a tautology since all predicates can take ui
as an input implicitly (which is how other predicates can be used in the
goals of first order preds). I can't think of a situation where you
would ever need to state ui explicitly.

The second thing, more important than io modes is the fact that pure
predicate logic lacks semantics for describing order of evaluation or
for formalizing the meaning and truth value of side-effects. Transaction
logic formalizes that with the introduction of a serial conjunction,
‘then’, which behaves similarly to a normal conjunction except that it
lacks commutativity and thus also binds more weakly than a normal
conjunction. So, for example:

A and B then C and D or E <=> ((A and B) then (C and D)) or E
and
A then B and C then D or E <=> (A then (B and C) then D) or E

Transaction logic can be summarized by a few simples rules regarding
side-effects and serial conjuntions:

-The truth value of a side-effect is its success or failure, so that
pure logical statements such as “A ^ B” can have a valid interperetation
even when A or B produce side-effects.

-Side-effects are considered valid contributions to a solution and are
not reversed when backtracking for multiple solutions, thus predicates
with an io::di mode should be valid in ‘multi’ as well as ‘det’ contexts.

-Serial conjunctions like regular conjunctions are considered atomic,
thus if a conjunction fails then all side-effects must be reversed. That
being the case, predicates with io::di modes cannot be valid in
‘semidet’ or ‘nondet’ contexts, unless they provably occur after
(serially follow) any term that can fail (thus avoiding the state
changes altogether when failure occurs). This also means that serial
conjunctions cannot be parallelized, although in cases like:
(A then B) and (C then D)
the regular (non-serial) conjunction can be parallelized as usual even
in the presence of side-effects.

Transaction logic uses typical ‘assert’ and ‘retract’ semantics which
are assumed to carry a ‘reversible destructive input’ mode, and
intuitively predicates with ‘rdi’ modes are considered pure in the same
way ‘promise_pure’ is used with 'impure' statements in mercury. In
practice implementing reversibility is inefficient, though, but as long
as the side-effect code is only called from contexts which never fail,
the compiler can optimize ‘rdi’ to ‘di’.

Assert and retract introduce an additional complication in that they can
change the determinacy of the predicates they manipulate, which
complicates termination checking.

I think the first approach to that would be to add a third side-effect
primitive, of the form:

mutate(pred X(Y)::in, pred X(Y’)::in, !IO) :-

which can promise that it won’t affect the determinacy of pred X. While
that covers many common cases, beyond that a form of liveness analysis
will be required in order to correctly infer determinacy.

Also of note is that assert, retract and mutate should only be able to
operate on facts, that is predicates whose arguments are all ground
terms with mode ::out and whose only allowable goal is ‘true’. An extra
type may be justified to ensure correctness, and personally I think
'fact' and 'rule' types would be nice to have simply for the sake of
readability.

Further Reading:
ftp://ftp.cs.toronto.edu/pub/bonner/papers/transaction.logic/iclp93.ps
ftp://ftp.db.utoronto.ca/cs/ftp/dist/db/pub/pub/bonner/papers/transaction.logic/jicslp96.pdf