Is `:a :b {}` the same triple as `:a :b true`

[jeswr]

In rdfjs/types#37 there has been a discussion around whether parsers should interpret {} as the literal true.

To me this seems reasonable. But I think an explicit decision needs to be made on this at a spec level, rather than it being implicit dependent on ones' interpretation of whether the last statement in ground graph semantic is a syntactic or semantic one.

Once a decision is made I am happy to follow up with a PR containing either the positive or negative test case.

[doerthe]

The whole discussion here has several aspects.

First of all: In N3 and also in RDF the empty graph (already in N3's base interpretation and RDF's simple entailment) is always true.

But in the examples you give, we do not just have the empty graph, we do have the empty graph used as a term and that is different. If we have an N3 implication like

{}=>{:birds :can :fly}.

We can translate the premise to an FOL-like truth, all together

⊤ → can(birds,fly)

But: true is a boolean literal and not a formula, so the question here is rather whether we want to translate ⊤ to true. To add another example:

:doerthe :denies {}.

(freely translated to "Dörthe denies the truth" :)) then we have in FOL-style something like

denies(doerthe, ⊤)

Again, here the {} stands for ⊤ as a formula and it is up to us whether we think that this is the same as the boolean literal true.

Currently we see them as equal, we state that true is syntactic sugar for {}. So, following your request, I would either make more explicit that we do that or define some IRI n3:trueGraphTerm instead.

Could you (or others) think of any use cases in which we would like to be able to distinguish between true and {}? So far, I think it is a good solution to treat {} and true as equal, but I could be wrong.

[jeswr]

@william-vw ?

[william-vw]

Could you (or others) think of any use cases in which we would like to be able to distinguish between true and {}? So far, I think it is a good solution to treat {} and true as equal, but I could be wrong.

Not really, no. Inversely, I can imagine use cases where one would want to differentiate between false and { }, e.g., when a builtin fails (false) versus returning an empty formula (nothing was found / calculated). I can't think of an example where we'd have to distinguish between a true vs. { } value, but maybe I'm lacking the imagination...

[doerthe]

I thought about it and think that it might be problematic that {} and true might get two raw types.
Try the following with jen3 and EYE: https://n3-editor.herokuapp.com/n3/editor/s/jO8Pj1lC
We see that they differ and currently literals and graphs are disjoint (even though we do not explicitly state that in the semantics, but I guess we can get into trouble with some built-ins).

Also: log:includes only accepts graph terms as input, but {} is a literal according to EYE.

So maybe, it is not that easy after all...

[doerthe]

Ah, and I see that eye.js allows two types (but I guess you knew that :) )

[josd]

There is a very old eye there so an update is required. It was corrected a while ago and should give two types which you can see when choosing eye-js :result :is (log:Formula log:Formula log:Formula). :result :is (log:Formula log:Literal log:Formula). :result :is (log:Literal log:Formula log:Formula). :result :is (log:Literal log:Literal log:Formula).

…

-- https://josd.github.io

On Tue, Jul 4, 2023 at 3:51 PM doerthe ***@***.***> wrote: I thought about it and think that it might be problematic that {} and true might get two raw types. Try the following with jen3 and EYE: https://n3-editor.herokuapp.com/n3/editor/s/jO8Pj1lC We see that they differ and currently literals and graphs are disjoint (even though we do not explicitly state that in the semantics, but I guess we can get into trouble with some built-ins). Also: log:includes only accepts graph terms as input, but {} is a literal according to EYE. So maybe, it is not that easy after all... — Reply to this email directly, view it on GitHub <#185 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABPHJFWVWW4GZTWXGCCKKDXOQNWTANCNFSM6AAAAAAY3UFDTU> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[doerthe]

OK, so my main question is: can something be a formula and a literal at the same time? So far that is no problem, but I wonder whether it somehow clashes with RDF.