Semi-explicit quantification

Hi all,

Following a number discussions (during calls, on github, and in private 
email conversations), here's a new crazy idea for revisiting 
quantification in N3. This is a variant of the "different kinds of curly 
brackets" idea that I mused with previously. The rationale is to (a) 
restrict the expressiveness of the language to avoid falling into full 
FOL, while (b) keeping it possible to use log:semantics (see issue #90) 
and similar constructs. Disclaimer: whether (a) is actually achieved by 
this proposal remains to be formally proven.


The proposal:

* universal variables are always represented by quick-variables (e.g. 
?x); existential variables are always represented by blank nodes (e.g. 
_:b or [ ... ])

* @forAll and @forSome are not used anymore

* define two new keywords @QAE and @QE, that can be used in any formula, 
without any argument, directly followed by a period ("."). A good 
practice is to put them before any triple in the formula, but their 
position is actually irrelevant. E.g.

     :alice :believes { @QE. [] a :Unicorn. [] a :Dragon }.
     :doc1 :contains { @QAE. { ?x a :Unicorn } } => { ?x a 
:FantasticBeast } }.

* whenever a blank node appears, it is quantified in the inner-most 
enclosing formula that contains @QE or @QAE

* whenever a quick variable appears, it is quantified in the inner-most 
enclosing formula that contains @QAE

* @QAE is implicitly contained in the root formula of any N3 document

* @QE is implicitly contained in the formulae on either side of '=>' and 
'<='

The last bullet is optional -- I think it would make writing rules 
easier, but I know that Doerthe (at least) has reservations about it... 
Note that I propose to make it an effect of the '=>' and '<=' keywords, 
so entirely linked to the *surface* syntax.


Unifying two formulae would require that their "quantification level" 
match, so the following would not match:

     { @QE. [] a :Unicorn. [] a :Dragon } log:includes { ?x a :Unicorn }.
     { @QE. [] a :Unicorn. [] a :Dragon } log:includes { _:u a :Unicorn }.

but the following would

     { @QE. [] a :Unicorn. [] a :Dragon } log:includes { @QE. _:u a 
:Unicorn }.


   best

Received on Thursday, 26 August 2021 09:24:04 UTC