Inference

  Semantic processing, such as data flow analysis, in compilers and other language processors can frequently be specified as in a rule-based, logical deductive style. In Prop , deductive inference using forward chaining is provided as a built-in mechanism, orthogonal to pattern matching and rewriting, for manipulating user-defined algebraic datatypes.

Similar to rewriting classes, inference classes may be used for data encapsulation. An inference class is a combination of a C++ class, a database of inference relations, and a collection of inference rules of the form lhs -> rhs. The lhs of an inference rule is a set of patterns in conjunctive form. During the inference process, a rule is fired when its lhs condition is satisfied. A fired rule then executes the corresponding rhs action, which may assert or retract additional relations from the database. Using multiple inheritance, it is possible to combine a rewriting class with an inference class such that the rewriting process generates new relations to drive the inference process, or vice versa.

Datatype relations are not a distinct kind of data structure but are in fact simply algebraic datatypes declared to be such. For example, in the following definition three relation types Person, Parent and Gen are defined.

   datatype Person :: relation = person (const char *)
       and  Parent :: relation = parent (const char *, const char *)
       and  Gen    :: relation = same_generation (const char *, const char *);

   instantiate datatype Person, Parent, Gen;

Using these relations we can define an inference class that computes whether two persons are in the same generation. Nine axioms are defined (i.e. those whose lhs are empty) in the following. The two inference rules state that (1) the same person is the same generation, and (2) two persons are in the same generation if their parents are in the same generation.

   inference class SameGeneration {};

   inference SameGeneration
   {  -> person("p1") and person("p2") and
         person("p3") and person("p4") and
         person("p5");

      -> parent("p1", "p2") and
         parent("p1", "p3") and
         parent("p2", "p4") and
         parent("p3", "P5");

      person ?p -> same_generation (?p, ?p);

      parent (?x, ?y) and parent (?z, ?w) and same_generation (?x, ?z)
      -> same_generation(?y, ?w);
   };

In general, datatypes qualified as relations will inherit from the base class Fact, while a rewrite class definition implicitly defines two member functions used to assert and retract facts in the internal database. For example, in the above example, the following protocol will be automatically generated by the inference compiler.

   class SameGeneration : ...
   {
   public:
       virtual Rete&    infer       ();       // start the inference process
       virtual ReteNet& operator += (Fact *); // assert fact
       virtual ReteNet& operator -= (Fact *); // retract fact
   };

Using these methods, an application can insert or remove relations from an inference class. This will in turn trigger any attached inference rules of the class.

Another example

Consider the following example, which is used to compute Pythagorean triangles. Only one axiom and two rules are used. The axiom and the first rule are used to assert the relations num(1) to num(n) into the database, where n is limited by the term limit(n). The second inference rule is responsible for printing out only the appropriate combinations of numbers.

   datatype Number :: relation = num int | limit int;

   inference class Triangle {};

   inference Triangle
   {  ->  num 1;

          num m
      and limit n | n > m
      ->  num (m+1);

          num a
      and num b
      and num c | a < b && b < c && a*a + b*b == c*c
      ->  { cout << a << " * " << a << " + "
                 << b << " * " << b << " = "
                 << c << " * " << c << "\n";
          };
   };

Now, to print all the triangle identities lying in range of 1 to 100, we only have to create an instance of the inference class, insert the limit, and start the inference process, as in below:

   Triangle triangle;
   triangle += limit(100);
   triangle.infer();

Operational semantics of inference
This section is under construction.

Safe negation
This section is under construction.

Indexing and index specifications
This section is under construction.