CWM Bug: Rules That Strip Quantification

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

CWM Bug: Rules That Strip Quantification

Sean B. Palmer
This is quite a straightforward bug, but I have a bigger underlying question.

$ cat test01.n3
@prefix log: <http://www.w3.org/2000/10/swap/log#> .

{ @forAll :p . { :p :q :r } a :First }
   :test
{ @forAll :p . { :p :q :r } a :Second } .

@forAll :a, :b, :c, :d .

{ [ log:includes { :a :b :c }; :test :d ] }
   => { :a a :Result } .

{ :d :test [ log:includes { :a :b :c } ] }
   => { :a a :Result } .

# EOF

$ cwm test01.n3 --think
#Processed by Id: cwm.py,v 1.195 2007-08-23 16:28:29 syosi Exp

#  Notation3 generation by
#       notation3.py,v 1.198 2007-10-15 14:55:54 syosi Exp

     @prefix : <#> .
    @prefix log: <http://www.w3.org/2000/10/swap/log#> .

     @forAll :a,
                :b,
                :c,
                :d .
    {
        :p     :q :r .

        }     a :Result .
    {
        :p     :q :r .

        }     a :Result .
    {
         @forAll :p .
        {
            :p     :q :r .

            }     a :First .

        }     :test { @forAll :p .
        {
            :p     :q :r .

            }     a :Second .
        } .
    {

          [      :test :d;
                 log:includes {:a     :b :c .
                } ].

        }     log:implies {:a     a :Result .
        } .
    {
        :d     :test  [
                 log:includes {:a     :b :c .
                } ] .

        }     log:implies {:a     a :Result .
        } .

#ENDS

The bug is that when I query for a nested universal which isn't scoped
over the root formula, when it gets barfed out again suddenly it isn't
scoped at all: it becomes a URI rather than a universal.

I expected this because I've been thinking about how CWM is designed,
and I know that it stores variables scopes as attributes of formulae.
This makes it possible for a variable to be scoped over multiple
formulae, as in the test input above, though of course the variable
itself doesn't have two scopes as far as CWM knows: CWM only knows
that the formulae that they're scoped over has been scoped to from
those variables.

What I'm trying to do is make the design of CWM replicable, not just
its underdefined behaviour. To understand, in other words, not just
how CWM actually works, and but how it's actually intended to work. It
seems that with quantification, if you do something fairly
impractical, CWM throws up its hands and says "look, I don't wanna
know about this". As it did, for example, in this recent bug
submission:

[[[
I'm not sure how cwm interprets when variables are declared
inconsistently like that. Weirness resulted.
]]] - http://lists.w3.org/Archives/Public/public-cwm-bugs/2007Oct/0002

Yosi actually called it *inconsistent* to do strange scoping as I'd
(accidentally) done in that test, but the fact that it's *possible* to
do it surely means that it should have some kind of well defined
outcome. At the moment, there are inputs that you can give CWM where
it gives essentially random results, only specified by behaviour
rather than by design.

This is true, in a sense, of CWM in general. It's only defined by its
tests, not a specification.

On the other hand, the quantification and implication in N3 and CWM
seem to be modelled very strongly after First Order Predicate Logic,
as the early N3 design documents state. If that's so then it should be
too difficult to formalise this sort of thing by just looking at some
KIF reasoners or whatever. I'm sure that DanC's tried to do this sort
of thing hundreds of times :-)

But does CWM need to be that complicated in the real world? It's a
Semantic Web application, not a logic application, so if what's being
implemented is just a subset of First Order Predicate Logic which is
useful on the Semantic Web, then why not define that subset and make
all other things impossible?

The kind of thing that I'm thinking about is that rather than
quantification over whatever scope one chooses, perhaps there are only
really two different kinds of variables in the day-to-day use of CWM:
variables that you want to match input in queries, and variables that
you don't want to match input, to be left alone, in queries. The thing
that scoping appears to add is a mechanism for saying when you
suddenly want a quoted variable to turn into a usable variable, for
example when you have rules-producing-rules and you want the rules
that have been produced to actually work—but you don't want them to be
active before they work.

Scoping makes CWM quite difficult to re-implement, and I'm not sure
that it's possible to model FOPL by having formulae store the
variables that they're quantified over. I think that you have to store
the scoping in the variable, but I'm not an expert. You can see what I
was trying to achieve by test01.n3; I was wondering whether it'd
properly preserve the scoping, and it failed to do so not just in
quantifying over the wrong scope, but in removing the quantification
entirely!

Thanks,

--
Sean B. Palmer, http://inamidst.com/sbp/
Reply | Threaded
Open this post in threaded view
|

Re: CWM Bug: Rules That Strip Quantification

Sean B. Palmer

On Nov 11, 2007 8:15 AM, Sean B. Palmer <[hidden email]> wrote:

> On the other hand, the quantification and implication in N3 and CWM
> seem to be modelled very strongly after First Order Predicate Logic,

I've since done some research, and the best two statements on this
situation I've found are as follows:

[[[
There's a trick to making RDF rules be Horn-expressive instead of
merely datalog-expressive with only a slight change in the rules
language.  We use this trick in cwm/n3, and I used it in some
unpublished pre-w3c work.  I've mentioned it before (in proposals I
wouldn't exactly support any more) [1] [2], but I still haven't come
up with any proper references.

The idea is this: if an RDF rule is a pair of RDF graphs (the
body/antecedent and the head/consequent), with certain nodes/arcs in
the graph marked as variables (just like in DQL), then we only have
datalog rules.  If, however, we also allow nodes/arcs in the
consequent to be marked as existential variables in the scope of the
consequent, we have Horn expressivity.
]]] - http://www.daml.org/listarchive/joint-committee/1237.html

(Old, though, being from 2002.)

[[[
We do not expect rule engines or other rule processing systems (such
as editors) to handle even a large set of the features standardized by
this Working Group. There are many viable rule languages and rule
engines which do not handle even all the Phase 1 features. (In
particular, it is common to implement only function-free Horn Logic
(Datalog), which is has a finite deductive closure.)
]]] - http://www.w3.org/2005/rules/wg/charter.html#conformance

Which suggests that there is a decidable level of expressivity,
datalog, and an undecidable level of expressivity, Horn Logic, and
that CWM kinda implements both in some way. I also found this:

[[[
TimBL: should we support --datalog in cwm?
<DanC> (seems like a reasonable idea, but I don't see any specific
benefit that motivates me to write the RFE)
]]] - http://www.policyawareweb.org/2005/pf-dev/09-28-paw-minutes

Which suggests that it's possible to add a mode to cwm to restrict it
to only those rules which are decidable. Cf. also what Yosi wrote
recently about lean graphs:

[[[
When writing cwm's rule engine, the decision was made to try to not
entail redundant triples. A set of triples is redundant if the graph
after those triples are added is rdf-entailed by the graph
beforehand. Because of this, the following will not loop forever

echo '{?x ?p ?y} => {[] ?p []} . :a :b :c . ' | cwm --think
]]] - http://lists.w3.org/Archives/Public/public-cwm-bugs/2007Oct/0015

Which seems like it's related, but I'm not sure how.

JHendler dropped by #swig and commented on the SWIG Scratchpad posting
of this bug, saying that there's some paper due out about how CWM
works:

[[[
hendler: There is a new paper coming soon on the semantics of N3 in a
more operational way -- I was looking for a pointer from Dig or arxiv
but couldn't find it
hendler: will try to get it posted at dig
]]] - http://swig.xmlhack.com/2007/11/11/2007-11-11.html#1194768958.252283

Which might be one of those papers that I've personally overheard
mention of in DIG circles. I'd certainly be very grateful if that
paper were to be posted on Breadcrumbs, as I think JHendler was
suggesting he'd try to make happen.

--
Sean B. Palmer, http://inamidst.com/sbp/

Reply | Threaded
Open this post in threaded view
|

Re: CWM Bug: Rules That Strip Quantification

Sean B. Palmer

On Nov 11, 2007 10:05 AM, Sean B. Palmer <[hidden email]> wrote:

> I've since done some research

And a couple more references today via JHendler and Chimezie:

http://arxiv.org/abs/0711.1533 - N3Logic paper
http://www.w3.org/DesignIssues/N3Logic - N3Logic Design Issue

Quite a bit to digest, especially Section 5.7 in the paper.

--
Sean B. Palmer, http://inamidst.com/sbp/