- From: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>
- Date: Wed, 23 Jun 2021 08:37:33 +0200
- To: William Van Woensel <william.vanwoensel@gmail.com>, Jos De Roo <josderoo@gmail.com>, Dörthe Arndt <doerthe.arndt@ugent.be>, David Booth <david@dbooth.org>
- Cc: "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <b737f5f3-18f7-ded5-653b-25c1c5b8ab88@ercim.eu>
Sorry, I sent this email too quickly.
On 22/06/2021 20:22, William Van Woensel wrote:
>
> 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?
>
Actually, I overinterpreted what you wrote in (1)... I agree that all
blank nodes outside of rules (i.e. quantified at the top-level) can
safely be skolemized.
>> (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? ..
>
Yes indeed, I meant *static* scoping... :-/
(apologies to David Booth for the confusion)
pa
>>>
>>> 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 06:38:10 UTC