Re: Discussion from today

Dear Doerthe,

Blank nodes occurring in built-ins (such as log:implies) are in
our current implementation local to the built-in.

Kind regards,
Jos

-- https://josd.github.io


On Wed, Jan 26, 2022 at 3:20 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de>
wrote:

> Dear Jos,
>
>
>
> In our current implementation blank nodes are N3 document global
> so we already have "(global) existential quantification on top level"
> and it is indeed done with blank nodes.
>
>
> Do you also do that with blank notes occurring in rules? Or do we need a
> solution for these?
>
> Kind regards,
> Dörthe
>
>
>
> Kind regards,
> Jos
>
> -- https://josd.github.io
>
>
> On Wed, Jan 26, 2022 at 2:07 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de>
> wrote:
>
>> Dear Jos,
>>
>> The nesting and the opportunity to use that to impose an order on the
>> quantifiers was one of the motivations for the proposal. I am still
>> wondering whether it would be better to have a more special notion for
>> quantification (like @forAll) to make sure that people only  manipulate
>> quantified triples when they know what they are doing, but I am not sure
>> yet. For sure the notion has the advantage of an explicit scope.
>>
>> What is still missing here is a way to have (global) existential
>> quantification on top level. We could change the meaning of blank nodes or
>> use the explicit quantifier here? What would you propose?
>>
>> Kind regards,
>> Dörthe
>>
>> Am 26.01.2022 um 13:49 schrieb Jos De Roo <josderoo@gmail.com>:
>>
>> Dear Doerthe,
>>
>> To deal with both log:universal and log:existential we can simply use
>> nested log:scope like in the example
>> http://ppr.cs.dal.ca:3002/n3/editor/s/1Jisg9ES
>>
>> @prefix log: <http://www.w3.org/2000/10/swap/log#>.
>> @prefix : <http://example.org/etc#>.
>>
>> :bob :smurfs {
>>     (log:universal :a) log:scope {
>>         (log:existential :x :u) log:scope {
>>             :x a :Unicorn.
>>             :u :p :x.
>>         }.
>>         :a :p :o.
>>     }
>> }.
>>
>> {
>>     ?y :smurfs {
>>         (log:universal :b) log:scope {
>>             :b :p :o.
>>             (log:existential :v :y) log:scope {
>>                 :v :p :y.
>>                 :y a :Unicorn.
>>             }
>>         }
>>     }
>> } => {
>>     ?y a :NaivePerson.
>> }.
>>
>> Using the latest eye
>> <https://github.com/josd/eye/releases/tag/v22.0126.1149> it can derive
>>
>> :bob a :NaivePerson.
>>
>> Kind regards,
>> Jos
>>
>> -- https://josd.github.io
>>
>>
>> On Tue, Jan 25, 2022 at 4:07 PM Jos De Roo <josderoo@gmail.com> wrote:
>>
>>> Dear Doerthe,
>>>
>>> Your log:scope is an excellent proposal and I was able to extend unify/2
>>> in the latest eye https://github.com/josd/eye/releases/tag/v22.0125.1445
>>> so that http://ppr.cs.dal.ca:3002/n3/editor/s/SHY7RXbG should give
>>> :bob a :NaivePerson1 but not :bob a :NaivePerson1
>>> of course after that @William Van Woensel <William.Van.Woensel@dal.ca>
>>> resolves
>>> https://github.com/william-vw/n3-editor-js/issues/5
>>>
>>> Kind regards,
>>> Jos
>>>
>>> -- https://josd.github.io
>>>
>>>
>>> On Tue, Jan 25, 2022 at 1:29 PM Doerthe Arndt <
>>> doerthe.arndt@tu-dresden.de> wrote:
>>>
>>>> Dear Jos,
>>>>
>>>> That is very interesting and I like the compact notion. I am not sure
>>>> about the use of the universal, but that is a separate discussion.  I
>>>>  still have two bigger concerns:
>>>>
>>>> 1. We can only quantify over triples and not over formulas which is
>>>> what we would actually need.
>>>> 2. The quoted variable could still be seen as a constant, look for
>>>> example here: http://ppr.cs.dal.ca:3002/n3/editor/s/ioYMxfcC
>>>>
>>>> So we could do something like :bob :smurfs { (log:existential :x)
>>>> log:scope {:x a :Unicorn.} }.
>>>>
>>>> This looks far less elegant than your solution but we have the
>>>> advantage that the scope is clearly defined and that we can quantifiy over
>>>> formulas. Maybe you have an idea ho to improve that?
>>>>
>>>> Kind regards,
>>>> Dörthe
>>>>
>>>> Am 25.01.2022 um 12:20 schrieb Jos De Roo <josderoo@gmail.com>:
>>>>
>>>> Dear Doerthe,
>>>>
>>>> Forgot to point to a concrete example
>>>> http://ppr.cs.dal.ca:3002/n3/editor/s/IT3znjsL
>>>> Here the log: namespace is (mis)used instead of the e: namespace.
>>>> Both Cwm and Eye agree again.
>>>>
>>>> Kind regards,
>>>> Jos
>>>>
>>>> -- https://josd.github.io
>>>>
>>>>
>>>> On Tue, Jan 25, 2022 at 11:56 AM Jos De Roo <josderoo@gmail.com> wrote:
>>>>
>>>>> Dear Doerthe,
>>>>>
>>>>> Agreed and a while ago I did some experiments in which the variables
>>>>> in quoted graphs were replaced by either
>>>>> (e:existential ?X)
>>>>> or
>>>>> (e:universal ?X)
>>>>> and then using rules like you also suggested to transform that into
>>>>> regular data N3 data/rules/queries.
>>>>>
>>>>> It is also quite close to Pierre-Antoine's proposal of one variable
>>>>> type.
>>>>> The scope of those variables is the so-called statement level.
>>>>>
>>>>> It actually worked quite well.
>>>>>
>>>>> Kind regards,
>>>>> Jos
>>>>>
>>>>> -- https://josd.github.io
>>>>>
>>>>>
>>>>> On Tue, Jan 25, 2022 at 10:46 AM Doerthe Arndt <
>>>>> doerthe.arndt@tu-dresden.de> wrote:
>>>>>
>>>>>> Dear Jos,
>>>>>>
>>>>>> I was too fast in the previous mail. There is one example where cwm
>>>>>> and Eye differ: http://ppr.cs.dal.ca:3002/n3/editor/s/okGlsqyV
>>>>>>
>>>>>> But that does not change the message from the previous mail.
>>>>>>
>>>>>> Kind regards,
>>>>>> Dörthe
>>>>>>
>>>>>>
>>>>>> Am 25.01.2022 um 10:38 schrieb Arndt, Dörthe <
>>>>>> doerthe.arndt@tu-dresden.de>:
>>>>>>
>>>>>> Dear Jos,
>>>>>>
>>>>>> Thank you for sharing. To complete your example, I also added
>>>>>> universal quantification:
>>>>>> http://ppr.cs.dal.ca:3002/n3/editor/s/IWXT3bhG
>>>>>> The reasoners still both do the same.
>>>>>>
>>>>>> I think that from a logical point of view, some of these derivations
>>>>>> are problematic.  But I also better understand, why you would be against
>>>>>> fully introducing explicit quantification. That would require us to make a
>>>>>> whole theory how reasoning works for the cases mentioned and then to also
>>>>>> implement it  accordingly which most likely will never be done since there
>>>>>> are not that many use cases which really require that complexity.
>>>>>>
>>>>>> My proposal was thus more to have some kind of notation for example
>>>>>> for proofs with which we can only do further derivation if we express that
>>>>>> structure in the rules. Maybe there is a third option between skolem iris
>>>>>> and explicit quantification with only minimal support which I am not seeing
>>>>>> (yet)?
>>>>>>
>>>>>> Kind regards
>>>>>> Dörthe
>>>>>>
>>>>>>
>>>>>>
>>>>>> Am 25.01.2022 um 01:10 schrieb Jos De Roo <josderoo@gmail.com>:
>>>>>>
>>>>>> Dear Doerthe,
>>>>>>
>>>>>> I was curious how your 5 examples currently fare with cwm and eye
>>>>>> and they both give the same results! Yes, the same results!
>>>>>>
>>>>>> You can try it at http://ppr.cs.dal.ca:3002/n3/editor/s/tR5T9red
>>>>>>
>>>>>> So there is a state of the art with explicit quantification and I was
>>>>>> not expecting that cwm and eye were so close here.
>>>>>>
>>>>>> Jos
>>>>>>
>>>>>> -- https://josd.github.io
>>>>>>
>>>>>>
>>>>>> On Mon, Jan 24, 2022 at 11:21 PM Doerthe Arndt <
>>>>>> doerthe.arndt@tu-dresden.de> wrote:
>>>>>>
>>>>>>> Dear all,
>>>>>>>
>>>>>>> After our meeting today I thought about explicit quantification and
>>>>>>> can say that I actually like the idea to have it in N3 as some kind of
>>>>>>> annotation which has no meaning for the reasoning except that it is a kind
>>>>>>> of pattern. My vision here is that we would have a  variable namespace
>>>>>>> which can be combined with quantifiers. Whenever a cited graph contains a
>>>>>>> quantifier, we simply disallow unification with the triples in that graph
>>>>>>> unless we also have the quantifier. So, if we come back to my example:
>>>>>>>
>>>>>>> :bob :smurfs { @forSome :X. :X a :Unicorn. }.
>>>>>>>
>>>>>>> { ?y :smurfs { @forSome :X. :X a :Unicorn } } => { ?y a :NaivePerson
>>>>>>> }.
>>>>>>>
>>>>>>> Should result in :bob a :NaivePerson. but
>>>>>>>
>>>>>>> :bob :smurfs { @forSome :X. :X a :Unicorn. }.
>>>>>>>
>>>>>>> { ?y :smurfs { _:x a :Unicorn } } => { ?y a :NaivePerson }.
>>>>>>>
>>>>>>> should not.
>>>>>>>
>>>>>>> Of course, things could get more complicated here:
>>>>>>>
>>>>>>> :bob :smurfs { @forSome :X. :X a :Unicorn. }.
>>>>>>>
>>>>>>> { ?y :smurfs ?g. ?g log:includes {?x a :Unicorn} } => { ?y a
>>>>>>> :NaivePerson }.
>>>>>>>
>>>>>>> Should not fire, but what about
>>>>>>>
>>>>>>> :bob :smurfs { @forSome :X. :X a :Unicorn. :Unicorn a
>>>>>>> :MagicalCreature }.
>>>>>>>
>>>>>>> { ?y :smurfs ?g. ?g log:includes {?x a :MagicalCreature } } => { ?y
>>>>>>> a :NaivePerson }.
>>>>>>>
>>>>>>> So, here we would have to agree and either decide that the moment
>>>>>>> that there is a quantifier involved in the graph, we stay away and do not
>>>>>>> match anything, we could use the name-space to know when not to match or we
>>>>>>> make a more fine-grained theory about scopes (but here we can really get
>>>>>>> into the problems, Jos mentioned). An example:
>>>>>>>
>>>>>>> :bob :smurfs { @forSome :X. :X a :Unicorn. :X :says {:sokrates a
>>>>>>> :Person} }.
>>>>>>>
>>>>>>> { ?y :smurfs ?g. ?g log:includes {?x :says {:sokrates a :Person} } }
>>>>>>> => { ?y a :NaivePerson }.
>>>>>>>
>>>>>>> Here, we see that the namspace alone can’t be a reason to allow or
>>>>>>> disallow a unification. We would need some concept to express, when a
>>>>>>> triple is scoped, and this theory could indeed get complicated.
>>>>>>>
>>>>>>> (So,I see your concerns here, Jos.)
>>>>>>>
>>>>>>> So, why do I even propose that kind of pattern? The answer is that I
>>>>>>> like that we would have some way to express the patterns which go
>>>>>>> beyond our logic which is limited to implicit quantification without
>>>>>>> loosing the possibility to involve them to our theory. We could then
>>>>>>> explicitly define our reasoning calculus which only allows implicit
>>>>>>> quantification and provide rules to support more sophisticated theories. We
>>>>>>> cannot express that by only having constants because then there would be no
>>>>>>> way of blocking unification.
>>>>>>>
>>>>>>> My ideas are not really thought through yet (it cn perfectly be that
>>>>>>> I change my mind next week, also depending on your comments ;) ). But I
>>>>>>> wanted to elaborate why (for now), it seems to be an interesting idea to me.
>>>>>>>
>>>>>>> Kind regards
>>>>>>> Dörthe
>>>>>>>
>>>>>>
>>>>>>
>>>>>>
>>>>
>>
>