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.