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

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 :-(

Anyway, another way to ask the question I have in mind is: is a forward chaining conformant implementation of Core possible without using some feature that PRD does not have? In the end, it might end up being exactly the issue that Gary raised in [2] (I thought initially that it subsumed it).

The point is: if one wants to make sure that PRD extends Core, one has to compare their semantics. Since PRD does not have a model theory, one way would be to check whether an implementation of Core syntax with PRD semantics could be conformant to Core, and to determine under what condition it would, or why it would not.

As it happens, the syntactic subset of PRD that is equivalent to Core does not have negation in the condition part, and has only assertions in the action part. The order in which the rules are fired is thus immaterial, and the result will be the same whatever the conflict resolution strategy, provided that the termination test is that no rule is fireable (which is the only termination test specified in PRD, at this point).

So, we are lucky, and the fact that PRD has an execution strategy and Core does not is immaterial to the comparison.

Further more, for rules with no negation in the condition and only asserts in the actions, the semantics of PRD seems to be equivalent to the fix-point semantics of the syntactically identical logic programme in Core (or is it: inflationary semantics, or Apt-van Emden-Kowalski semantics? My understanding is that they are all the same, at least for that subset, but you know that I am no expert), which, in turns, is known to be equivalent to the minimal model semantics.

So, lucky again? Maybe or maybe not, because, PRD's way to bind variables to produce fireable instances seems to differ from how ground clauses are produced in the inflationary (forward chaining) version of Core's semantics (initially, I thought that I could pin down the difference in terms of pattern matching VS unification, but that does not work).

> 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. 

I do not see either how Core would produce the ground clause: ex:A(3) :- ex:A(2), and that's why I thought the maybe Core allowed to unify ex:A(?x - 1) and ex:A(2) (but, yes, that has nothing to do with full unification vs pattern matching).

Or is it that there can be no forward-chaining implementation of Core? But, where am I mistaken wrt to the inflationary semantics, then?

Cheers,

Christian

[1] http://lists.w3.org/Archives/Public/public-rif-wg/2008Aug/0085.html
[2] http://lists.w3.org/Archives/Public/public-rif-wg/2008Sep/0143.html

Received on Monday, 24 November 2008 15:49:39 UTC