Subsections

• Refinement Operators
• Using Refinement Operators

Refinement

We saw in Section 2 how MIS goes about specialising a theory that is too general; the counterpart problem of generalising a theory that is too specific is carried out with the use of a refinement operator.

The following inputs are required:

• A theory $T$ that fails to prove a positive observation $O^{+}$. We say that $T$ is too-specific; it is incomplete relative to the concept the oracle has in mind.

• An oracle capable of answering queries about the truth of ground atoms in the model $M$.

• A set of marked clauses that the backtracing algorithm has previously deemed too general to describe $M$.

• A refinement operator, that, when applied to a marked clause, yields a logically weaker (i.e. more specific) clause.

  It should be noted that, even though the new candidate clause is less general than the previously-considered one, adding it does not decrease the number of facts entailed by the current theory. (It may not actually increase it, though.) So, the new conjecture should be considered a generalisation of the previous one.

Shapiro's generalisation algorithm is parameterised by both the refinement operator and the strategy that makes use of it. We deal with each in the following sections.

Refinement Operators

A refinement operator $\rho$ suggests a logically weaker plausible replacement to a hypothesis refuted by the diagnosis algorithm outlined in Section 2. Formally, $q$ is a refinement of $p$ if it satisfies the following two criteria:

1. $p \vdash q$, i.e. everything provable from $q$ is provable from $p$, or equivalently, $p$ is at least as general as $q$.

2. $size(p) < size(q)$ under some size metric. In logic programming terms, Shapiro uses the following:

   The $size$ of a sentence $p$, $size(p)$, is the number of symbol occurrences in $p$ (excluding punctuation symbols) minus the number of distinct variables occurring in $p$.

   Intuitively, building a monotonic size increase into the notion of refinement means that all refinements of $p$ are more specific/weaker than $p$, as it requires more things to be provable (in the case of adding a body goal) or more structure to be present in the query (if a function symbol is introduced, or two or more variables are unified). This exploits the intimate relationship between the syntax and semantics of logic programs.

A refinement operator $\rho$ is then defined to be a set-valued function that maps a statement $p$ to a subset of its refinements, with some technical side-conditions.

A function satisfying this definition induces a partial order (where ``larger'' is interpreted to mean more-specific) over the statements of the language $L$, and can be visualised as a directed acyclic graph (generally termed a Hasse diagram in the context of partial orders). If all statements in $L$ appear in the graph at some point, and are transitively reachable from the most-general clause $\Box$, then the refinement operator is termed complete for the language $L$.

Shapiro proves the existence of a refinement operator complete for any first order language in [Sha81]. This property in itself is not particularly desirable, however, as it leads to inefficient induction of theories due to the exponential explosion of the size of the refinement graph. It is more interesting to define refinement operators that work on subsets of $L$ that are more likely to contain satisfactory theories, as this is the only way the search is going to be tractable.

One class of interesting logic programs that can be enumerated via a refinement operator in practice is the that of the definite clause grammars. Using such an operator, it is possible to learn the syntax of simple programming languages.

The refinement operator used in Section 4 is defined as follows: Let $PSyms$ be the set of predicate symbols in $L_h$, $FSyms$ the function symbols; then $q \in \rho(p)$ iff $q$ is a modification of $p$ in precisely one of the following ways:

1. Let $U, V$ be distinct variables in $p$; unify them in $q$ (i.e. $q = p\{U/V\}$, read as ``substitute $V$ for $U$ in $p$'').

2. Let $f/n \in FSyms$ and $U$ be a variable in $p$; let $q = p \{U/f(A_1, ..., A_n)\}$ where the $A_i$ are new variables.

3. Let $g/n \in PSyms$, $A_i$ distinct variables in $p$ and $p = h :- b_1, ..., b_m$; let $q = h :- b_1, ..., b_m, g(A_1, ..., A_n)$.

See Section 4.1 for a discussion of some of the pragmatic issues of defining a useful refinement operator.

Figures 3 and 4 show how the two clauses for the add/3 relation can be derived using these rules. Note that in practice there will probably be several other clauses included in the theory, such as the symmetric base case add(B, z, B).

Figure 3: The success path through the refinement DAG for the base clause of add/3.

Figure 4: The success path through the refinement DAG for the recursive clause of add/3.

Using Refinement Operators

In essence, the bug-correction algorithm employed by MIS is little more than a search through an enumeration of all clauses in $L_h$. Given the intractability of this search in general, the given refinement operator $\rho$ is used to bias the enumeration towards clauses that are more likely to be correct.

The search itself is general-to-specific, starting with the empty theory $\Box$. The advantage of this strategy over a specific-to-general one is that there is a simple starting point; for the latter the initial theory would have to contain - notionally, at least - all ground statements in $L_h$. This set will be infinite if there is at least one function symbol with an arity of one or more in the language (which will be the case in all interesting domains), and so is difficult to represent on a physical machine.

As $\rho$ induces a partial (and not total) order on $L_h$, three sets need to be maintained:

• The theory set contains all clauses that have been examined and found to be consistent with the facts.

• The marked set contains all clauses that have been flagged by the contradiction backtracing algorithm as the culprits for the proof of a negative observation, and have yet to be refined.

• The dead set contains all marked clauses that have been refined.

The search itself is straightfoward: select the next marked clause, add it's refinements to the theory and move it to the dead set. Note that the ordering of the marked set must be fair, for otherwise the algorithm may get stuck examining an infinite path that does not contain useful clauses. This is analogous to a Prolog proof attempt failing to terminate even though the query logically follows from the program, due to it's incomplete depth-first-search strategy.

In the context of Figure 1, searching the refinement DAG is purely a generalisation step; the consistency of the resulting theory with the facts is established by the framework itself.