- 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