- From: Pierre-Antoine Champin <pierre-antoine@w3.org>
- Date: Thu, 26 Aug 2021 11:23:44 +0200
- To: "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <cedbf1ca-78d9-0128-cd26-fd4cd840ed15@w3.org>
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
Attachments
- application/pgp-keys attachment: OpenPGP public key
Received on Thursday, 26 August 2021 09:24:04 UTC