[Bug 1605] New: The inference engine is not specified (only the rule base it uses is)

http://www.w3.org/Bugs/Public/show_bug.cgi?id=1605

           Summary: The inference engine is not specified (only the rule
                    base it uses is)
           Product: XPath / XQuery / XSLT
           Version: Last Call drafts
          Platform: PC
        OS/Version: Windows 2000
            Status: NEW
          Severity: normal
          Priority: P2
         Component: Formal Semantics
        AssignedTo: simeon@us.ibm.com
        ReportedBy: fred.zemke@oracle.com
         QAContact: public-qt-comments@w3.org


2.1.3 Notations for inference rules
It says "Inference rules express the logical relation between
judgments and describe how complex judgments can be concluded from
simpler premise judgments."  This tells when an inference CAN be
made, but it does not tell me when an inference MUST be made.

There are a few places where you want the application of
inferences to be nondeterminstic, for example, whether an "and"
or "or" expression raises an error, or which error is propagated
from a function invocation with multiple errors.  However, for
the most part, you do not intend to leave the selection of which
inferences to draw entirely to the implementation's discretion.
Otherwise an implementation could simply refuse to draw some
conclusions and (for example) not complete the evaluation of 
some evaluatable expression, perhaps raising a gratuitous 
error, and still claim compliance.  This should be clarified.

Here are some general principles you might consider:

a) Any inference whose conclusion is of the form
statEnv |- Expr : Type that can be drawn during static analysis,
must be drawn during static analysis.

b) If the Static Typing Feature is supported, then any inference
whose conclusion is of the form
statEnv |- Expr raises TypeError that can be drawn during static
analysis, must be drawn during static analysis.

c) Any inference whose conclusion is of the form
dynEnv |- ... that can be drawn during dynamic evaluation, must be
drawn during dynamic evaluation.

Principle c) would seem to exclude certain desired nondeterminisms.
I think the solution is to build the nondeterminism into the
judgment through an "implementation-dependent choice" operator.  Thus

dynEnv |- Expr1 raises Error
dynEnv |- Expr2 => false
----------------------------
dynEnv |- choice (Expr1 and Expr2 => false,
                  Expr1 and Expr2 raises Error)

An alternative approach would be, instead of rule c), say
"if an Expr passes static analysis phase, then the dynamic
evaluation phase must draw inferences until either a judgment
of the form 'dynEnv |- Expr => Value' or a judgment of the form
'dynEnv |- Expr raises an error' is reached."

Received on Thursday, 14 July 2005 23:56:37 UTC