- From: Sean B. Palmer <sean@miscoranda.com>
- Date: Sun, 11 Nov 2007 08:15:15 +0000
- To: public-cwm-bugs@w3.org
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/
Received on Sunday, 11 November 2007 08:15:25 UTC