- From: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>
- Date: Tue, 1 Feb 2022 10:23:52 +0100
- To: "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <2e5d039c-d0c9-697e-6acf-089e261e6064@ercim.eu>
Hi all,
Following the discussion during our call yesterday, I was convinced that
the log:scope construction is indeed better than my bnode-based proposal...
Actually, this morning, I even have an idea to push this further. While
I am not at all sure this is the right way to go, I wanted to share it
with you.
PROPOSAL: treat quickvars as syntactic sugar for log:universal
quantified variables.
VARIANT1: any top-level triple containing some quickvars is wrapped into
a log:universal / log:scope construct
example 1
{ ?x a :Student } => { ?x a :Person }.
becomes
(log:universal var:x) log:scope {
{ var:x a :Student } => { var:x a :Person }
}.
example 2 (N3 patch example from the Solid spec)
|_:rename a solid:InsertDeletePatch;|
|solid:where { ?person ex:familyName "Garcia". };|
|solid:inserts { ?person ex:givenName "Alex". };|
|solid:deletes { ?person ex:givenName "Claudia". }. |
becomes
|(log:||universal var:person) log:scope { _:rename a solid:InsertDeletePatch;|
|solid:where { var:person ex:familyName "Garcia". };|
|solid:inserts { var:person ex:givenName "Alex". };|
|solid:deletes { var:person ex:givenName "Claudia". }. }. |
VARIANT2: any quickvar in a graph causes the whole graph to be wrapped
in a log:universal / log:scope construct
CONSEQUENCES AND LOOSE ENDS:
* finding rules in a N3 graph becomes slightly more complex: instead of
locating log:implies triples in the top-level graph, a reasoner now also
needs to dig into the objects of log:scope until it finds a log;implies
triple . Maybe should it only accept /some/ chains of quantifiers (e.g.
only universals)
* we would have to decide on a deterministic way to order the variables
to generate the log:scope "chain" (we don't want to rely on the order in
which triples are serialized)
* it seems that this would offer a clean(?) way to synthesize rules from
parts (including "building" the quantifier)
* if we do that for quickvars, wouldn't it make sense to do something
similar for blank nodes?
* although a part of me finds this elegant, another part fears that,
without "real" universals in the abstract syntax, the core semantics
will be impoverished, and that everything interesting will be defined as
"ad-hoc" behavior by specific built-ins (not sure this is clear... this
is really a gut feeling at this point).
best
||
On 31/01/2022 17:49, Doerthe Arndt wrote:
> Dear Pierre-Antoine,
>
> I dislike here that you introduce a new blank node and - as we all
> know - nested blank nodes in N3 can be problematic, so I would like to
> avoid them where possible.
>
> I also still don't understand the problem you had with the other
> proposal. The subject of the quantification triple is a list, there is
> only one graph involved. What am I missing here?
>
> Kind regards,
> Dörthe
>
>> Am Montag, 31. Januar 2022, 17:34:51 MEZ hat Jos De Roo
>> <josderoo@gmail.com> Folgendes geschrieben:
>>
>>
>> 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
>>>>> <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 Tuesday, 1 February 2022 09:23:59 UTC