- From: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>
- Date: Wed, 23 Jun 2021 10:17:27 +0200
- To: Dörthe Arndt <doerthe.arndt@ugent.be>, William Van Woensel <william.vanwoensel@gmail.com>
- Cc: Jos De Roo <josderoo@gmail.com>, "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <88ab8fb1-78d7-6fe0-6967-3d84642cc785@ercim.eu>
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.
>
>
> 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.
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. :-/
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....
> 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 08:17:40 UTC