Implicit Quantification in N3

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

Implicit Quantification in N3

Dörthe Arndt
Hello,

I am currently trying to write down the basic formal semantics of N3 and
I had some problems with implicit quantification. Maybe you could help
me here?

I am not 100% sure how the scope of the universal quantifiers is. If I
have for example the formula:


     {{?x :p :o}=> {?x :pp :o}}=> {{?x :g :l}=>{?x :k :o}}.

Are the four ?x the same? Does it mean

     1. ∀x: ((p(x,o) → pp(x,o))→(g(x,l)→k(x,o)))

or

     2. ((∀x_1 p(x_1, o) → pp(x_1, o))→(∀x_2 g(x_2, l)→k(x_2, o)))


I checked in the N3 team submission
(http://www.w3.org/TeamSubmission/N3/#Quantifica) which states:

"Apart from the set of statements, a formula also has a set of URIs of
symbols which are universally quantified, and a set of URIs of symbols
which are existentially quanitified. Variables are then in general
symbols which have been quantified. There is a also a shorthand syntax
?x which is the same as :x except that it implies that x is universally
quantified not in the formula but in its parent formula"

This and the behaviour of the cwm reasoner
(http://www.w3.org/2000/10/swap/doc/cwm.html) in that case, suggest that
it is 2. But in the EYE reasoner (http://eulersharp.sourceforge.net/)
the first option seems to be implemented (and this first interpretation
would also be easier to formalise).

What about nested formulas? Is the quantification on top level inherited
or is there a new quantifier for every level? For EYE it is inherited,
but I tested two examples in cwm:

     1. {?y :p :o}=> {:s :p {?y :pp :o}}.

     2. {:s :p :o}=> {?x :p {?x :pp :o}}.

According to its parsing, the ?y in the first formula are the same, the
two ?x of the second formula aren't. cwm's interpretation:

     1.  ∀y: (p(y,o) → p(s,pp(y,o))

     2. p(s,o) → (∀x_1: p(x_1,(∀x_2: pp(x_2,o))

So, how is it supposed to be? Maybe I am misunderstanding it, but
shouldn't the parsing for the two formulas behave similarly?
Why is there a difference?

Thank you in advance for your help!

Kind regards,
Dörthe Arndt

--
Dörthe Arndt
Researcher Semantic Web
Ghent University - iMinds - Multimedia Lab
Faculty of Engineering and Architecture
Department of Electronics and Information Systems
Gaston Crommenlaan 8 bus 201, B-9050 Ledeberg-Ghent, Belgium

t: +32 9 331 49 59
e: [hidden email]
URL:  http://multimedialab.elis.ugent.be



Reply | Threaded
Open this post in threaded view
|

Re: Implicit Quantification in N3

Tim Berners-Lee

On 2015-01 -16, at 11:05, Dörthe Arndt <[hidden email]> wrote:

> Hello,
>
> I am currently trying to write down the basic formal semantics of N3 and I had some problems with implicit quantification. Maybe you could help me here?
>
> I am not 100% sure how the scope of the universal quantifiers is. If I have for example the formula:

They are universally quantified in the graph one outside the one they are mentioned in.  This is to
get simple rules to work like sparql.
 
>
>    {{?x :p :o}=> {?x :pp :o}}=> {{?x :g :l}=>{?x :k :o}}.
>
> Are the four ?x the same?

No, the first two are the same and the second two are.

If in doubt use @forAll


> Does it mean
>
>    1. ∀x: ((p(x,o) → pp(x,o))→(g(x,l)→k(x,o)))
>
> or
>
>    2. ((∀x_1 p(x_1, o) → pp(x_1, o))→(∀x_2 g(x_2, l)→k(x_2, o)))

The latter

>
>
> I checked in the N3 team submission (http://www.w3.org/TeamSubmission/N3/#Quantifica) which states:
>
> "Apart from the set of statements, a formula also has a set of URIs of symbols which are universally quantified, and a set of URIs of symbols which are existentially quanitified. Variables are then in general symbols which have been quantified. There is a also a shorthand syntax ?x which is the same as :x except that it implies that x is universally quantified not in the formula but in its parent formula"


The important bit here is 'not in the formula but in its parent formula'.



>
> This and the behaviour of the cwm reasoner (http://www.w3.org/2000/10/swap/doc/cwm.html) in that case, suggest that it is 2. But in the EYE reasoner (http://eulersharp.sourceforge.net/) the first option seems to be implemented (and this first interpretation would also be easier to formalise).
>

I wasn't aware that EYE was different.

The reason for having the rule that the quantification is in the parent formula is that

1) that makes it work as you would expect with simple rules


        { ?x :p ?y  } => { ?y :p ?x }.


2) If you can and paste a rule into something else, it doesn't change it meaning

@forAll :p.

        { :p a  :SymmetricProperty } =>  {{ ?x :p ?y  } => { ?y :p ?x }}.

works.  But note you cannot use ?p -- you have to explicitly quantify p.

I hope this helps.


> What about nested formulas? Is the quantification on top level inherited or is there a new quantifier for every level? For EYE it is inherited, but I tested two examples in cwm:
>
>    1. {?y :p :o}=> {:s :p {?y :pp :o}}.
>
>    2. {:s :p :o}=> {?x :p {?x :pp :o}}.
>
> According to its parsing, the ?y in the first formula are the same, the two ?x of the second formula aren't.



> cwm's interpretation:
>
>    1.  ∀y: (p(y,o) → p(s,pp(y,o))
>
>    2. p(s,o) → (∀x_1: p(x_1,(∀x_2: pp(x_2,o))
>
> So, how is it supposed to be? Maybe I am misunderstanding it, but shouldn't the parsing for the two formulas behave similarly?
> Why is there a difference?
>
> Thank you in advance for your help!
>
> Kind regards,
> Dörthe Arndt
>
> --
> Dörthe Arndt
> Researcher Semantic Web
> Ghent University - iMinds - Multimedia Lab
> Faculty of Engineering and Architecture
> Department of Electronics and Information Systems
> Gaston Crommenlaan 8 bus 201, B-9050 Ledeberg-Ghent, Belgium
>
> t: +32 9 331 49 59
> e: [hidden email]
> URL:  http://multimedialab.elis.ugent.be
>
>
>
>


signature.asc (506 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Implicit Quantification in N3

naudts guido
I'm not busy with these things anymore, butI would agree with Tim.
Greetings, Guido Naudts
 
Naudts - Van Noten
Secretarisdreef 5
2288 Bouwel
Belgium


On Monday, January 19, 2015 4:10 PM, Tim Berners-Lee <[hidden email]> wrote:



On 2015-01 -16, at 11:05, Dörthe Arndt <[hidden email]> wrote:

> Hello,
>
> I am currently trying to write down the basic formal semantics of N3 and I had some problems with implicit quantification. Maybe you could help me here?
>
> I am not 100% sure how the scope of the universal quantifiers is. If I have for example the formula:

They are universally quantified in the graph one outside the one they are mentioned in.  This is to
get simple rules to work like sparql.

>
>    {{?x :p :o}=> {?x :pp :o}}=> {{?x :g :l}=>{?x :k :o}}.
>
> Are the four ?x the same?

No, the first two are the same and the second two are.

If in doubt use @forAll


> Does it mean
>
>    1. ∀x: ((p(x,o) → pp(x,o))→(g(x,l)→k(x,o)))
>
> or
>
>    2. ((∀x_1 p(x_1, o) → pp(x_1, o))→(∀x_2 g(x_2, l)→k(x_2, o)))

The latter

>
>
> I checked in the N3 team submission (http://www.w3.org/TeamSubmission/N3/#Quantifica) which states:
>
> "Apart from the set of statements, a formula also has a set of URIs of symbols which are universally quantified, and a set of URIs of symbols which are existentially quanitified. Variables are then in general symbols which have been quantified. There is a also a shorthand syntax ?x which is the same as :x except that it implies that x is universally quantified not in the formula but in its parent formula"


The important bit here is 'not in the formula but in its parent formula'.



>
> This and the behaviour of the cwm reasoner (http://www.w3.org/2000/10/swap/doc/cwm.html) in that case, suggest that it is 2. But in the EYE reasoner (http://eulersharp.sourceforge.net/) the first option seems to be implemented (and this first interpretation would also be easier to formalise).
>

I wasn't aware that EYE was different.

The reason for having the rule that the quantification is in the parent formula is that

1) that makes it work as you would expect with simple rules


    { ?x :p ?y  } => { ?y :p ?x }.


2) If you can and paste a rule into something else, it doesn't change it meaning

@forAll :p.

    { :p a  :SymmetricProperty } =>  {{ ?x :p ?y  } => { ?y :p ?x }}.

works.  But note you cannot use ?p -- you have to explicitly quantify p.

I hope this helps.



> What about nested formulas? Is the quantification on top level inherited or is there a new quantifier for every level? For EYE it is inherited, but I tested two examples in cwm:
>
>    1. {?y :p :o}=> {:s :p {?y :pp :o}}.
>
>    2. {:s :p :o}=> {?x :p {?x :pp :o}}.
>
> According to its parsing, the ?y in the first formula are the same, the two ?x of the second formula aren't.



> cwm's interpretation:
>
>    1.  ∀y: (p(y,o) → p(s,pp(y,o))
>
>    2. p(s,o) → (∀x_1: p(x_1,(∀x_2: pp(x_2,o))
>
> So, how is it supposed to be? Maybe I am misunderstanding it, but shouldn't the parsing for the two formulas behave similarly?
> Why is there a difference?
>
> Thank you in advance for your help!
>
> Kind regards,
> Dörthe Arndt
>
> --
> Dörthe Arndt
> Researcher Semantic Web
> Ghent University - iMinds - Multimedia Lab
> Faculty of Engineering and Architecture
> Department of Electronics and Information Systems
> Gaston Crommenlaan 8 bus 201, B-9050 Ledeberg-Ghent, Belgium
>
> t: +32 9 331 49 59
> e: [hidden email]
> URL:  http://multimedialab.elis.ugent.be
>
>
>
>


Reply | Threaded
Open this post in threaded view
|

Re: Implicit Quantification in N3

jos.deroo
In reply to this post by Tim Berners-Lee
Hi Tim, just a quick clarification:

> I wasn't aware that EYE was different.

At the occasion of the first team submission d.d. 2008-01-14
http://www.w3.org/TeamSubmission/2008/SUBM-n3-20080114/
I made the following comments 5 days later
http://lists.w3.org/Archives/Public/public-cwm-talk/2008JanMar/0000.html
esp.

[[
The main differences that we have in our implementation are
1/ the scope of quickvars like ?A is the statement level
...
]]

Statements are clauses i.e. facts (triples) and rules.

I never wanted to change that in our implementation,
so we have an issue:


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

{{?s :p :o} => {?s :pp :o}} => {:i a :Black}.
{<>!log:semantics log:notIncludes {{?s :p :o} => {?s :pp :o}}} => {:i a :White}.

{:p :p :o} => {:p :pp :o}.


$ eye --nope black_and_white.n3 --pass 2> /dev/null
#Processed by Id: euler.yap 7698 2015-01-13 19:40:14Z josd
#eye --nope black_and_white.n3 --pass

PREFIX log: <http://www.w3.org/2000/10/swap/log#>
PREFIX : <http://example.org/test#>

:i a :Black.


$ cwm black_and_white.n3 --think --data 2> /dev/null
#Processed by Id: cwm.py,v 1.198 2012-01-30 09:30:20 timbl Exp
        #    using base file:///home/jdroo/temp/quickvars/black_and_white.n3
             @prefix : <http://example.org/test#> .
   
    :i     a :White .


This inconsistency was resolved by Dörthe by simply adding a dummy rule

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

# "dummy rule" found by Dörthe
{?s ?s ?s} => {?s ?s ?s}.

{{?s :p :o} => {?s :pp :o}} => {:i a :Black}.
{<>!log:semantics log:notIncludes {{?s :p :o} => {?s :pp :o}}} => {:i a :White}.

{:p :p :o} => {:p :pp :o}.


and then cwm gives


$ cwm black_and_white_try.n3 --think --data 2> /dev/null
#Processed by Id: cwm.py,v 1.198 2012-01-30 09:30:20 timbl Exp
        #    using base file:///home/jdroo/temp/quickvars/black_and_white_try.n3
             @prefix : <http://example.org/test#> .
   
    :i     a :Black .



Kind regards,
Jos

Jos De Roo | Agfa HealthCare
Senior Researcher | HE/Advanced Clinical Applications Research
http://www.agfa.com/w3c/jdroo
http://twitter.com/josderoo

Agfa HealthCare NV, Moutstraat 100, B-9000 Gent, Belgium
http://www.agfa.com/healthcare

Reply | Threaded
Open this post in threaded view
|

Re: Implicit Quantification in N3

Dörthe Arndt
In reply to this post by Tim Berners-Lee
Hello,
first of all: Thank you for your answers!
I still have two remaks/questions:



I am currently trying to write down the basic formal semantics of N3 and I had some problems with implicit quantification. Maybe you could help me here?

I am not 100% sure how the scope of the universal quantifiers is. If I have for example the formula:
They are universally quantified in the graph one outside the one they are mentioned in.  This is to 
get simple rules to work like sparql.
I am a little bit confused here, I thought that sparql handles that case different.  If I have the query:

select distinct ?p ?t where {
	{{{?p a <http://dbpedia.org/ontology/Place>.}}}
	{{{?t <http://xmlns.com/foaf/0.1/primaryTopic> ?p. }}}
} 



Doesn't it mean the same as:

select distinct ?p ?t where {
	{?p a <http://dbpedia.org/ontology/Place>.}
	{?t <http://xmlns.com/foaf/0.1/primaryTopic> ?p. }
} 



So here the quantification seems to be on top level and not just on the "mother-graph".


 
   {{?x :p :o}=> {?x :pp :o}}=> {{?x :g :l}=>{?x :k :o}}.

Are the four ?x the same?
No, the first two are the same and the second two are.

If in doubt use @forAll 


Does it mean

   1. ∀x: ((p(x,o) → pp(x,o))→(g(x,l)→k(x,o)))

or

   2. ((∀x_1 p(x_1, o) → pp(x_1, o))→(∀x_2 g(x_2, l)→k(x_2, o)))
The latter


I checked in the N3 team submission (http://www.w3.org/TeamSubmission/N3/#Quantifica) which states:

"Apart from the set of statements, a formula also has a set of URIs of symbols which are universally quantified, and a set of URIs of symbols which are existentially quanitified. Variables are then in general symbols which have been quantified. There is a also a shorthand syntax ?x which is the same as :x except that it implies that x is universally quantified not in the formula but in its parent formula"

The important bit here is 'not in the formula but in its parent formula'.



This and the behaviour of the cwm reasoner (http://www.w3.org/2000/10/swap/doc/cwm.html) in that case, suggest that it is 2. But in the EYE reasoner (http://eulersharp.sourceforge.net/) the first option seems to be implemented (and this first interpretation would also be easier to formalise).

I wasn't aware that EYE was different.

The reason for having the rule that the quantification is in the parent formula is that 

1) that makes it work as you would expect with simple rules


	{ ?x :p ?y  } => { ?y :p ?x }.


2) If you can and paste a rule into something else, it doesn't change it meaning

@forAll :p.

	{ :p a  :SymmetricProperty } =>  {{ ?x :p ?y  } => { ?y :p ?x }}.

works.  But note you cannot use ?p -- you have to explicitly quantify p.

I hope this helps.


What about nested formulas? Is the quantification on top level inherited or is there a new quantifier for every level? For EYE it is inherited, but I tested two examples in cwm:

   1. {?y :p :o}=> {:s :p {?y :pp :o}}.

   2. {:s :p :o}=> {?x :p {?x :pp :o}}.

According to its parsing, the ?y in the first formula are the same, the two ?x of the second formula aren't.


cwm's interpretation:

   1.  ∀y: (p(y,o) → p(s,pp(y,o))

   2. p(s,o) → (∀x_1: p(x_1,(∀x_2: pp(x_2,o))

So, how is it supposed to be? Maybe I am misunderstanding it, but shouldn't the parsing for the two formulas behave similarly?
Why is there a difference?

Thank you in advance for your help!

Kind regards,
Dörthe Arndt

-- 
Dörthe Arndt
Researcher Semantic Web
Ghent University - iMinds - Multimedia Lab
Faculty of Engineering and Architecture
Department of Electronics and Information Systems
Gaston Crommenlaan 8 bus 201, B-9050 Ledeberg-Ghent, Belgium

t: +32 9 331 49 59
e: [hidden email]
URL:  http://multimedialab.elis.ugent.be





    


-- 
Dörthe Arndt
Researcher Semantic Web
Ghent University - iMinds - Multimedia Lab
Faculty of Engineering and Architecture
Department of Electronics and Information Systems
Gaston Crommenlaan 8 bus 201, B-9050 Ledeberg-Ghent, Belgium

t: +32 9 331 49 59
e: [hidden email]
URL:  http://multimedialab.elis.ugent.be
Reply | Threaded
Open this post in threaded view
|

Fwd: Re: Implicit Quantification in N3

Dörthe Arndt
Hello,
Sorry for sending an unfinished mail! Here the entire mail:

first of all: Thank you for your answers!
I still have two remarks/questions:


I am currently trying to write down the basic formal semantics of N3 and I had some problems with implicit quantification. Maybe you could help me here?

I am not 100% sure how the scope of the universal quantifiers is. If I have for example the formula:
They are universally quantified in the graph one outside the one they are mentioned in.  This is to 
get simple rules to work like sparql.
1. I am a little bit confused here, I thought that sparql handles that case different.  If I have the query:

select distinct ?p ?t where {
	{{{?p a <http://dbpedia.org/ontology/Place>.}}}
	{{{?t <http://xmlns.com/foaf/0.1/primaryTopic> ?p. }}}
} 



Doesn't it mean the same as:

select distinct ?p ?t where {
	{?p a <http://dbpedia.org/ontology/Place>.}
	{?t <http://xmlns.com/foaf/0.1/primaryTopic> ?p. }
} 



So here the scope of the quantification seems to be on top level and not just on the "mother-graph". This is different than in the n3-example I posted earlier. But maybe I just misunderstood you?


 
   {{?x :p :o}=> {?x :pp :o}}=> {{?x :g :l}=>{?x :k :o}}.

Are the four ?x the same?
No, the first two are the same and the second two are.

If in doubt use @forAll 

2. I started with with a formalisation which uses @forAll but I got problems with formulas such as:

	{ @forAll :x. :x :p :o.} => {:x :pp :o}.

Does the scope of the @forAll end with the bracket "}"?


Thank you in advance for your explanations and opinions!

Greetings,
Dörthe Arndt


-- 
Dörthe Arndt
Researcher Semantic Web
Ghent University - iMinds - Multimedia Lab
Faculty of Engineering and Architecture
Department of Electronics and Information Systems
Gaston Crommenlaan 8 bus 201, B-9050 Ledeberg-Ghent, Belgium

t: +32 9 331 49 59
e: [hidden email]
URL:  http://multimedialab.elis.ugent.be