Hi Mark,
Declaration Formula
----------- -------
class Eq a => Ord a forall a. Ord a => Eq a
instance Eq a => Eq [a] forall a. Eq a => Eq [a]
class C a b | a -> b forall a, b. C a b /\ C a c => b = c
This correspondence between declarations and formulas seems to be
very similar to what you did in the paper using CHRs. I haven't
read the paper carefully enough to know what extra mileage and/or
problems you get by using CHRs. To me, predicate logic seems more
natural, but I don't think that matters here---I just wanted to
acknowledge that essentially the same idea is in your paper.
i wondered about that "extra mileage" question when i first
encountered chrs and the fd-to-chr translations - here's my
take on it:
while chr started out with a predicate logic semantics, it helps
to think of them as representing a subset of linear logic instead
(which is where recent chr semantics are headed). other
relevant aspects are: committed choice language (no reliance
on backtracking), no implicit unification (left-hand sides of
rules are matched, unification has to be called explicitly in
right-hand sides, *after* committing to a rule).
what is helpful about using chr, then, is that they are closer
to implementations of functional dependencies, making it
easier to expose/discuss some general issues relevant to
implementations but not to abstract semantics (such as
incomplete and changing knowledge due to separate
compilation, or some implementations risking to lose
information), without having to wade through all other
implementation-level details.
in other words, chr expose a few more details, so more things
can go wrong; which is useful, because one can discuss how
to avoid these wrongs, providing more concrete guidelines
for implementations. they also avoid exposing details not
(currently) relevant to the application, as a mapping to prolog
would.
I don't dispute your claim that fullness is necessary to establish
confluence with CHRs. But that is a consequence of the formal
proof/rewrite system that you're using, and not of the underlying
semantics.
i tried to argue that case (the confluence issues are due to the
translation, not inherent in functional dependencies) last year,
even suggested an alternate translation of fd to chr. something
like this (the 'TC a b' should be 'TC a1..an', i think, and the
notation is meant to correspond to figure 2 in the jfp paper):
http://www.haskell.org//pipermail/haskell-prime/2006-March/000893.html
simplifying slightly, the alternate translation uses an embedding
of classical into linear logic, so knowledge about fds never
decreases as long as it remains consistent, whereas the jfp
paper translation works directly in a linear logic (<==> is like
linear implication -o, consuming its pre-conditions), so applying
inference steps in the "wrong" order can lose knowledge
about fds, leading to loss of confluence (unless additional
restrictions are introduced).
if i recall correctly, the paper also relied on confluence as
one possible means to ensure termination, meaning that
results about termination or results relying on termination
were to some extent tied up with the extra conditions used
to ensure confluence. i believe that fixing the translation to
chr would get rid of the confluence issues discussed in the
paper alltogether, so it could have focussed on the
remaining issues, like termination, without distraction.
frustratingly, while the paper was still a draft at the time,
the discussion came too late to have an impact on the
version published in jfp.
hope this helps,
claus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
