Conformance

Let Τ be a set of data types, which includes the types specified in the RIF DTB document, and suppose Ε is a set of external predicates and functions, which includes the built-ins specified in the DTB document. Let D be a RIF dialect (e.g., RIF-BLD). We say that a formula φ is a D_Τ,Ε formula iff

• it is a formula in the dialect D,
• all the data types used in φ are in Τ, and
• all the externally defined functions and predicates used in φ are in Ε.

A RIF processor is a conformant D_Τ,Ε consumer iff it implements a semantics-preserving mapping, μ, from the set of all D_Τ,Ε formulas to the language L of the processor.

Formally, this means that for any pair φ, φ' of D_Τ,Ε formulas, φ |=_D,Τ,Ε φ' iff μ(φ) |=_L μ(φ'). Here |=_D,Τ,Ε denotes the logical entailment in the RIF dialect D with respect to the set of data types Τ and the set of externals Ε, and |=_L is the logical entailment in the language L of the RIF processor. In addition, a D_Τ,Ε compliant consumer must reject any document that contains a non-D_Τ,Ε formula.

A RIF processor is a conformant D_Τ,Ε producer iff it implements a semantics-preserving mapping, μ, from a subset of the language L of the processor to the set of D_Τ,Ε formulas.

Formally this means that for any pair φ, φ' of formulas in L, φ |=_L φ' iff μ(φ) |=_D,Τ,Ε μ(φ').

BLD: A conformant BLD consumer is a conformant consumer for all and only the datatypes and builtins required by BLD. It must reject all inputs which do not match the syntax of BLD. If it implements extensions, it may do so under user control -- having a "strict BLD" mode and a "run-with-extensions" mode.

A conformant BLD producer produces only the datatypes and builtins required by BLD.

A conformant BLD Document is one which conforms to all the constraints of this BLD specification, including ones which cannot be checked by XML Schema validator.

OLD STUFF -- includes explanation that might be useful.

%%% Say something about round-tripping?

Incorporate something about syntactic strictness, like:

   Systems which accept RIF input in the Basic Logic Dialect are
   required to check whether the input conforms to the grammar of BLD
   and (unless overriden by the user) to reject input documents which
   fail the check.  This check can be done by an XML Schema validating
   parser or by other software.  This check is required as part of the
   RIF approach to multiple dialects, extensions, and fallback
   translations.  If, instead of rejecting the document, a BLD system
   "repaired" it (such as by ignoring the part it did not recognize),
   it could silently produce incorrect results if it were (quite
   reasonably) given a RIF document which used some other dialect or
   some extension.  Given the undesirability of silent failures under
   normal use, systems which accept BLD as input MUST reject any RIF
   document which is not syntactically valid BLD.

   The rejection message SHOULD inform the user that the input does not
   conform to the syntax of the Basic Logic Dialect and that it may be
   a valid RIF document in some other dialect or using some extension.
   The system MAY allow the user to override the rejection and proceed
   with some ad hoc repair process, with clear warnings about the
   possibility of incorrect results.  The system MAY inform the user
   that it was unable to perform any fallback translation to BLD, but
   this messaging is not required in this version of BLD.

   EDITOR'S NOTE: The preceding text is expected to change once the
   fallback translation system is specified.  At that point, a new
   requirement is expected to be put into place, that systems SHOULD
   implement the fallback translation system, and that if they do not,
   they MUST inform users that they do not implement this RIF feature.