- From: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>
- Date: Tue, 22 Jun 2021 17:50:45 +0200
- To: William Van Woensel <william.vanwoensel@gmail.com>, Jos De Roo <josderoo@gmail.com>, Dörthe Arndt <doerthe.arndt@ugent.be>
- Cc: Pierre-Antoine Champin <pierre-antoine@w3.org>, "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <b4d82ba9-8eda-c6f0-6d7c-1ee5203f3cb7@ercim.eu>
On 22/06/2021 14:59, William Van Woensel wrote:
>
> Hi Jos, everyone,
>
> If I understood correctly:
>
> (1) all blank nodes within cited formulas, aside from rule premises
> and conclusions, are skolemized, and (2) the purpose for this is to
> implement static scoping, which avoids their "leakage" as existential
> variables beyond the cited formula. Such leakage can be problematic
> when blank nodes are "pulled into" rules (i.e., blank node is unified
> with a rule variable); they'd be considered as rule variables and thus
> lose their role as local identifiers, which is how they are often used
> in practice. Another reason is that it would allow inferring an
> existence claim in the top scope that was previously only in a nested
> scope (personally I don't really think that's an issue, and more like
> "caveat emptor" - it's up to the rule author to attach importance to a
> nested formula).
>
> Is this the case?
>
(1) is not absolutely correct, although it "works" for simple cases
(complex cases being: if you have rules inside rules...)
(2) As I pointed out at the end of our last call, the question of static
vs. dynamic scoping is orthogonal to the question of where we put the
implicit quantifiers. Let's rephrase by saying that "the purpose is to
place implicit quantifiers in a way that hopefully makes it easier to
cleanly implement dynamic scoping".
I agree with the rest of your description.
> I do think this kind of static scoping will match many practical use
> cases (as opposed to "dynamic" scoping, which I now believe is only
> really useful for one particular use case.)
>
> In that interpretation, I think the following should work:
>
> { {
> :will :hasName "will"
>
> } log:includes {
> _:x :hasName "will"
>
> } } => {
> :test1 a :SUCCESS
> } .
>
Agreed -- although I must admit that at first, I was tempted to say that
it should not succeed. :-/
>
> (it works in cwm but not eye, as the latter skolemizes the blank node,
> even when directly embedded in the rule premise)
>
> And the following should not, I suppose:
>
> { :will :hasName "will" } :label "formula1" .
> { _:x :hasName "will" } :label "formula2" .
>
> { ?f1 :label "formula1" .
> ?f2 :label "formula2" .
> ?f1 log:includes ?f2 } => { :test1 a :SUCCESS } .
>
Agreed again.
>
> (again, works in cwm but not eye)
>
Note that, in the two examples above, CWM should not be expected to give
the "correct" result as CWM puts the quantifiers in a different place
than what the proposal suggests. But with explicit quantifiers, CWM does
indeed succeed on the 1st one and fail on the 2nd one, as it should.
http://ppr.cs.dal.ca:3002/n3/editor/s/2agYgMr8
http://ppr.cs.dal.ca:3002/n3/editor/s/vXoJ1RLb
>
> William
>
>
> On 2021-06-21 8:25 p.m., Jos De Roo wrote:
>> You are right Doerthe and sorry for my failing recollection :-(
>>
>> Anyhow, as per my action of today's meeting I looked into the
>> consequences
>> of static (lexical) scoping of bnodes and changed eye accordingly
>> at https://github.com/josd/eye/releases/tag/v21.0621.2307
>> <https://github.com/josd/eye/releases/tag/v21.0621.2307>:
>> 1/
>> https://github.com/josd/eye/blob/master/reasoning/bnodes/example7.n3
>> <https://github.com/josd/eye/blob/master/reasoning/bnodes/example7.n3>
>> now
>> produces
>> https://github.com/josd/eye/blob/master/reasoning/bnodes/example7-pass-all.n3
>> <https://github.com/josd/eye/blob/master/reasoning/bnodes/example7-pass-all.n3>
>> and so ':d :e :f' is no longer produced.
>> 2/ all the other tests at
>> https://github.com/josd/eye/tree/master/reasoning
>> <https://github.com/josd/eye/tree/master/reasoning>
>> are still working fine as before.
>>
>> Jos
>>
>> -- https://josd.github.io/ <http://josd.github.io/>
>>
>>
>> On Mon, Jun 21, 2021 at 5:52 PM Dörthe Arndt <doerthe.arndt@ugent.be
>> <mailto:doerthe.arndt@ugent.be>> wrote:
>>
>> Hi Pierre Antoine,
>>
>> I am still reading the comments and thinking about my own opinion
>> here, but I can say that your proposal has been implemented some
>> time ago in EYE (I even have an implementation of my grammar for
>> this case and I formalized it that way). So, if you want to
>> „play“ with your idea, I think an EYE version from around 2017
>> should do what you it (but please double check with Jos).
>>
>> Hear you in a few minutes.
>> Dörthe
>>
>> > Am 16.06.2021 um 09:26 schrieb Pierre-Antoine Champin
>> <pierre-antoine@w3.org <mailto:pierre-antoine@w3.org>>:
>> >
>> > Hi all,
>> >
>> > here's a crazy idea. I am not even sure I like it myself, but I
>> wanted to ear others' opinion about it.
>> >
>> > During our last call, William made a point, with which I agree
>> (assuming I understood it correctly). To sum it up: people use
>> blank node in data more as "local" identifiers than as proper
>> existential variables. This pleads for quantifying blank nodes at
>> the top level.
>> >
>> > On the other hand, as we also pointed out during the call,
>> blank nodes as used in rule bodies (and rule heads, I believe)
>> need to be quantified locally.
>> >
>> > Hence my crazy idea: why not make the scope of blank node
>> determined by the log:implies (=>) predicate?
>> >
>> > More precisely:
>> >
>> > * a formula that is the subject or object of log:implies
>> defines a new scope for blank nodes
>> >
>> > * any other formula inherits the scope of its immediate parent
>> >
>> > * blank nodes in the top level scope are quantified *before*
>> universals (which is consistent with viewing them as "local
>> constants")
>> >
>> > Below is a long (apologies) list of examples.
>> >
>> > WDYT?
>> >
>> > pa
>> >
>> >
>> > Examples 1:
>> >
>> > :alice :belives { [] a :Unicorn }.
>> > [] a :Person.
>> >
>> > is equivalent to (using old-style explicit quantifiers)
>> >
>> > @forSome v:u, v:p.
>> > :alice :belives { v:u a :Unicorn }.
>> > v:p a :Person.
>> >
>> > ----
>> >
>> > Example 2:
>> >
>> > { [] a :Unicorn } => { :world a :MagicalPlace }.
>> >
>> > is equivalent to (using old-style explicit quantifiers)
>> >
>> > { @forSome v:u. v:u a :Unicorn } => { :world a :MagicalPlace }.
>> >
>> > (i.e. no change with today's interpretation)
>> >
>> > ----
>> >
>> > Example 3:
>> >
>> > { ?x a :Person } => { ?x :mother [] }.
>> >
>> > is equivalent to (using old-style explicit quantifiers)
>> >
>> > { ?x a :Person } => { @forSome v:m. ?x :mother v:m }.
>> >
>> > (i.e. no change with today's interpretation)
>> >
>> > ----
>> >
>> > Example 4:
>> >
>> > :alice :belives { [] a :Unicorn }.
>> > { ?x :believes { [] a :Unicorn } } => { ?x a :GulliblePerson }.
>> >
>> > is equivalent to (using old-style explicit quantifiers)
>> >
>> > @forSome v:u1.
>> > :alice :believes { v:u1 a :Unicorn }.
>> > { @forSome v:u2. ?x :believs { v:u2 a :Unicorn } } => { ?x
>> a :GulliblePerson }.
>> >
>> > which, unless I am mistaken, is also equivalent to
>> >
>> > @forSome v:u1.
>> > :alice :believes { v:u1 a :Unicorn }.
>> > { ?x :believs { ?u2 a :Unicorn } } => { ?x a :GulliblePerson }.
>> >
>> > I would expect this to produce.
>> >
>> > :alice a :GulliblePerson.
>> >
>> > ----
>> >
>> > Example 5:
>> >
>> > :alice :belives { [] a :Unicorn }.
>> > { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.
>> >
>> > is equivalent to (using old-style explicit quantifiers)
>> >
>> > @forSome v:u1.
>> > :alice :believes { v:u1 a :Unicorn }.
>> > { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.
>> >
>> > I would have no problem with this producing
>> >
>> > :alice :wishesToRide v:u1. # where v:u1 is still
>> quantified by the top @forSome
>> >
>> >
>> > <OpenPGP_0x9D1EDAEEEF98D438.asc>
>>
Received on Tuesday, 22 June 2021 15:52:17 UTC