william-vw
commented
5 years ago To elaborate on the second "type" of use-case for scoped negation as failure:
This involves identifying cases where all resources in an identified set have to adhere to a given condition. For instance, when needing to check whether all subtasks of a composite task have a completed status. In an open-world context this would not be possible, since it requires assuming that there's no other graph that defines another subtask (that, in this case, is not completed).
One can represent this using scoped negation as failure (see here): using log:notIncludes, one can rule out the existence of a counter-example (i.e., a non-completed subtask) and solve the problem.
However this requires an N3 developer to themselves redefine the problem from (scoped) universal quantification to scoped negation as failure, which I do not think is trivial.
Hence an option here could be to introduce a new builtin to represent "scoped" universal quantification. This would however not be a simple "macro expansion" as with the SNAF builtin (i.e., expanding the built-in to a simple chain of existing builtins), since there's no current way to express negation in N3 (?) For instance, inventing a new built-in (@forAll <varlist> @in (<doc>|<formula>)):
@forAll :t. {
:t a :CompositeTask.
@forAll :st @in <subtasks.n3> {
{ :t :subTask :st. } log:implies { :st a :Completed. }.
}.
} log:implies {
:t a :AllTasksCompleted.
}.Would have to be converted to:
@forAll :t. {
:t a :CompositeTask.
<subtasks.n3> log:semantics ?sem.
?sem log:notIncludes { :t :subTask _:st. _:st a :NotCompleted. }
} log:implies {
:t a :AllTasksCompleted.
}.I.e., the negation of Completed would need to be known as well. (Not saying that this is an insurmountable problem, but still.)
doerthe
josd
Realizing negation-as-failure is currently realized by chaining two or three built-ins, i.e.,
log:semantics(log:conclusions)log:notIncludes. See here for an example. This seems quite cumbersome for representing a single concept.If we introduce a custom built-in (such as notIn) we only require a single built-in to represent NAF, which could be a good selling point for N3. Implementation-wise it could be simply macro-expanded to the aforementioned chain of built-ins (where backward-chaining systems could optimize its implementation). On the other hand, this requires going beyond what N3 currently provides, which could lead to a slippery slope of new built-ins that bog down the standardization process.
A similar issue occurs with representing a "scoped" universal quantification as exemplified here. This can also be represented using a combination of
log:semantics(log:conclusions)log:notIncludes, as shown here. Nevertheless it seems trickier to define a custom built-in for this as compared to the above case.Note that Eye also has custom built-ins (including findall, fail) that can be used to represent NAF (see examples directory).
Thoughts?