- From: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>
- Date: Mon, 31 Jan 2022 17:03:30 +0100
- To: Jos De Roo <josderoo@gmail.com>, "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <82cc525a-5521-c5a0-3de9-40fe218ac713@ercim.eu>
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
>>> <mailto: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
>>>>>>
>>>>>
>>>>
>>>
>>
>
Attachments
- application/pgp-keys attachment: OpenPGP public key
Received on Monday, 31 January 2022 16:03:36 UTC