Fwd: Re: Hello, n3

Dear all,

William and I - by accident - continued our discussion privately. Please 
find below the summary.

Regards,
Doerthe


Hi Doerthe, all,

Oops, that was by mistake .. I’m not used to replying on mailing lists, 
lol.

//

/If you don’t mind, I will try to summarize our conversation below—I 
think we’re pretty much in agreement on most issues. If you have no 
problems with it then feel free to forward (a summarized version?) to 
the mailing list.///

• As an aside, I was wondering in what cases rules in consequences would 
be useful from a logical point of view (don’t have access to [1] right 
now). Isn’t the following just as effective:

{ ?C1 rdfs:subClassOf  ?C2, ?x a ?C1 } => ?x a ?C2

But I understand why it could be (syntactically) useful from a 
pre-processing point of view—since only the initial rule body needs to 
be instantiated with TBox terms (?).

 > Yes, you can do that as well, but then the rules you use cannot be 
"automatically" written by the reasoner.

/Indeed, that’s a pretty interesting aspect of it—the reasoner alone can 
instantiate the axioms based on the TBox. I will get around to reading 
your paper!/

• As mentioned by Doerthe, and unbeknownst to me previously, N3 allows 
to describe statements directly using “formulae”, without having to 
explicitly “s-p-o-encode” the described statements, i.e.,

{ :william dc:wrote :Moby_Dick } a n3:falsehood .

As also referenced by Doerthe, this very much reminded me of the work by 
Hartig et al., who introduced an extended semantics (RDF* and SPARQL*) 
[1] for reification support…

 > "The RDF semantic conditions do not place formal constraints on the 
meaning of much of the RDF vocabulary which is intended for use in 
describing containers and bounded collections, or the reification 
vocabulary intended to enable an RDF graph to describe RDF triples. This 
appendix briefly reviews the intended meanings of this vocabulary" 
(quote from: https://www.w3.org/TR/rdf11-mt/#whatnot)

 > In other words: it is not formally defined what rdf reification means.

For sure—but it says the same thing about RDF containers and collections 
(and I hope we’re not going to skip representing those as well in N3!). 
I think that the intended meaning and the particular representation as 
defined in that section, is currently more or less taken as the standard 
way to deal with reification (e.g., it is also listed in the RDF 
primer). For instance, Hartig et al. define a syntax and semantics for a 
different, more usable reification representation; and present a 
conversion into this “standard” reification representation (in fact, as 
a way to support the model-theoretic interpretation of RDF*).

 > The general problem of reification is the rather unusual use of blank 
nodes: as you know, blank nodes already have a meaning, they are 
existentially quantified (and I hope that the discussion on the mailing 
list will not change that). So, the above means according to RDF 
semantics: "There exists a falsehood, this falsehood is a statement and 
has the subject "William", etc.") That is not the same as saying "The 
statement that William wrote Moby Dick is a falsehood.". This 
semantically rather big difference is a problem for the formal 
specification of reification and we have indeed the exact same problem 
(but in my opinion even worse) with lists and containers (by saying that 
a list *exists* you do not have the list).

/Do you mean: having a more robust, formal definition of reification / 
lists / containers in place for N3, instead of building on the current 
(unformalized) method, would be a way forward? I’m not necessarily 
disagreeing here, but it could be a bit beyond our scope (?) Indeed, to 
me, there has always been this strange dichotomy between blank nodes 
being “existentially quantified” on the one hand (i.e., someone has an 
address, which has street X, etc.), and local identifiers on the other, 
where someone can actually reference this existential quantification 
elsewhere in the document (more like “existential variables” (?))./

 > N3 does not need these ugly constructs since it supports lists as 
"first class citizens" and has a construct for citation (the brackets 
{}). So, in practice I would add some rules making reification and 
first-rest-ladders "real" citations and lists and support only these 
"real" constructs in the mode theory. That would not exclude the use of 
them and by giving the rules we also give it the meaning you suggest here.

/I think we’re in agreement here—the current way of representing lists 
and reification is quite ugly and, by adding well-defined constructs, we 
can make working with them much easier. But in the end, this meaning 
would be based on the “intended meaning” just like with Hartig et al./

 > I would be really careful with such "intended" meanings since that 
will cause misunderstandings.

/Sure, but it’s unclear what else we could base ourselves on (?)/


/> There are different logics which have the notion of context, like for 
example KIF, ISO Common Logic and MacCarthy's logic of context ( there 
are many more). We have to agree whether we want to have a higher order 
construct here (I would rather say no) or whether we want to model it as 
first order logic. I hope that will become clear if everyone also 
explains how he or she wants to use the concept./
//

• I believe there could be a semantic layer, aside from a syntactical 
one, that facilitates working with lists (i.e., RDF collections). For 
instance, when computerizing the OWL2 RL axiomatization, one often runs 
into the following types of rules:

{ ?c owl:unionOf ?l, ?l x:member ?cl } => ?cl owl:subClassOf ?c

Where the x:member can be supported by adding an extra few rules [4]. 
Using rdfs:member seems to do something similar for RDF(S) containers, 
but that’s much easier since containers do not represent linked lists.

>  We should formalise built-ins: Cwm (and I think also the team 
submission) mentions a list of built-ins, you can find them at 
https://www.w3.org/2000/10/swap/doc/CwmBuiltins

>  EYE supports even more built-ins. Some are taken from RIF, some are 
customized: http://eulersharp.sourceforge.net/2003/03swap/eye-builtins.html

I hope that we as a group will be able to extend the list of N3 built-in 
predicates such that it won't be necessary for any reasoner to have such 
own predicates (but that is my vision for later).

For sure—with an accompanying semantics, these built-ins / constructs / 
terms .. could be implemented consistently (and perhaps even without 
necessitating built-in support; e.g., by simply adding the corresponding 
axioms to the dataset?).

• Even in case all list elements need to be referenced:

{ ?c owl:intersectionOf ?l, @forall :cl (?l x:member :cl, :cl a ?t, ?y a 
?t) } => ?y a ?c


>  Note that the rule above is problematic since the scope of your 
@forAll is basically the whole Web, so you can never know whether the 
antecedence of this rule is true. What you can do, is set a scope, 
saying something like "for all c1 mentioned in a certain document", this 
is something we can test.


I had based this on your examples from your presentation (slides 12, 16; 
I don’t remember defining explicit scopes) but perhaps I’m wrong ...

>  Your example would not work because it requires that whatever you find 
in the whole semantic we needs to be in the list ?l (@forAll :cl. ?l 
x:member :cl.). The reason for that is that the quantifier is in the 
antecedence of the rule. You basically say "if every cl is a member of l 
.... then" and not what you would like to have "for every member cl of l".

/Note that I merely used this notation since I noticed it on your slides 
and it seemed to suit the purpose. But I understand your point—the 
universal quantification should be scoped to include only members of the 
list: /

… Based on the rule you wrote, I think we could also go for local 
scoping here (so, mention a scope together with the universal 
quantifier), but maybe we should discuss that in the group (there could 
be better solutions).

William