Re: Comments on N3 and its use for writing rules

----- Original Message -----
From: "Jonas Liljegren" <jonas@rit.se>
To: "Tim Berners-Lee" <timbl@w3.org>
Cc: "Dave Reynolds" <der@hplb.hpl.hp.com>; <www-rdf-logic@w3.org>; "Wraf
development" <rdf@uxn.nu>
Sent: Tuesday, March 13, 2001 9:19 AM
Subject: Comments on N3 and its use for writing rules


> I have now read these pages of yours:
>         http://www.w3.org/DesignIssues/Notation3.html
>         http://www.w3.org/DesignIssues/Anonymous.html
>         http://www.w3.org/2000/10/swap/Primer.html
>
> There is a lot on inconsistencys.  Both <#g> and '#g' and :g is used.
> But <#g> is not defiend in the BNF.  I guess you have replaced '' with
> <>.

Ooops. Excuse me. I changed '' to <> a long time ago but eth BNF is still
wrong
It should 9and now does) read:
    uri-ref2
        qname
        < URI-Reference >

> I also guess that the dot at the end inside {} is optional.

True.  In the production for statementlist the dot is used as a separtor.
It isn't introdued that way in the primer.  There are many ways yu can write
N3 which are not introduced in the primer, as the primer's goal is to get
people
unconfused and expressing themselves as fast as possible.

>
>
>
>
> EXPLOSION OF NESTED MODELS
>
> (I am using the word model[1], since I have put a diffrent meaning in
> the word context[7].)

OK

> I would like to comment on the last part of the Primer:
>
>     <> log:forAll :p, :q.
>     { :p ont:inverse :q } log:implies
>     {
>       {
>         { :x :p :y } log:implies { :y :q :x }
>       } a log:Truth; log:forAll :x, :y.
>     }.
>
> And Now blow it to pieces, using the format "Model Stating[2]
> Subject Predicate Object" (Triple, quad, whats next? penta something?)
>
>   C00  S01  C00   log:forAll   :p
>   C00  S02  C00   log:forAll   :q
>   C01  S03  :p    ont:inverse  :q
>   C02  S04  :x    :p           :y
>   C03  S05  :y    :q           :x
>   C04  S06  C02   log:implies  C03
>   C05  S07  C04   rdf:type     log:Truth
>   C05  S08  C04   log:forAll   :x
>   C05  S09  C04   log:forAll   :y
>   C00  S10  C01   log:implies  C05
>
>
> That log:Truth statement got me thinking.  Let's consider your first
> rule of models: "The statements are all independent, in that you can
> remove any of the statements and the rest are still true".

That only applies to models which are true.  It is a property of
"and" which is the operator connecting the statements.
It does not hold in a negated model or a model on the left hand
side of an implication, or a formula in general.

> What happens if we kill S07?  We would still have the statements S08
> and S09.  Can't we implicitly say that C4 is true for all :x and :y?

No, that is not the way I defined forAll, as for example I don't want to
imply truth in a condition on the left of log:implies.

> Ok. Maby not.
>
>
>
> Now, let us see this thing in action.  We start by Inserting some
> seeds in the system.  Here we declare our trust in the infered
> statements [3], here placed in L01:
>
>   C11  S11 C00    rdf:type     log:Truth
>   C11  S12 :child ont:inverse  :parent
>   C11  S13 :agnus :child       :bengt
>   C11  S14 L01    rdf:type     log:Truth
>
>
> And now press GO!
>
>   R01  L01->imports( C11 )
>   R02  L01->imports( C00 )
>   R03  L01->state( :p, rdf:type, log:variable )
>   R04  L01->state( :q, rdf:type, log:variable )
>   R05  L02 = L01->eval( C01 )
>   R06  L01->find( *, ont:inverse, * )
>   R07  L01->state( :p, =, :child )
>   R08  L01->state( :q, =, :parent )
>   R09  L01->imports( C05 )
>   R10  L01->state( :x, rdf:type, log:variable )
>   R11  L01->state( :y, rdf:type, log:variable )
>   R12  L03 = L01->eval( C04 )
>   R13  L04 = L01->eval( C02 )
>   R14  L01->find( *, :child, * )
>   R15  L01->state( :x, =, :agnus )
>   R16  L01->state( :y, =, :bengt )
>   R17  L03->imports( C03 )
>   R18  L03->state( :bengt, :parent, :agnus )
>   R19  L01->imports( L03 )
>
> Ok. That seems to work. :)
>
> This was just some pseudocode I invented as I wrote it. The  L01-L04 is
> models produced by the inference function.  R01-R19 are just row
> numbers.  The L01->f() syntax is for specifying in which model the
> function operates.  See the Wraf API [4].
>
> I was trying to find out for myself if we could keep the models
> separated as in your example with an inner and outer model.
>
>
> In Wraf, I will mostly use inverse inference.  I will start with the
> sought after property and determine its value.  We just have to turn
> the logic functions outside in.

yes. That will be interesting to see the same rules being used in
forward chaining and backward chaining.

> BINDING QUANTIFIERS
>
> I don't think it's necessary to bind quantifiers to a specific
> model.  All statings already are in a model.  Look at S01 and
> S02 above.  You don't have to say the same thing twice.  log:forAll is
> not a binary predicate.


On the contrary, you must specify the scope of a quantifier.

Compare (in lispy syntax):
    (exists (x)
        (forall (y)
            (loves x y)))
with:
    (forall (y)
        (exists (x)
            (loves x y)))

The type of quantification going on is the same in each case but the
scoping is different and the mean ing is quite different
(There is somebody who loves everybody, vs every person is loved by someone)

> I suggest we declare them as special types of variables:
>
>     log:Variable rdf:type rdfs:Class.
>     log:ForAll rdfs:subClassOf log:Variable.

If you use type, and you don't use a special property which links to the
context,
 then you are saying something about the thing, not the variable.  It
doesn't work.
You need to break out of the logic, adding something new. You can't overload
type with this.

>
>   UNIVERSAL
>
> I don't think it is meaningful to say in what model a resource is a
> variable and in what model it isn't.  The result would be the same
> if you said:
>
>     <> log:forAll :p, :q, :x, :y.
>     { :p ont:inverse :q } log:implies
>     {
>         { :x :p :y } log:implies { :y :q :x }
>     }.

Yes, it would.  My software would not (I think) do
the right thing with this - I haven't written code
to handle left over universals in the conclusion.
@@

> Or, treating them as variables:
>
>     my:revtype ont:inverse rdf:type.
>     log:ForAll my:revtype :p, :q, :x, :y.
>     { :p ont:inverse :q } log:implies
>     {
>         { :x :p :y } log:implies { :y :q :x }
>     }.
>
> Hehe.  And thats Yet Another Recursive Dependency (YARD). ;-)
>
>
>
>   EXISTENTIAL

le me say straight off thatthere is a bug with the tripples representation
I use for forSome.

> So, what about log:forSome ?  In the Notation3 page under #quoting,
> you give the example:
>
>   {
>     [x:firstname "Ora"] dc:wrote [dc:title "Moby Dick"]
>   } a n3:falsehood .
>
> And you give this translation (model, stating, p, s, o ):
>
>  #c1  #s1  n3:forSome         #c1    #g1
>  #c1  #s2  x:firstname        #g1    "Ora"
>  #c1  #s3  n3:forSome         #c1    #g2
>  #c1  #s4  dc:wrote           #g1    #g2
>  #c1  #s5  dc:title           #g2    "Moby Dick"
>  doc  #s6  n3:forSome         doc    #c1
>  doc  #s7  n3:subExpression   doc    #c1
>  doc  #s8  rdf:type           #c1    n3:falsehood
>
>
> Hum...  I don't agree with #s6.  The model #c1 says that there exist
> some #g1 and #g2 such that #g1 wrote #g2.  #s8 negates that.  #s6
> doesn't make sense. #c1 is an generated resource. But it's properties
> is fully defined. #c1 is not a variable.

Yes, that "forSome" statement was put there to tell the code that
c1 was a variable, existentially qualified, with scope doc.

> Futher, there is no need for #s7.

True, that has been removed from the code and that page now.
Thanks for pointing it out.

> We can write back the remaining statings in n3, using the method from
> above:
>
>   n3:ForSome my:revtype :g1, :g2.

[[[ yes .. I keep wanting revtype. You know you can say in N3

    n3:ForSome is rdf:type of :g1 , :g2.

The reverse syntax was introduced just for this.  I'm also toying
with introducing comma-separated lists in the subject or even predicate
fields:
    :g1, :g2  rdf:type n3:ForSome .
Of couse n3:ForSome is your invention I still maintain doesn't work
for reasons given above. End syntax diversional]]]

>   :c1 =
>   {
>     :g1 x:firstname "Ora".
>     :g1 dc:wrote :g2.
>     :g2 dc:title "Moby Dick".
>   } a n3:falsehood .

When you don't state something has been given  a name which is arbitrary
then you can never make it anonymous again.


>   BOTH UNIVERSAL AND EXISTENTIAL
>
> Notation3 page section #quantification gives this example:
>
>     {{:g :loves :h} log:forSome :g} log:forAll :h.
>
> My nonattached version is ambigous:
>
>     :g a log:ForSome.
>     :h a log:forAll.
>     :g :loves :h.
>
> :g and :h is variables.  Let me rewrite a bit:
>
>     :g a log:ForSome.
>     :h a log:forAll.
>     :h log:implies { :g :loves :h }.

That I don't understand - you have some new meaning for log:implies.
You can't do that - its my term.  I tink you mean a relationship between
h the context, which is probably my forAll relation.

> Now, that takes care of it.  And for the other direction:
>
>     :g a log:ForSome.
>     :h a log:forAll.
>     :g log:implies { :g :loves :h }.
>
> Now, a lone resource is here taken to mean "{ :g a rdfs:Resource}".

You mean [ :g a rdfs:Resource ] . ?
True for any :g.

> But we would usually say something more about the resource.  Probably
> this:
>
>     :g a log:ForSome.
>     :h a log:forAll.
>     {:h a ont:Person} log:implies { :g :loves :h }.
>
_________________________
I had to leave at this point
Tim

>
>
> THE MODEL FOR INFERED STATINGS
>
> The Notation3 page introduces the log:parsesTo predicate.  I don't
> like that name.
>
> The thing here is that we in some way declare our trust[5] in a) source
> data and b) a inference service[6].  When we ask the service to find some
> infered data for us, we tell it what sources we trust.  We resulting
> statings is placed in a separate model.
>
> This resulting model should have metadata saying that it is infered
> data, and the inference service and source data used.  The same source
> model can be used in many inference models and the same inference
> model can use many sources.
>
> Let the model with the infered statings declare its sources.  If we
> wan't we can state the trust in the resulting data.
>
>
>
>  [1] http://uxn.nu/wraf/RDF-Service/doc/html/model.html
>  [2] http://uxn.nu/wraf/RDF-Service/doc/html/stating.html
>  [3] http://uxn.nu/wraf/RDF-Service/doc/html/inference.html
>  [4] http://uxn.nu/wraf/RDF-Service/doc/html/api.html
>  [5] http://uxn.nu/wraf/RDF-Service/doc/html/trust.html
>  [6] http://uxn.nu/wraf/RDF-Service/doc/html/service.html
>  [7] http://uxn.nu/wraf/RDF-Service/doc/html/context.html
>
> --
> / Jonas Liljegren
>
> The Wraf project http://www.uxn.nu/wraf/
> Sponsored by http://www.rit.se/
>

Received on Friday, 16 March 2001 17:38:01 UTC