Re: Discussion from today

Nice and I have done a small test at
http://ppr.cs.dal.ca:3002/n3/editor/s/HO51TdBf
and so far it works for nesting and triple permutation too.

Jos

-- https://josd.github.io


On Mon, Jan 31, 2022 at 5:03 PM Pierre-Antoine Champin <
pierre-antoine.champin@ercim.eu> wrote:

> I find interesting the proposal of modelling explicit quantification with
> "standard" triples.
>
> However, I find the log:scope construction weird, using two levels of
> graphs
>
>   { (log:universal ?x) log:scope { ?x :b :c }
>
> why not simply something like
>
>   [ log:universal ?x ; log:graph { ?x :b :c } ]
>
> ?
>
> Some experiment here (using blank nodes rather than quickvars for the
> "quantified" variables)
>
> http://ppr.cs.dal.ca:3002/n3/editor/s/yi3A4XKi
>
>   pa
> On 26/01/2022 15:54, Jos De Roo wrote:
>
> 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
>>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>
>>>
>>