This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
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."
This is a very good comment. This would probably help the reader a lot to have such a description. This is mostly of editorial nature, but would make the whole specification much more approachable. Let me try and sketch a description for the 'inferrence engine' as you call it. 1. What does an inferrence rule mean. (See comment also on bug [1612]). statEnv |- Expr1 : Type1 statEnv |- Expr2 : Type2 ------------------------ statEnv |- Expr1, Expr2 : Type 1, Type2 logically means: IF statEnv |- Expr1 : Type1 AND statEnv |- Expr2 : Type2 THEN statEnv |- Expr1, Expr2 : Type 1, Type2 The important point is the use of conjunctions between the preconditions. 2. What if you have several inferrence rules? a set of rules is essentially a disjunction: dynEnv |- Expr1 => false -------------------------------------- dynEnv |- Expr1 and Expr2 => false dynEnv |- Expr2 => false -------------------------------------- dynEnv |- Expr1 and Expr2 => false logically means: IF dynEnv |- Expr1 => false THEN dynEnv |- Expr1 and Expr2 => false OR IF dynEnv |- Expr2 => false THEN dynEnv |- Expr1 and Expr2 => false 3. How does the inferrence engine works You take the disjunction of all the rules and your try and 'prove' that a judgment is true or not. For static typing, typically, you are trying to prove: statEnv |- Expr : Type For the given expression, the inferrence rules will tell you if this is true or not. This is true if you can logically infer that the judgment holds, and results in a given type. If you cannot draw an inferrence, then the judgement does not hold and static typing fails. for example, take the following XQuery expression: fn:count((1,2,3)) you are trying show that statEnv |- fn:count((1,2,3)) : Type holds you can draw the inference as follows: statEnv |- 1 : xs:integer (from typing of literals) statEnv |- 2 : xs:integer (from typing of literals) ---------------------------------------- (from typing of sequence constr.) statEnv |- 1,2 : xs:integer, xs:integer statEnv |- 3 : xs:integer -----------------------------------------------------(sequence constr.) statEnv |- 1,2,3 : xs:integer, xs:integer, xs:integer declare function fn:count($x as item()*) as xs:integer statEnv |- xs:integer,xs:integer,xs:integer <: item* ----------------------------------------------------------(function call) statEnv |- fn:count((1,2,3)) : xs:integer So the static typing succeeds and results in the static type of xs:integer Here is another example: fn:nilled((1,2,3)) Here again, the inferrence can proceed up to: .... -----------------------------------------------------(sequence constr.) statEnv |- 1,2,3 : xs:integer, xs:integer, xs:integer But there is no rule that can infer the type of fn:nilled((1,2,3)), notably because the static typing rules for function calls will only hold if xs:integer,xs:integer,xs:integer <: node? which is false. Would something along those lines help? = Jerome
As an addition: we should have a 4. item which talks about non-determinism and errors. Notably: * An error is either raised when you reach a conclusion of the form 'Expr raises Error' or when no conclusion can be reached. * In the cases several conclusions can be reached, the result is non-deterministic. Note that this can only occur for the dynamic semantics, not the static semantics. For instance, consider the expression: true() or fn:error() The inference rules can allow to infer both: dynEnv |- true() or fn:error() raises Error as well as dynEnv |- true() or fn:error() => true() and both results are acceptable for the query. - Jerome
What you wrote is probably useful, but I had in mind something like the following. There are still gaps in this description because I am not sure this permits the following: 1) static type error if no inference of the form statEnv |- Expr : Type can be deduced. 2) short circuit evaluation of some expressions I wrote this without seeing your second reply, which goes into some of this. But I must quit now. The group can kick this around. Execution model of the inference engine This specification does not specify a particular order of execution. Instead, it uses a theoretical device called an inference engine. There are two inference engines, one for the static analysis phase, and the other for the dynamic evaluation phase. An inference engine consists of the following components: 1. The rule base (a collection of concrete inferences); 2. The deductions (a collection of concrete judgments); 3. The rule processor (an algorithm for utilizing the rule base to populate the deductions). 4. The objectives. The inference engine stops when either: a) a deduction that is an objective is placed in the collection of deductions, or b) no further deductions can be drawn. A rule base consists of a theoretically infinite number of inferences. Since there are infinitely many possible inferences, it is impossible for this specification to enumerate all of them. Instead, this specification provides a finite number of inference patterns. Each inference pattern has some finite number of premise patterns (possibly zero) and one conclusion pattern. Premise patterns and conclusion patterns can be viewed as templates from which concrete judgments can be derived by substituting concrete syntax or values for the italicized variables in the premise or conclusion pattern. For example, here is a possible premise or conclusion pattern: dynEnv |- Expr => Value This pattern is a shorthand for the infinite number of judgments that can be obtained by substituing concrete objects for the two variables, Expr and Value. For example, "a/b" is a concrete instance of Expr, and "2" is a concrete instance of Value. Substituting these two objects in the pattern produces the concrete judgment dynEnv |- a/b => 2 Note that this judgment is not necessarily true. It is the role of the inference engine to find true judgments, out of the space of all possible judgments. The inference engine seeks to discover true judgments. Any true judgment that the inference engine discovers is placed in the collection of deductions. Also note that this judgment might be true in some contexts and might be false in other contexts. This fact is handled by initializing the inference engine with the information about the initial state of the static and dynamic environment groups. So far we have seen an example of a pattern for a single judgment. Such patterns are grouped into an iference pattern. An example of an inference pattern is dynEnv |- Expr1 => Value1 dynEnv |- Expr2 => Value2 ------------------------- dynEnv |- (Expr1, Expr2) => (Value1, Value2) This inference pattern is a template from which concrete inferences such as the following may be constructed: dynEnv |- a/b => 2 dynEnv |- x/y => 3 ------------------- dynEnv |- (a/b, x/y) => (2, 3) This specification contains many inference patterns. Each inference pattern denotes a collection of concrete inferences, consisting of all inferences that can be obtained by substituting appropriate objects for the variables in the inference pattern. Every possible combination of objects that substitute for the variables constitutes a separate concrete inference. It must also be recognized that there are infinitely many possible static and dynamic environment groups. Each concrete static environment group or concrete dynamic environment group is a possible value for the statEnv or dynEnv in judgments. Thus a judgment pattern such as dynEnv |- Expr => Value denotes the infinite collection of judgments that a particular dynamic environment group evaluates a particular expression to a value (and that concrete judgment may be true or false). The inference engine for the static analysis phase uses only those inference patterns whose conclusion begins with either "|-" or "statEnv |-". The inference engine for the dynamic phase uses all inferences in this specification. The rule processor may be visualized as a collection of "daemons". Each daemon corresponds to a particular concrete inference. If D is the daemon for a concrete inference I, then the behavior of D is as follows: if D detects that all the premises of I are in the pool of deductions, then D places the conclusion of I in the pool of deductions. The initial state of the inference engine is that the pool of deductions is empty. From this state, any concrete inference with no premises may be placed into the pool of deductions by its daemon. This will provide a collection of judgments which will enable other daemons to "fire" and place more judgments in the pool of deductions. This provides the seed to start the recursive activity of an inference engine. Once started, the inference engine could continue forever, expanding its collection of deductions. However, the user is only interested in learning certain deductions, so the inference engine can stop when the objective set by the user has been deduced. The [query/expression] supplied by the user determines the objectives. In the static analysis phase, the objectives are to find a deduction matching either of these patterns: statEnv |- Expr : Type or statEnv |- Expr raises a type error where statEnv is the initial static environment group and Expr is the user's [query/expression]. In the dynamic evaluation phase, the objective are to find a deduction matching any of these patterns; dynEnv |- Expr => Value or dynEnv |- Expr raises a type error or dynEnv |- Expr raises a dynamic error where dynEnv is the initial dynamic environment group.
Fred, The WGs have discussed this thread today and is leaning toward adding explainatory material along the lines I suggested in my additional comment #1, and not go all the way to add the kind of description for an 'inference' engine that you suggest. The rationale for this is that the FS is more declarative in nature that what you suggest, and that it would require more work. Please let us know if you could live with this before Wednesday next week if possible so we can process this issue at our next telcon. Best, - Jerome On behalf of the XML Query and XSL WGs
I can live with your "declarative description", with a little tightening of the description, as follows: Your point 1, "what does an inference rule mean". What you wrote is good, but I would add my proposal, that the judgments and inferences in FS are patterns, which represent every possible instantiation of the variables with concrete values matching the BNF non-terminal indicated by the name of the variable. For example, the judgment pattern statEnv |- Expr1 : Type1 statEnv |- Expr2 : Type2 ------------------------ statEnv |- Expr1, Expr2 : Type1, Type2 has as one of its concrete instantiations statEnv |- (a/b) : xs:integer+ statEnv |- (c + d) : xs:integer -------------------------------- statEnv |- (a/b), (c+d) : xs:integer+, xs:integer This adddresses the issue about the implicit quantification of the inferences (more about that in my response to #1612). Yor point 2, "what if you have several inferences?". I question whether you really mean that the implicit conjunction between inferences is OR. Consider your example: dynEnv |- Expr1 => false -------------------------------------- dynEnv |- Expr1 and Expr2 => false dynEnv |- Expr2 => false -------------------------------------- dynEnv |- Expr1 and Expr2 => false This does not mean OR, ie, that at least one of these inferences is true. Both of the inferences are true. For example, consider the concrete instantiations with "2=3" as Expr1 and "1=1" as Expr2. Then the two inferences are: dynEnv |- 2=3 => false ---------------------------- dynEnv |- 2=3 and 1=1 => false dynEnv |- 1=1 => false ---------------------------- dynEnv |- 2=3 and 1=1 => false Both of these inferences are true. The second one is true due to the mathematical definition of "material implication", ie, either "dynEnv |- 1=1 => false" is false, or "dynEnv |- 2=3 and 1=1 => false" is true. What may be deceptive about this example is that the second inference, though true, is also irrelevant because you can never deduce "dynEnv |- 1=1 => false". This is an issue in general with material implication, that there are many irrelevant cases. Implementations will of course not need to worry about ever utilizing an inference with a false premise, but there is no simple way to weed them out of the specification (or mathematics) so we just live with it. Further, I think that saying the implicit conjunction is OR actually breaks the specification. This is because, if P OR Q, where P and Q are statements, you do not know whether it is P that is true, or Q, or both. You do mean that both are true, so P AND Q is the correct conjunction between inferences. I think when you proposed OR, what you meant was "the implementation gets to pick which inferences to use in making its deductions". I expressed this concept by providing asynchronous daemons that fire when they see that their premise(s) are fulfilled. (To model that an implementation ignores a particular inference, simply let the daemon for that inference be so slow to fire or with such a low priority that other inferences are drawn first.) Anyway, this is generally true about inference engines, that there is an element of choice when deciding which inference to use. Take for example a working mathematicican, who is an inference engine whose rule base is all the mathematics he has learned. When tackling a problem, he may or may not happen to use a particular inference known to him. But this does not mean that he regards the collection of truths that he knows as logically conjoined by OR. Rather, he simply has a choice about how to reach his objective. Your point 3, "how does an inference engine work". In this section you say "For static typing, typically, you are trying to prove: 'statEnv |- Expr : Type' ". I have an issue with the word "typically", because it suggests that there is no definite target for the inference engine, and to that extent, leaves the specification vague. "Typically" does not connote a normative specification. To fix this, I would tighten this to say "The objective of the inference engine is to deduce either a judgment of the form 'statEnv |- Expr : Type', where statEnv is the initial static environment group, Expr is the [query/expression] submitted by the user, and Type is to be discovered by the inference engine, or to conclude that there is no such Type." I realize that the inference engine may have other judgments that it attempts to prove along the way to its final objective. This is probably why you inserted the "typically". If you want to capture this thought, I suggest a further sentence such as "The inference engine may also attempt to deduce additional judgments as steps in its pursuit of its overall objective." Your point 4, "about non-determinism and errors", this is good and important. Concerning the first subpoint "An error is either raised when you reach a conclusion of the form 'Expr raises Error' or when no conclusion can be reached." My question is whether an error is raised only for the the failure to reach the overall objective, or could an error be raised for the failure to reach an intermediate objective? I don't know the answer to this.
Dear Fred, I agree with most of your changes. I think they are all good suggestions. Again, I think I would like to stay away from any description which is too procedural or implementation oriented (such as introducing something like a 'deamon'). It seems that we are mostly in agreement though, and that the remaining part could be left to editorial discretion. Best, - Jerome
The working group endorses Jerome's response and will resolve the issue. Please close the issue if you agree with the resolution or reopen the issue if you disagree.