[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-20 23:55 -------
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.

Received on Wednesday, 20 July 2005 23:55:46 UTC