Re: ISSUE-82 (Unification): Shall Core limit unification to pattern matching (as PRD does)? [Core]

I'm not so happy with the new restriction in Core that forbids nested 
Externals.  Consider these "equivalent" rulesets:

RS1:
ex:A(2)
ex:A(?x) :- ex:A(?x - 1)

RS2:
ex:A(2)
ex:A(?x + 1) :- ex:A(?x)

RS3:
ex:A(2)
ex:A(?x) :- ex:A(?y), ?y + 1 = ?x

RS1 is unsafe, so if PRD adopts Core safety, we don't have to worry 
about it.
RS2 is safe, PRD has no problem with it, it would be nice if this is Core
RS3 is unsafe, so if PRD adopts Core safety then RS3 would not be in 
PRD, even though it poses no problems.

Dave Reynolds wrote:
>
> Christian de Sainte Marie wrote:
>>
>> Dave Reynolds wrote:
>>>
>>> Sorry to be stupid but could someone please what this means. The 
>>> notion in PRD surely depends on the execution strategy and in Core 
>>> we have no execution strategy.
>>
>> Trying to clarify what I meant, I came to the conclusion that I was 
>> wrong and that it had nothing to do with unification VS pattern 
>> matching.
>>
>> So, the good thing is that you are all right, and the wording of the 
>> issue does probably not make sense :-)
>>
>> The bad thing is that, is that there maybe an issue nonetheless, and 
>> I have no short description for it anymore :-(
>
> OK. It seems that this issue is about safety criteria and binding 
> patterns for builtins and my initial position is that the current 
> safety criterion in Core handles it.
>
>>> What would be an small concrete example a rule set which illustrates 
>>> the issue?
>>
>> Gary raised the problem long ago [1] wrt the example below example, 
>> and raised it again more recently with reference to variable binding 
>> in PRD in [2].
>>
>> From:
>> ex:A(2)
>> ex:A(?x) :- ex:A(?x - 1)
>>
>> Infer: ex:A(3).
>>
>> No way a PRD implementation can pass that test case, as far as I can 
>> see, because, PRD does not allow binding ?x to 3, in that case.
>
> First, to make things clearer we have modified Core to only permit 
> external function calls syntactically within equality statements not 
> nested within predicates calls. This doesn't fundamentally change the 
> problem[*] but it isolates it and at least makes it easier to explain 
> and talk about.
>
> So that ruleset would be rewritten as:
>
>   ex:A(2)
>   ex:A(?x) :- ex:A(?y),  ?y = ?x - 1
>
> That's still not something solvable by a production rule system.
> However, that was the whole point of adding safety criteria in Core.
> The rule is unsafe by those criteria [1] because ?x does not occur in 
> a plain atomic subformula in the condition.
>
> Where formula within Externals or Disjunctions are regard as non-plain 
> and all others are plain.
>
> Thus a PRD engine could not implement it as written but is not 
> expected to. A PRD engine could be a "safely conformant"[2] but not a 
> "conformant" consumer.
>
> The above is a legal (conformant) Core document but safely conformant 
> consumers are free to reject it (as being unsafe) or to accept it and 
> rewrite to some form they can handle. In this case:
>
>   ex:A(2)
>   ex:A(?x) :- ex:A(?y),  ?x = ?y + 1
>
> As it says in the Core overview section "Producers of RIF-Core who 
> require maximum interchange are advised to restrict themselves to safe 
> rules."
>
> Thus we've attempted to limit safe Core to the syntactic subset which 
> is implementable in PRD without the need for equational rewriting 
> while not ruling out unsafe Core rulesets.
>
> There may be some bugs lurking in the definitions that we haven't 
> found yet but I think the approach should work.
>
> However, I do think there is a problem with PRD in that the same 
> unsafe Core rule set is also a syntactically legal PRD ruleset and not 
> easily implementable in the production rule setting!
>
> Dave
>
> [*] OK you got me, that's an oversimplification. Without this change 
> the safety criteria weren't strong enough. With this change I think 
> they are.
> [1] http://www.w3.org/2005/rules/wiki/Core#Safeness
> [2] http://www.w3.org/2005/rules/wiki/Core#Conformance_Clauses
>

Received on Tuesday, 25 November 2008 17:04:40 UTC