An Object-Oriented Architecture

Clearly, to be able to assign the correct values to the IN and FROM slots, the uniform algorithm has to know in which mode it is. To make this an automatic task the uniform algorithm has been embedded in an object-oriented environment. In this environment parsing and generation are defined as instances of a class PROOF, and the control mechanism of the underlying object-oriented language automatically will choose the right slots.

The item sharing method has been implemented on the basis of the implementation of the uniform tabular algorithm. Since Common Lisp now also entails the Common Lisp Object System (CLOS for short, [Steele1990]) as an standard extension, it has been very easy to embed the uniform tabular algorithm in an object-oriented environment. The definition of the general class PROOF is as follows:

(defclass proof ()
  ((name :accessor name :initarg :name
         :documentation "The name of the prover.")
   
   (sf :accessor sf :initarg :sf
       :documentation "The specified selection function.")

   (start-item :accessor start-item :initarg :start-item
               :documentation 
                 "The item that carries the goal to prove.")
   
   (result :accessor result :initarg :result
           :documentation 
             "Holds the result of the proof.")
   
   (agenda :accessor agenda :initarg :agenda
           :documentation 
              "The agenda processed by the prover.")
   
   (task-counter :accessor task-counter :initarg :task-counter
                 :documentation "Counts tasks from 0 upward.")
   
   (prio-fct :accessor prio-fct :initarg :prio-fct
             :documentation 
               "The priority function to be used by the agenda.")
   
   (restrictor-fct :accessor restrictor-fct :initarg :restrictor-fct
                   :documentation 
                     "The restrictor function defined for prover instance.")
   
   (lex-access-fct :accessor lex-access-fct :initarg :lex-access-fct
               :documentation 
                 "The function that performs lexical access.")
   )
  )

Note that for the above definition as well as for the definitions that come we make use of implementational aspects already described in 4.14.

Parsing and generation are simply defined as subclasses of this class and instances are created in the following way:

(make-instance 'parse
      :name "Parsing direction"
      :sf #'dynamic-selection
      :agenda (make-agenda)
      :task-counter 0
      :prio-fct #'depth-first
      :restrictor-fct #'restrict-clause
      :lex-access-fct #'string-access
      )


(make-instance 'generate
      :name "Generation direction"
      :sf #'dynamic-selection
      :agenda (make-agenda)
      :task-counter 0
      :prio-fct #'depth-first
      :restrictor-fct #'restrict-clause
      :lex-access-fct #'sem-access
      )

Note that the slot :lex-access-fct is the only slot that is assigned with different (functional) values.

All functions (with the few exceptions given below) are defined as methods for the class PROOF. This means, that the control function, the inference rules, as well as the agenda mechanism is still the same, and defined only once. In some sense, this means that the uniform tabular algorithm only exists one time, but is used by the two different instances. The advantage of using two different instances is that we can easily maintain different agendas or can use specific priority functions for both instances. Thus, our implementation directly mirrors the architecture of the item sharing approach as shown in figure 4.15.

The only functions that are defined as specific methods for the parsing and generation classes are MAKE-ITEM and ADD-ITEM (see section 4.14), and they differ only with respect to one additional call of a function. For the case of MAKE-ITEM, we have to provide, that if a new lemma is passive, we have to determine values for the slots of the direction that is currently not active. And for the case of ADD-ITEM we additionally have to add the new item to the corresponding item set (which has been created trough MAKE-ITEM, if the new lemma is passive) maintained by the inactive instance. Note that this does not mean that the new item is copied, but that the parsing and generation instances actually share this item (internally this means that Lisp provides two pointers to the same internal object).

To illustrate the behaviour of the item sharing approach consider the parsing and generation example given in section 4.11 (see also figures 4.13 and 4.14). For example, when during parsing the passive item for the partial string ``mit Maria'' is re-solved (in figure 4.13 it is the item with task counter 15 and item number 13), then this will cause the creation of an item set for generation with index ``mit(Maria)''. Additionally a pointer to the passive item 13 is established. In the item sharing approach the structure of the item 13 is (making use of the abbreviations introduced in section 4.11):

Thus if we perform generation with the semantics ``sehen(Peter,mit(Maria))'' the ``parsed'' passive item for ``mit Maria'' with semantics ``mit(Maria)'' can directly be used during the generation mode.