On 14/07/16 15:44, Paul Houle wrote:
If I understand that right,  you're saying that the signature for
builtins would have to change because there would have to be some way to
either pass back a list of possible bindings or maybe pass back one
binding and an indication that there might be more,  right?

Right. Though just changing the signature isn't enough of course, you would need a non-trivial change to the backward reasoner to handle this.

If this was a pure backward rule engine then the builtins would have support for either multiple results or for explicit backtracking (e.g. something like the prolog 4-port model). Historically we started with a forward engine and builtins were designed for that, then the system was extended to add backward and hybrid rules but for backward compatibility and simplicity we stuck with the limited notion of builtins as just filters not as generators of alternative solutions.

A specific multi-binding case I have thought of is a function like
"lcfirst" in PHP which lowercases the first character in a string.  If
you write

lcfirst(A,"night")

there are two solutions for A,  "night" and "Night" and it would be
reasonable to search backwards.  On the other hand,  if you are
lowercasing everything

lc(A,"night")

then you have 32 solutions when the right parameter has no uppercase
letters,  generally 2^N solutions where N is the number of  lowercase
letters.  It is more reasonable to do the search in the other direction
(look up all A and see if they match) although the perfect system would
probably search A over a small set of prefixes and then filter.

Sure and then you have cases like relational operators where the results can be infinite (?x > 0 etc).

That sort of thing is possible in constraint logic programming where the equational literals act as constraints rather than generators or filters. Then you have a constraint engine can checks whether the current set of constraints is satisfiable. That's a whole different world :)

Even add() might have problems because of numeric coercion (there might
be more than one type which fits.)

Would the ability to return binding sets affect both the forward and
backwards modes?

It's not clear what such builtins would mean in the forward world.

For existing builtins like add it's easy - they are all functions so they don't get invoked until all the inputs are bound and then generate only one answer.

If you allowed the current builtins to have other binding patterns with non-deterministic answers and/or allowed builtins to generate multiple results then I'm not sure what that would mean. I guess you would expect the forward rule to fire and generate all the possible answers.

Dave

-- Paul Houle paul.ho...@ontology2.com On Thu, Jul 14, 2016, at 03:57
AM, Dave Reynolds wrote:
>   13/07/16 18:24, Paul Houle wrote:
> >In the following docs:
> >
> >https://jena.apache.org/documentation/inference/
> >
> >The arithmetic builtins are described as such:
> >
> >"Note that these do not run backwards, if in sum a and c are bound and b
> >is unbound then the test will fail rather than bind b to (c-a). This
> >could be fixed."
> >
> >This is repeated in the source code for said functions.
> >
> 
>https://github.com/apache/jena/blob/master/jena-core/src/main/java/org/apache/jena/reasoner/rulesys/builtins/Sum.java
> >
> >in that case at line 78.
> >
> >My question is:  is the only reason this does not work because the
> >Builtin doesn't handle it,  or because the engine wouldn't be able to
> >work correctly if the Builtin was fixed?
>
>If I remember correctly the engine requires a deterministic answer from
>the builtin - it doesn't support builtins that expand the search space
>(doesn't support return of a set of legal answers). So specific cases
>where there's only one unbound to an arithmetic builtin and only one
>result to bind could be supported. However, in general once you allow
>arithmetic expressions to run backwards you are getting into equational
>constraint solve territory.
>
>Dave

Reply via email to