[EMAIL PROTECTED] (Carl R. Witty) writes:
> "Claus Reinke" <[EMAIL PROTECTED]> writes:
>
> > Fergus (and others): how about compiling a summary of the
> > relationships (a kind of dictionary of terminologies) ? In
> > particular, what is the state of the art in logic programming
> > wrt determinism and termination analysis? Can you
> > recommend any recent surveys, or can anyone offhand
> > propose "nicer" constraints to ensure termination and
> > determinism (of executions, not results), compared to
> > those currently used for type classes?
>
> My former thesis adviser, David McAllester, did some work on efficient
> (and hence terminating) execution of logic programs that may be
> relevant here. You might be interested in
> http://www.research.att.com/~dmac/kr92.ps
> (and several of his other papers).
>
> There are also simpler methods for determining termination. One
> simple constraint which proves termination is that every proper
> subterm of an "antecedent" must also be a proper subterm of the
> "conclusion". An instance declaration like
>
> (P (F [a]) (G [(a, b)]) (H a [b]), Q b a) => (R (H (F [a]) [(G [(a, b)])]) (H a
>[b]) c)
>
> would thus be acceptable.
>
> Of course, this does not prove determinism. I think that is probably
> the harder of the two problems.
I have been thinking about how to check determinism of a set of
inference rules (check whether every provable statement has at most
one proof). I have come up with a proof that checking determinism for
inference rules of the above form (where every proper subterm of an
antecedent is a proper subterm of the conclusion) is undecidable. Let
me know if you want the proof; it's somewhat long.
You can imagine checking determinism either where the type class
instance is defined, or where the type class is used. According to
the above result, if you insist on checking determinism at instance
definition time, you'll have to restrict the class of allowed
instances more than my suggestion does. However, if you delay
flagging ambiguity errors until the ambiguous case is actually used,
that can still be efficiently checked.
Carl Witty
