- From: Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>
- Date: Tue, 1 Feb 2022 16:01:50 +0100
- To: Doerthe Arndt <doerthe.arndt@tu-dresden.de>
- Cc: "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <8b50ccaf-0123-df76-d327-4fccf77ebf07@ercim.eu>
Doerthe, I think we are generally on the same page here. The doubts you
raise about my proposal echo my own doubts ;)
On a specific point, though:
> I would like to keep the „normal“ quickvars and the new syntax for
quantification separated because that way we make it clear that we can
express everything but we cannot expect the reasoner to understand
everything
That's a good point. But on the other hand, what about quickvars used
outside of rules? As in:
:alice :likes ?x .
:bob :smurfs { ?x a :Unicorn }.
And even if we refuse to define any operational semantics for that, how
would it differ, from a user's perspective, from:
(log:universal v:x) log:scope { :alice :likes v:x } }.
(log:universal v:x) log:scope { :bob :smurfs { v:x a :Unicorn } }.
??
pa
On 01/02/2022 12:36, Doerthe Arndt wrote:
> Dear Pierre-Antoine,
>
> I am also still thinking about your proposal, so I only report my
> first thoughts (no strong opinion yet).
>
> I like your proposal from a logical point of view and would consider
> to do some translation in the semantics. But from a rather practical
> point of view, I would like to keep the „normal“ quickvars and the new
> syntax for quantification separated because that way we make it clear
> that we can express everything but we cannot expect the reasoner to
> understand everything. If we say that reasoners only reason over
> quick-vars and then provide the environment to define rules for
> „quantification-constructs“ which allow „stronger“ reasoning, we have
> a cleaner solution where the user always knows what (not) to expect.
> That is also the reason why I am against using quickvars as
> quantification variables: I think then we don’t have a clean
> separation anymore.
>
> But as this is a „writing-while-thinking“-mail: I am not sure whether
> the pure syntactical construct is enough and whether it would not be
> easier to clearly define with what reasoners can deal and with what
> not. I would clearly want to stay away from any equivalences of
> quantification patterns within cited graphs at least if there is no
> built-in involved.
>
> I would be interested in some way of stating existential
> quantification on top level and without distinctions between
> occurrences in rules and cited graph. This could be done easily with
> the new notation.
>
> But if we support reasoning which takes the semantics of the explicit
> quantifier into account, we have to be explicit, which derivation
> steps are supported or could be supported. That should not look random
> to the user.
>
> Kind regards,
> Dörthe
>
>
>>
>>
>>
>>
>> ----- Weitergeleitete Nachricht -----
>> *Von:* Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu>
>> *An:* public-n3-dev@w3.org <public-n3-dev@w3.org>
>> *Gesendet:* Dienstag, 1. Februar 2022, 10:24:16 MEZ
>> *Betreff:* Re: Discussion from today
>>
>> 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 <mailto:josderoo@gmail.com>> Folgendes
>>>> geschrieben:
>>>>
>>>>
>>>> Nice and I have done a small test at
>>>> http://ppr.cs.dal.ca:3002/n3/editor/s/HO51TdBf
>>>> <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 <https://josd.github.io/>
>>>>
>>>>
>>>> On Mon, Jan 31, 2022 at 5:03 PM Pierre-Antoine Champin
>>>> <pierre-antoine.champin@ercim.eu
>>>> <mailto: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
>>>> <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 <https://josd.github.io/>
>>>>>
>>>>>
>>>>> On Wed, Jan 26, 2022 at 3:20 PM Doerthe Arndt
>>>>> <doerthe.arndt@tu-dresden.de
>>>>> <mailto: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 <https://josd.github.io/>
>>>>>>
>>>>>>
>>>>>> On Wed, Jan 26, 2022 at 2:07 PM Doerthe Arndt
>>>>>> <doerthe.arndt@tu-dresden.de
>>>>>> <mailto: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 <mailto: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
>>>>>>> <http://ppr.cs.dal.ca:3002/n3/editor/s/1Jisg9ES>
>>>>>>>
>>>>>>> @prefix log: <http://www.w3.org/2000/10/swap/log#
>>>>>>> <http://www.w3.org/2000/10/swap/log#>>.
>>>>>>> @prefix : <http://example.org/etc#
>>>>>>> <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 <https://josd.github.io/>
>>>>>>>
>>>>>>>
>>>>>>> On Tue, Jan 25, 2022 at 4:07 PM Jos De Roo
>>>>>>> <josderoo@gmail.com <mailto: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
>>>>>>> <https://github.com/josd/eye/releases/tag/v22.0125.1445>
>>>>>>> so that
>>>>>>> http://ppr.cs.dal.ca:3002/n3/editor/s/SHY7RXbG
>>>>>>> <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
>>>>>>> <https://github.com/william-vw/n3-editor-js/issues/5>
>>>>>>>
>>>>>>> Kind regards,
>>>>>>> Jos
>>>>>>>
>>>>>>> -- https://josd.github.io <https://josd.github.io/>
>>>>>>>
>>>>>>>
>>>>>>> On Tue, Jan 25, 2022 at 1:29 PM Doerthe Arndt
>>>>>>> <doerthe.arndt@tu-dresden.de
>>>>>>> <mailto: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
>>>>>>> <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
>>>>>>>> <mailto:josderoo@gmail.com>>:
>>>>>>>>
>>>>>>>> Dear Doerthe,
>>>>>>>>
>>>>>>>> Forgot to point to a concrete example
>>>>>>>> http://ppr.cs.dal.ca:3002/n3/editor/s/IT3znjsL
>>>>>>>> <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
>>>>>>>> <https://josd.github.io/>
>>>>>>>>
>>>>>>>>
>>>>>>>> On Tue, Jan 25, 2022 at 11:56 AM Jos De Roo
>>>>>>>> <josderoo@gmail.com
>>>>>>>> <mailto: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
>>>>>>>> <https://josd.github.io/>
>>>>>>>>
>>>>>>>>
>>>>>>>> On Tue, Jan 25, 2022 at 10:46 AM
>>>>>>>> Doerthe Arndt
>>>>>>>> <doerthe.arndt@tu-dresden.de
>>>>>>>> <mailto: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
>>>>>>>> <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
>>>>>>>>> <mailto: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
>>>>>>>>> <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
>>>>>>>>>> <mailto: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
>>>>>>>>>> <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
>>>>>>>>>> <https://josd.github.io/>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> On Mon, Jan 24, 2022 at 11:21 PM
>>>>>>>>>> Doerthe Arndt
>>>>>>>>>> <doerthe.arndt@tu-dresden.de
>>>>>>>>>> <mailto: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
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>
>>>>>>>
>>>>>>
>>>>>
>>>
>> <OpenPGP_signature><OpenPGP_0x9D1EDAEEEF98D438.asc>
>
Attachments
- application/pgp-keys attachment: OpenPGP public key
Received on Tuesday, 1 February 2022 15:01:58 UTC