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

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





------- Additional Comments From fred.zemke@oracle.com  2005-07-25 20:45 -------
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.

Received on Monday, 25 July 2005 20:45:34 UTC