Re: safety and external predicates

Hi Jos,

>> I'm suggesting that Document Conformance should be unrestricted. That
>> Core be undecideable and that rulesets which might not terminate under
>> some execution strategies would be legal Core rulesets.  That a
>> Conformant Producer should be free to emit such rulesets (so long as the
>> semantics of the original ruleset is preserved, as normal).
>>
>> But that we allow a Consumer to be conformant even if it only preserves
>> semantics of some subset of legal rulesets so that it is possible for a
>> range of existing PR and LP engines to be conformant consumers even
>> though some legal RIF Core rulesets would, for example, lead to
>> non-termination with a forward execution strategy. If preferred we could
>> call this "minimally conformant", a term used in other W3C specs.
> 
> I think that would be fine.  However, I'm not sure we even need to
> define the subset for conformance.
> For example, in the conformance statement for BLD we talk about the
> language of a particular implementation.  However, it is known that any
> implementation for a language conformant to BLD, in the sense of the
> conformance statement in the BLD document, cannot be correct and complete.
> So, an implementation can be conformant without being able to compute
> all possible entailments, as long as its "language" is conformant with
> BLD. I think that for Core we could do the same.

Not sure I understand the implications of that.

Let's rephrase this as a test case using Axel's example. Take the rule 
set a1:

  Prefix(ex   http://example.com/example#)
  Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)

  Group  (
    Forall ?z ( ex:a(?z) :- ex:a(?x) External(pred:numeric-add(?x 1 ?z) )
    ex:a(1)
  )

and the positive entailment test case t1:
    premise:      a1 as above
    conclusion:   ex:a(3).

Some questions we need to answer for Core are:

(1) Is a1 a legal Core ruleset, i.e. a document containing that would be 
a Conformant RIF Core document?

(2) Is t1 an admissible Core test case?

(3) Could a RIF Consumer that translated Core into a production rule 
language in the obvious way be a Conformant RIF Consumer despite not 
being able to pass t1?

If I understand Axel's position correctly he would say "no, no, yes" 
respectively.

I'm arguing for "yes, no, yes", we don't care if someone writes a 
non-terminating rule set but don't want to exclude, say, production rule 
languages from implementing Core just because they can't execute such a 
test case.

I'm not quite sure what the implication of your suggestion would be. I 
think it would be "yes, yes, yes". Is that right? Thus there would be 
test cases that are legitimate Core test cases but an implementation 
that did not pass those test cases could still be a conformant 
implementation.

>> The question is how to define that subset.
>>
>> It was thinking (perhaps incorrectly) that the notion of a Core rule set
>> having a finite set of ground entailments is a well defined(definable)
>> one, even though there can be no algorithm for detecting that. So that
>> could be the basis for a conformance statement.
> 
> First of all, every ruleset will entail infinitely many ground atomic
> formulas, e.g., isInteger(0),  isInteger(1), etc.
> Second, the problem in logic is not the infinite set of entailment a
> ruleset has , but the undecidability of the entailment relation.  So,
> checking the entailment of a single fact might not terminate.

Both true, thanks for the correction, should have thought more before 
writing.

>> Alternatively we could pick a syntactic safety constraint as you and
>> Axel have proposed. However, under this scheme we would be using that
>> safety constraint only to limit conformance, not to constrain the
>> language - there would be no requirement for a translator (producer or
>> consumer) to implement that safety check and explicitly detect unsafe
>> rulesets.
>>
>> Does that make sense at least?
> 
> Yes, that makes sense (from a technical point of view at least).  In a
> conformance statement we would allow the language of the processor to be
> a subset of Core, namely, that subset for which the safety restriction
> holds.

Exactly.

Dave
-- 
Hewlett-Packard Limited
Registered Office: Cain Road, Bracknell, Berks RG12 1HN
Registered No: 690597 England

Received on Thursday, 28 August 2008 09:14:19 UTC