Re: Blank node quantification

Hi Pierre-Antoine,

Note that the rule produced at (1) can not be expressed with the implicit quantification scheme that I am proposing (nor is it with the current implicit quantification scheme, by the way). More precisely, v:u is existentially quantified outside the formula that contains it, despite the fact that this formula is the object of log:implies.

This seems reminiscent of lexical scope vs. dynamic (runtime) scope of the (quantifier of the) existential variable, (ab)using programming terms.

In the lexical scope, the quantifier scope of a variable would be governed by the variable's lexical appearance (i.e., when originally appearing in a formula, the formula will define its scope). In the dynamic scope, this quantifier scope would be governed by where variable "ends up" during unification at runtime (i.e., when ending up in a formula, the formula will define a new scope). (The other two tenets remain the same.) 

In example 6, the lexical scope indeed yields:

  { @forSome v:e2. v:e2 a :UnicornEater } => { v:u :is :threatened } # with v:u still quantified by the top @forSome

And thus:

  v:u :is :threatened. # with v:u still quantified by the top @forSome

The dynamic scope would yield:

{ @forSome v:e2. v:e2 a :UnicornEater } => { @forSome v:u . v:u :is :threatened }. 

This can still be represented using implicit quantification.

In example 7, the lexical scope would yield:

   @forSome v:y { v:y :b :c } => { :d :e :f }.

For the dynamic scope:

   { @forSome v:y { v:y :b :c } } => { :d :e :f }.

At this point I seem to lean more towards the dynamic scope - this can represent examples 6 & 7 w/o explicit quantification, I think. Also, it seems to be more in line with my expectations (and,  not to mention my implementation and some of my use cases :-). 

I think either solution would still solve your original issue with "leakage" of blank nodes from quoted graphs, Pierre-Antoine, but I could be wrong.

Re my "use case": (apologies for the long example; it's abbreviated, and thus also incomplete):

:cmp-observation_resources rdf:value {
    ?report fhir:DiagnosticReport.result ?observation
} . 

#...

:cmp-find_low_o2_sat rdf:value {
    ?observation!fhir:Observation.valueQuantity!fhir:Quantity.value math:lessThan 88 . # this expands to a bunch of blank nodes
} . 

:tpl-o2_sat_low a :CdsRuleTemplate ;
    :components ( :cmp-observation_resources :cmp-find_low_o2_sat ) .

{    ?ruleTemplate a :CdsRuleTemplate ; 
        :components ?components .
        
    (?formula
        {
            ?components list:member ?component .
            ?component rdf:value ?formula . 
        }
    ?formulas) log:collectAllIn _:x .
        
    ?formulas log:conjunction ?result

} => {
    ?result => { [ a fhir:Condition ] }
} .

I'd expect the blank nodes to be existentially quantified within the rule premise (as per dynamic scoping), because I want the rule to be able to fire, of course.

But, one can perhaps consider this a corner case as well. I'll try to come up with some more examples.

(maybe this is a candidate for a "mode-like" setup as with SA / PG mode >:-)

 

William

 

On 2021-06-16 4:33 p.m., Pierre-Antoine Champin wrote:

And here's another example, which helped me put the finger on why I was not sure about that solution!

Example 7:

   :a :b :c.
   { ?x :leadsTo ?y } => { ?x => ?y }.
   { _:y :b :c } :leadsTo { :d :e :f }.

is equivalent to (using old-style explicit quantifiers) 

  :a :b :c.
   { ?x :leadsTo ?y } => { ?x => ?y }.
   @forSome v:y { v:y :b :c } :leadsTo { :d :e :f }.

This would then produce

   @forSome v:y { v:y :b :c } => { :d :e :f }.

which can not be serialized exactly without explicit quantification
(it can be approximated with a witness).
And this would therefore not produce  :d :e :f, which might be surprising...

(interestingly, the current version of EYE, does not produce :d :e :f with this example,
 while CWM does. EYE does if I replace _:y with ?y)

---

I am not claiming that this is a problem, but it can be considered counter-intuitive at least...

But maybe this is too much of a corner case to be a real problem...

  pa

On 16/06/2021 12:32, Pierre-Antoine Champin wrote:



Fiddling with yet another example that came to my mind:

Example 6:

  _:u a :Unicorn.
  _:e a :UnicornEater.
  { ?x a :Unicorn } => { { [] a :UnicornEater } => { ?x :is :threatened } }.

is equivalent to (using old-style explicit quantifiers) 

  @forSome v:u, v:e.
  v:u a :Unicorn.
  v:e a :UnicornEater.
  { ?x a :Unicorn } => { { @forSome v:e2. v:e2 a :UnicornEater } => { ?x :is :threatened } }.

I would expect it to produce (1)

  { @forSome v:e2. v:e2 a :UnicornEater } => { v:u :is :threatened }. # with v:u still quantified by the top @forSome

which in turn would produce (2)

  v:u :is :threatened. # with v:u still quantified by the top @forSome

Note that the rule produced at (1) can not be expressed with the implicit quantification scheme that I am proposing (nor is it with the current implicit quantification scheme, by the way). More precisely, v:u is existentially quantified outside the formula that contains it, despite the fact that this formula is the object of log:implies.

So in that case, we would still need to skolemize v:u (generate a witness) in order to express that rule.

  pa

On 16/06/2021 09:26, Pierre-Antoine Champin wrote:

Hi all, 

here's a crazy idea. I am not even sure I like it myself, but I wanted to ear others' opinion about it. 

During our last call, William made a point, with which I agree (assuming I understood it correctly). To sum it up: people use blank node in data more as "local" identifiers than as proper existential variables. This pleads for quantifying blank nodes at the top level. 

On the other hand, as we also pointed out during the call, blank nodes as used in rule bodies (and rule heads, I believe) need to be quantified locally. 

Hence my crazy idea: why not make the scope of blank node determined by the log:implies (=>) predicate? 

More precisely: 

* a formula that is the subject or object of log:implies defines a new scope for blank nodes 

* any other formula inherits the scope of its immediate parent 

* blank nodes in the top level scope are quantified *before* universals (which is consistent with viewing them as "local constants") 

Below is a long (apologies) list of examples. 

WDYT? 

  pa 


Examples 1: 

    :alice :belives { [] a :Unicorn }. 
    [] a :Person. 

is equivalent to (using old-style explicit quantifiers) 

   @forSome v:u, v:p. 
   :alice :belives { v:u a :Unicorn }. 
   v:p a :Person. 

---- 

Example 2: 

    { [] a :Unicorn } => { :world a :MagicalPlace }. 

is equivalent to (using old-style explicit quantifiers) 

    { @forSome v:u. v:u a :Unicorn } => { :world a :MagicalPlace }. 

(i.e. no change with today's interpretation) 

---- 

Example 3: 

    { ?x a :Person } => { ?x :mother [] }. 

is equivalent to (using old-style explicit quantifiers) 

    { ?x a :Person } => { @forSome v:m. ?x :mother v:m }. 

(i.e. no change with today's interpretation) 

---- 

Example 4: 

    :alice :belives { [] a :Unicorn }. 
    { ?x :believes { [] a :Unicorn } } => { ?x a :GulliblePerson }. 

is equivalent to (using old-style explicit quantifiers) 

    @forSome v:u1. 
    :alice :believes { v:u1 a :Unicorn }. 
    { @forSome v:u2. ?x :believs { v:u2 a :Unicorn } } => { ?x a :GulliblePerson }. 

which, unless I am mistaken, is also equivalent to 

    @forSome v:u1. 
    :alice :believes { v:u1 a :Unicorn }. 
    { ?x :believs { ?u2 a :Unicorn } } => { ?x a :GulliblePerson }. 

I would expect this to produce. 

    :alice a :GulliblePerson. 

---- 

Example 5: 

    :alice :belives { [] a :Unicorn }. 
    { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }. 

is equivalent to (using old-style explicit quantifiers) 

    @forSome v:u1. 
    :alice :believes { v:u1 a :Unicorn }. 
    { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }. 

I would have no problem with this producing 

    :alice :wishesToRide v:u1.  # where v:u1 is still quantified by the top @forSome