A Larger Example of Techniques Editing

This page gives a larger example of the form of predicate construction used in Chapter 6. We have chosen the satisfy predicate which we used at to help us explore the behaviour of an operator model. To do the example we need an extra form of addition, as described below.

adds a pair of arguments, S and F, to a predicate named P. The purpose of S is to accumulate information on the way down through the recursion, with F being used to ``pass back'' the final instantiation of S. The first mapping is the recursive case which - via the pairs condition - ensures that the accumulator is passed through each of the recursive goals (in order) in the condition, B. For example, if B contains the sequence then these are replaced by . The second mapping takes a non-recursive expression and adds the two arguments S and F, while noting that F should be obtained from S.

constructs the conjunction of terms, , from B by replacing the sequence of recursive subgoals, in B by the new sequence in corresponding positions in .

We start by instantiating the skeleton (defined at ) to give:

We know that satisfy has to unpack conjunctions of terms so we instantiate F to the conjunction symbol, `'.

There are two different base cases for satisfy: when C is an input or when C is a system defined goal. Our skeleton currently has only one base case so we replicate the expression to give .

We then make the following instantiations:

• The first base case succeeds when C is an input for which we can find a potential output so is instantiated to:
  
• The second base case succeeds when C is a non-conjunctive term which is system defined so is instantiated to:
  
• The means of obtaining P from C in the final recursive case is to test that C is not system defined, a conjunction or an input and that there is a clause determining C from P. This is expressed by instantiating to:
  

This completes the flow of control for satisfy, which is determined solely by the first argument and associated conditions. Turning to the second argument, this is simply a number giving the depth limit, which needs to be carried through the search for solutions. We apply the addition (defined in Chapter 6 of the book):

The third and fourth arguments of satisfy are used to carry in the current input streams (via the third argument) and pass back the revised set of streams (via the fourth argument) after processing has occurred. This can be viewed as a form of paired accumulator so we apply the addition (defined above):

We now have a lot of loose ends to tie, thanks to the updates introduced by the paired accumulator. All of these, except for the first, simply require the variable we need to be identified with the variable from which the update says it should be derived. The exception to this is because this applies to the case where we have applied an operator and need to add it to the set of those which we are accumulating. The instantiations are:

• is instantiated to
• is instantiated to
• is instantiated to
• is instantiated to
• is instantiated to
• is instantiated to
• is instantiated to

The fifth, and last, argument contains the support tree which is built to record of how the conjunction in the first argument was satisfied. For this we use a single argument accumulator by applying the addition (defined in Chapter 6 of the book):

Finally, we make the instantiations:

• About this document ...