Quoted formulae generated by `log:semantics` are tricky

[pchampin]

Context:

• quickvars (?x) are universal variables, always quantified at the top-level of the document
• blank nodes are existential variables, always quantified in the inner-most pair of brackets containing them
• we have decided to get rid of explicit quantifiers, in order to make the language simpler without sacrificing any major use-case

Now consider the following

{ <someuri.n3> log:semantics ?x } => { :alice :believes ?x }.
# assuming that <someuri.n3> contains
{ ?x a :Dog } => { ?x a :Animal }.

The problem is that we can not correctly serialize the result. The correct serialization of the result would be (using explicit quantifiers)

:alice :believes { @forAll :x. { :x a :Dog } => { :x a :Animal } }.

but this can not be serialized using the implicit quantification conventions above. It also means that the quoted formula "produced" as the object of log:semantics should not be treated by the reasoner as a usual quoted formula.

Different solutions have been discussed over several calls:

• reintroduce explicit quantifiers
• introduce a special kind of brackets or a special literal datatype to represent the special formulae produced by log:semantics
• accept that this special kind of formula must be supported by reasoners but can not be serialized (or only in a lossy way)
• get rid of log:semantics

[gkellogg]

What about simply renaming quickvars from imported documents. This might require a scheme similar to JSON-LD bnode renaming when flattening, but there are probably similar ways to do it without being so explicit.

Corner cases:

• log:semantics using the same document multiple times.
• Document used in a chain of other log:semantics operations.

Should the quick car be consistent with all uses, or localized per usage?

the problem is similar with explicit quantifiers, but document relative IRIs mostly address this.

[pchampin]

@gkellogg the problem is not only about the name of variables (although of course this needs to be dealt with to avoid clashes). Depending on where they are quantified, this changes the meaning of the formula:

:alice :believes { @forAll :x. {:x a :Person} => {:x a :Nice} }.
# alice believes that all people are nice

vs.

 @forAll :x.  :alice :believes { {:x a :Person} => {:x a :Nice} }.
# for any thing in the world, alice believes that if it is a person, then it is nice

The 2nd statement is weaker than the first one -- although arguably their "practical" implications do not differ much...

[pchampin]

For the record, CWM's implicit quantification conventions are "log:semantics friendly": curly brackets do not behave differently from document boundaries...

[gkellogg]

@gkellogg the problem is not only about the name of variables (although of course this needs to be dealt with to avoid clashes). ...

But, this is not just a problem with log:semantics, but with the elimination of explicit quantification in general. Quickvars do not allow an inner scope, whether or not it comes from an external file.

[josd]

I wanted to point to https://lists.w3.org/Archives/Public/public-cwm-talk/2015JanMar/0003.html esp.

[[
The main differences that we have in our implementation are
1/ the scope of quickvars like ?A is the statement level
...
]]

Statements are clauses i.e. facts (triples) and rules.

so this is like a 5th possibility :-)

[doerthe]

But, this is not just a problem with log:semantics, but with the elimination of explicit quantification in general. Quickvars do not allow an inner scope, whether or not it comes from an external file.

In most cases, our decision to only allow implicit quantification and to fix the scope for this quantification as we did only reduces the expressivity of the language. This reduced expressivity will make the reasoning easier and of course we need to find a compromise between expressivity and performance of reasoners.

What makes the log:semantics example special is that we can construct our tricky cases by only using the language elements we allowed in our restricted version of N3 and that is the problem. Ideally, we want our reasoning to be complete, that is we want the reasoner to produce all meaningful (whatever that means) logical consequences of our formulas. The problem here is that there is no way the reasoner produces the correct N3 reasoning result since we cannot even express this correct result in the language.

[doerthe]

I wanted to point to https://lists.w3.org/Archives/Public/public-cwm-talk/2015JanMar/0003.html esp.

[[
The main differences that we have in our implementation are
1/ the scope of quickvars like ?A is the statement level
...
]]

Statements are clauses i.e. facts (triples) and rules.

so this is like a 5th possibility :-)

I don't understand how this solves the problem.

I would still understand :alice :believes { { ?x a :Dog } => { ?x a :Animal } }. as a statement, i.e. I would expect that it means @forAll :x. :alice :believes { { :x a :Dog } => { :x a :Animal } }..

Or would you define some kind of hierarchy which ensures that the quantifier gets inside? If so, how exactly would you do it?

[william-vw]

In my current understanding I think scopes can be "leaked" in two general ways:

• When using blank nodes, since they are scoped by the inner-most pair of brackets:

{ :will :lives _:b0 . _:b0 :place :buckinham_palace ; :number 12  } a :Lie .
{ { ?person :lives ?place. ?place :place :buckinham_palace ; :number 12 } a :Lie } => { ?place a :IncorrectPlace } .

Could generate:

_:bX a :IncorrectPlace # no co-referral possible due to _:b0's local scope

• When loading external graphs using log:semantics, since these have their own top-level scope (example from meeting notes):

:x a :Thing.

{<https://raw.githubusercontent.com/doerthe/N3tests/main/universals.n3> log:semantics ?y}=>
{?y =>{:a :b :c}}.

# where universals.n3 contains:
#PREFIX : <https://example.org/ns/example#>
#?x a :Thing .

Could generate:

{ ?x a :Thing } => { :a :b :c } . 
# but ?x should be quantified as { \forall :x . :x a Thing }, not \forall :x . { :x a Thing }

And hence (wrongly)

:a :b :c .

Perhaps a related problem: the Apache Jena API is able to read the current "model" from any arbitrary number of sources (one just invokes the model's "read" method for each). Could one see this as similar to invoking log:semantics a bunch of times, for each source, and then asserting the contents of the loaded formula? In that case, this could just be a different instance of the same problem - each of these sources would have their own top-level scope, which is then "leaked" into the same main graph .. Or, maybe it could point towards a solution of dynamic scoping for these particular cases >:-)

I have to say, Jena's "read" feature is quite useful to modularize one's code - I've used the log:semantics in a few instances for the same purpose.

Another issue: does this problem transfer to log:conclusion:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .

{<https://raw.githubusercontent.com/w3c/N3/master/tests/universals2.n3> log:semantics ?y .
( ?y { :k :y :z } )log:conjunction ?c .
 ?c log:conclusion ?c2
}=> { ?c2 a :Conclusion }.

[doerthe]

Different solutions have been discussed over several calls:

• reintroduce explicit quantifiers
• introduce a special kind of brackets or a special literal datatype to represent the special formulae produced by log:semantics
• accept that this special kind of formula must be supported by reasoners but can not be serialized (or only in a lossy way)
• get rid of log:semantics

Not my favourite solution, but we also discussed to do nothing, i.e. just give no output in that case.

[josd]

I don't understand how this solves the problem.

I would still understand :alice :believes { { ?x a :Dog } => { ?x a :Animal } }. as a statement, i.e. I would expect that it means @forAll :x. :alice :believes { { :x a :Dog } => { :x a :Animal } }..

Or would you define some kind of hierarchy which ensures that the quantifier gets inside? If so, how exactly would you do it?

We could for instance say that quickvars should only be used for rules and that their scope is the outermost rule in which they occur. Facts containing universals can always be expressed as e.g. {?x :p :o} <= true.