Re: safety and external predicates

Dave Reynolds wrote:
> 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.

Our conformance statement introduces the notion of the "language" of an
implementation. we do not formally define what this means (which is
probably a good idea), but intuitively one would interpreted as the
processor of the consumer accepting all possible inputs in this
language.  Now, we know that there are implementations with a particular
language (e.g., Prolog) that accept all possible inputs in that
language, but that do not always compute the entailment relation
(because of undecidability of the language).  But we don't care about
that, because there is a mapping from BLD to the language of the
interpretation. I suggested we use a similar conformance statements for
Core, which would also give us this flexibility for this dialect.

So, concerning your example: if this were in core and a PR engine
accepts this as input (but does not necessarily compute the entailment),
then the engine would conform with Core (so, yes to question 3).

Whether it is wise to include such a test case is a different matter.
Intuitively, I would say it is not, by the same argument you gave (so,
no to question 2).


I am at the moment undecided about question 1 (whether the example is in
Core).  I would be interested to hear about implementations that do/do
not require such safeness in their inputs.

There are actually 3 ways to answer question 1:
a) no, it is not in Core, because it is not "safe" (however we will
define that in the end)
b) yes, it is in Core, but conformant consumers may reject "unsafe"
documents (this is what you suggested below)
c) yes, it is in Core and conformant consumers may not reject it (but
consumers may fail to come up with an answer, because we said yes to
question 3, and because of the way the conformance statement is phrased)

<snip/>

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

-- 
Jos de Bruijn            debruijn@inf.unibz.it
+390471016224         http://www.debruijn.net/
----------------------------------------------
No one who cannot rejoice in the discovery of
his own mistakes deserves to be called a
scholar.
  - Donald Foster