Builtin assertions with unbound variables

[william-vw]

Yesterday's meeting left some core questions unanswered for me.

Under the interpretation discussed yesterday, are you saying that there a fundamental problem with a system firing the rule { (?a 1) math:sum ?s } => { :test1 :has ?s } (i.e., truthfulness of the antecedent)? Not talking about the practicality of implementation, or any other aspect, but rather the soundness of it. I feel much of yesterday's conversation were about implementation aspects, or about the difficulty of adding more builtin assertions into the rule. I understand these issues, but I'd like to start from the beginning.

[josd]

There indeed exist substitutions for ?a and ?s such that (?a 1) math:sum ?s is true, but what about (?a ?a) math:sum ?a, yes, there also exists one, namely ?a=0, but what about (?a 1) math:sum ?a and (?a ?a ?b) math:sum ?b, etc ...

[william-vw]

Ok, so for (?a 1) math:sum ?s there exist substitutions - so I assume there is not a fundamental problem with that one (?)

I understand a balance needs to be struck between completeness and soundness, of course. I'm just unsure how to go about it.

Since the BGP search on the builtin's "theory box" is defined as "constrained", an option is to define explicit constraints for each builtin. IMO these go beyond the expected datatypes for builtin arguments, since they simply reflect the "contents" of the theory box.

[pchampin]

Here is how I see things. For each built-in

• its semantics (a.k.a. theory box) should be well defined;
• the constraints on its execution shoulld also be well defined (i.e. math:sum only considers its object as output).

These define the minimal required behavior of a compliant implementation.

Then, a specific implementation may choose to be "smarter" when executing the built-in, as long as it complies with the semantics of the built-in (!), and as long as it produces the same triples as a minimally compliant implementation.

So

{ (?x 1) math:sum 43 } => { :ANSWER :is ?x }.

is not required to produce any triple, but a smarter implementation MAY produce :ANSWER :is 42..

Note that, in the case the specification requires a witness to be returned, I would allow a smarter implementation to return a concrete value instead of the witness. So it not so much about producing the same triples, as about producing at least as much information as a compliant implementation.