- From: William Van Woensel <william.vanwoensel@gmail.com>
- Date: Wed, 23 Jun 2021 11:20:27 -0300
- To: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>, Dörthe Arndt <doerthe.arndt@ugent.be>
- Cc: Jos De Roo <josderoo@gmail.com>, "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <90a9a03e-1ee3-588a-07cf-dfec404c1b5e@gmail.com>
Hi Pierre-Antoine, Doerthe, all
On 2021-06-23 5:17 a.m., Pierre-Antoine Champin wrote:
> On 23/06/2021 00:13, Dörthe Arndt wrote:
>> Dear all,
>>
>> As we identified them as different topics, I will treat dynamic
>> scoping and context dependent quantification as two different cases:
>>
>> 1. Dynamic scoping: After carefully reading William’s mail again, I
>> am still not sure whether I fully understand what you want here. Do
>> you want the following to be correct (copied from our meeting
>> minutes, not supported by EYE)?
>> _:y :b :c.
>> {?U_0 :b ?U_1} => {{?U_0 :u :v} => {?U_1 :b :c}}.
>> Produces
>> {?U_2 :u :v} => {:c :b :c}.
>>
>> If so, I dislike the whole idea because it seems to be far away from
>> first order logic and thereby from RDF. How would you write a proof
>> for the reasoning above? How would you translate it into first
>> order logic (this should be possible in this case since we do not use
>> cited formulas).
>
> big +1 here.
>
My original statement was that this is reminiscent of lexical vs.
dynamic scoping in programming languages - I wasn't worrying about the
downstream consequences, such as equivalence with FOL (perhaps another
shock here - I wasn't aware this was a priority) or existing proof
methods. While I still see the utility of the latter in certain
scenarios, the former makes more sense in most use cases (and is far
easier to implement). So this may have become a moot point.
>>
>> 2. As a second point, I thought about the context dependent
>> quantifiers and I think having these would break our built-ins. As an
>> example, take log:semantics:
>>
>> If we have a file containing a blank node like for example
>>
>> [] a :Unicorn.
>> „Unicorns exist."
>>
>> And we write a rule saying that we do not trust the information in
>> that file using log:semantics:
>>
>> {<example.n3> log:semantics ?x} => {we doubt ?x }.
>>
>> Using the traditional interpretation, we would conclude
>>
>> :we doubt {[ ] a :Unicorn.}.
>>
>> „We doubt that unicorns exist“
>>
>> This would be exactly what I would expect here. But the last
>> expression would, following the new proposal, mean: „There is some
>> instance x and we doubt that this instance is a unicorn.“ This is not
>> what log:semantics is expected to do.
Do you mean the consequences of placing all existential quantifiers on
the top level, as opposed to within the cited formula? (Just making sure
I understand here.) Anyhow, I see the problem ..
> I thought about log:semantics too, but I came to the conclusion that
> this problem arises /as soon/ as we get rid of explicit quantifiers,
> no matter what convention we use for implicit quantifiers.
>
> Change the content of example.n3 to:
>
> ?x a :Person.
>
> "Everything is a Person"
>
> Your rule above now produces
>
> :we :doubt { ?x a :Person }.
>
> "We doubt that /anything/ is a Person / For all X, we doubt
> that X is a Person"
>
> which is also problematic (even more, I would say, than with
> existentials, because here the produced conclusion is *stronger* than
> what one would expect). And that is already the case with the
> convention we have right now. :-/
>
Don't fully understand why this would be problematic - in my view, and
in this case, "problematic" involves not being in line with expectations
> One way out of this conundrum would be to consider that some formulae
> (such as the ones extracted by log:semantics) can not be expressed
> between curly brackets... Possibly, a special literal datatype could
> be used instead?
>
> Another way out, of course, would be to reintroduce explicit
> quantifiers....
My two cents: lack of explicit quantification has vastly simplified my
N3 system (well, for a programmer with limitations such as myself ..)
I seem to remember a suggestion by PA about using a special notation
(along the lines of "{|" "|}" ?) to indicate a "closed" cited formula
scope - but I can't find the email and I could be misremembering (as it
is clearly reminiscent of an rdf-star syntax ; I'll use "{*" "*}" to
avoid confusion).
Possibly, using such a notation (?), the existential "{* _:x a :Unicorn
*} :doubtedBy :us" could quantified within the cited formula, and hence
have the meaning that Doerthe expects, I think. One could also assume
this meaning for any cited formula pulled in by log:semantics.
But, then, how to represent the inference of the rule:
:ed :believes {* _:x a :Unicorn *} .
{ ?person :believes { ?x a :Unicorn } } => { ?person :gullibleAbout ?x } .
(which is also a problem when scoping the quantifier at the top level,
of course, but more easily solved by skolemization (?))
I suppose one could again use the skolemization "bullet" somehow, but, I
think it would lead to a much different meaning in this case
Anyhow, I hope I didn't cause anyone to go into shock again :-(
William
>> The built-in is meant to provide the content of a file which can then
>> be used for further reasoning. So, here we need some extra solution.
>> We could try to use a skolem iri in the output and simply create a
>> witness.
>>
>> :we doubt {:skolemiri_x a :Unicorn.}.
>>
>> This solution is not wrong, but we loose information here.
>>
>> You can see a modified example for the described behavior here (I []
>> a :Person. instead of [] a :Unicorn. because that triple was already
>> present in the examples we discussed): Link
>> <http://ppr.cs.dal.ca:3002/n3/editor/s/2kqzxbi2>
>>
>> I did not check yet, but I would expect similar problems for other
>> builtins.
>>
>> Kind regards,
>> Dörthe
>>
>>
>>
>>
>>> Am 22.06.2021 um 20:22 schrieb William Van Woensel
>>> <william.vanwoensel@gmail.com <mailto:william.vanwoensel@gmail.com>>:
>>>
>>>
>>> On 2021-06-22 12:50 p.m., Pierre-Antoine Champin wrote:
>>>> (1) is not absolutely correct, although it "works" for simple cases
>>>> (complex cases being: if you have rules inside rules...)
>>>
>>> Can you give an example of where this does not work?
>>>
>>>> (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".
>>>>
>>> Do you mean static scoping here? ..
>>>
>>>>>
>>>>> 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 Wednesday, 23 June 2021 14:20:58 UTC