Extending Reflective Architectures

I. Introduction

Primarily, the interest in reflective architectures has fo­ cused on addressing the problem of search-intensive in­ ference symptomatic of general knowledge-based sys­ tems. The basic approach has been to have the con­ trol component included alongside general inference: (i) generate secondary inferences to select among the best c?~rses availa~le to general inference, or (ii) apply sub­ stdtary deduct10n rules to replace inferences that would ?therw.ise have to be performed directly. The design ts. constdere~ 'r.eflective' (or 'introspective') since it pro­ vtdes for a hrmted form of self-directed reasoning. Ex­ ample~ of systems proposed along these lines may be fo~nd m [Bowen and Kowalski 1982], [Davis 1980], [Gal­ latre and Lasserre 1982), [Genesereth and Smith 1983], [Kramer 1984], and [Weyhrauch 1980).

A clearer picture of the concept of reflection in knowledge-based systems can be obtained by consider­ ing how control information is to be expressed. The idea as described in [Smith 1986], is to express 'properties of control' in the same way as 'properties of a domain', but to employ a separate knowledge-base (KB) for this pur­ pose. One immediate advantage is that control informa­ tion .is not tied directly to any set of domain properties, and 1s therefore free to interact in solving different prob­ lems. A second advantage is that by representing control in terms of a knowledge-base, large-scale changes such as those involved in re-programming an implement~tion , do not have to be made each time new control properties are introduced.

1 Financial assistance for this work was gratefully received from the School of Graduate Studies, and the Department of Computer Science, University of Toronto.

So far, combining reflection with pure declarative lan­ guages such as full first-order logic has run into several proble!fls. !he first is that, to be effective, secondary (or reflective) mference must be more constrained, less de­ pendent on search, than the general inference processes over which it is to exercise control. However it is not immediately apparent how to satisfy the dema~ds of hav­ ing a flexible control component, constraining reflective inference, and keeping the system deductively complete. The second problem centers on a pragmatic issue involv­ ing the relative ease with which control constructs can be e:cpressed for a g.iven representational language. In particular, an effective notion of control seems to de­ pend heavily on the syntatic form of the sentences over which they operate. For example, consider the following definition of Ancestor:

Vx, z Ancestor(x, z) = Parent(x, z) v 3y Ancestor(x, y) 1\ Parent(y, z).

To che.ck if. x is an ancestor z, a good strategy is to first check If x IS a parent of z, and if not, to find a y such that y is a parent of z. (Informally, the corresponds to traversing up the family tree.) However, representing the same sentence as a set of clauses,

-,Ancestor(x, z) V Parent(x, z) v Ancestor(f(x, z), z) Ancestor( x, z) V ...,parent( x, z)

Parent(f(x, z), z) -,Ancestor(x, y) -,Parent(y, z),

it is not longer straightforward how the same control strategy can be used. Additionally, there is the problem of how to logically organize sets of clauses so that it is possible to recognize at what point particular strategies may be applied.

The object of this paper is to describe a reflective ar­ chitecture for declarative languages, and show how it leads to a notion of selective inference for KB-systems based on first-order logic. The purpose of presenting a general architecture is to provide an account of the knowledge available to reflective (or non-reflective) in­ ference, i.e. to make precise the representational proper­ ties of these architectures which is independent of par­ ticular languages, or ideas on process and control. The design of a reflective system for first-order logic, fol­ lowing in Section III, is considered an instance of this general .architecture. The main part of the paper fo­ cuses on how a procedural correspondence between re­ flective and non-reflective inference can be obtained, lay­ ing the groundwork for two kinds of control, introduced in Section IV. Points in the design incorporate aspects of Smith's model of procedural reflection ([1982]), in con­ junction with Murray's rule of NC- (Non-Clausal) Res­ olution ([1982]).

II. The Model

A. Theories, Meta-theories

A logic L can be described as a 2-tuple < L, Cn >,where L is a language, and Cn a consequence operator. That is, Cn is a mapping of P(L) (the power set of L) into itself, which satisfies, for all X, Y ~ L,

(ii) Cn(X) ~ Cn(Y), whenever X ~ Y.

The model is based on the relationship between a the­ ory and a meta-theory. Informally, a theory denotes a collection of statements about some domain, while a meta-theory denotes a collection of statements about a theory. Formally, by a 'theory' it is meant any set A ~ L closed under Cn; that is, A = Cn(A), or equivalently, A= Cn(B), for some B ~ L. Note that Cn(B) denotes the set of all logical consequences that follow from the statements (premises) in B.

The ability of a meta-theory to refer explicitly to parts of a theory is carried out by way of a naming relation between linguistic entities in the object-language, used to express the theory, and terms in the meta-language, used to express the meta-theory. For example, suppose P(x) is a formula of L. Designating L as the object-language, this formula might be represented in a meta-language L' as

where peons, ~redsym, and varsym are functions in L', and r P1 and x 1 are constants in L' used to designate P and x in L. Without defining such as relation here, in general r E1 will be used to denote the meta-language representation of the object-language expression, or set of expressions, given by E.

Multiple theories are often useful for maintaining sets of statements about more than one domain, or for hav­ ing different aspects of the same domain organized into separate contexts. In the model, multiple theories are expressed as distinct sets of premises to a logic La = < La, Cna >. Thus, an arbitrary set of theories has the form Cna(KBa), ... , Cna(KBn), where KBa, ... , KBn denote sets of premises in La. Therefore, all theories are expressed in the same language and closed under the same consequence operation. Note that Cna(0) (where '0' refers to the empty set) denotes exactly the set of sentences valid across all theories expressible by La.

The advantage of this approach is that it allows a single logic Lt =< Lt, Cnt > to express the meta­ theories for any of these theories. A set of meta­ theories has the form Cnt(mKBa), ... , Cn1(mKBp), where mKBa, ... , mKBp denote sets of premises in the meta-language Lt. In this way, a single meta-theory can be associated with an arbitrary set of theories, or alter­ natively, an arbitrary set of meta-theories can be associ­ ated with any theory.

Also incorporated into the model is a reflection prin­ ciple ([Feferman 1962]), which establishes a correspon­ dence between a theory and any of its meta-theories. The property defined is one of provability: in general, for L =< L, Cn >, let A 1-L a hold iff a E Cn(A), where A~ Land a E L. Then,

where ,81 ( · , ·) is a fixed 2-place expression of L1 (with 'holes' for Lt terms), .81(fKBk1,fa1) is a formula of L 1, and fKB k 1 and r a 1 are meta-language expres­ sions denoting KBk and a in La, respectively. Thus, ',B1(fKBk1,fa1)' might be read as 'a is a logical conse­ quence of KBk in <La, Cna >'.

It follows from the definition that provability is the same across all meta-theories by virtue of the fact that Cn1(0) ~ Cn1(mKBk), for all mKBk ~ L1. In par­ ticular, any meta-theory Cn1(mKBk) can be viewed as arising from a set of 'axioms of provability' AP1 ~ L1 such that Cn1(mKBk) = Cn~(mKBk U APt), for some consequence operator Cn~.

B. The Tower

By definition, any meta-theory is itself a theory, so that hypothetically this theory can be provided with its own meta-theory- and so on, ad infinitum. In its full general­ ity, therefore, the model is presented in terms of a 'tower' of logics L;, i E .AI, such that La expresses all domain theories, and Lk+1 expresses all of the meta-theories for Lk, k E .AI. At each level of the tower, an arbitrary set of theories is supported, given by sets of premises (i.e. KBs). A generalized reflection principle can be stated as follows: for i E .AI,

where ,Bi+1 ( · , ·) is a fixed 2-place expression of Li+1 (with 'holes' for Li+1 terms), ,8;+1(rKBk1,fa1) is a for­ mula of L;+l, and fKBk 1 and fa1 are meta-language ex­ pressions denoting KBk and a in L;, respectively.

Note that no constraints have been given regarding what kinds of logics instantiate a tower, e.g. proposi­ tional, first-order, intuitionistic, etc., or even combina­ tions of these, as long as any particular combination sat­ isfies the reflection principle.

C. The Tower Interface

Two operations are defined for each level of the tower. In this case, the focus is on a computational setting. The idea is to view each level of the tower as comprised of a set of knowledge-bases (KBs) which a user can interact with independently.

If the intention is to use the architecture to perform inference, the logics L;, i E .A!, must be those where the rules of inference defining the consequence operations Cn; are recursively enumerable. This ensures that the theorems of any logic of the tower can be generated com­ putationally. The two tower operations are analogues of those presented in [Levesque 1984]. Specifically, they allow a user to tell a new statement to a knowledge­ base, and to ask if a statement is a logical consequence ofthose contained in a knowledge-base. In the following, let k, n E .A!. Then,

The operation meta-TELL[ n ](KBn,k, o:) takes KBn,k C Ln, i.e. the kth KB at the nth level of the tower, and returns KBn,k with o: included as a premise.

The operation meta-ASK[n](KBn,k, o:) takes KBn ,k ~ Ln, i.e. the kth KB at the nth level of the tower, and returns yes or no, depending on whether o: is provable or not provable from KBn ,k in Ln, respectively. 2

III. The First-Order Example

A. Inference and Procedural Reflection

The next problem to be discussed is where inference can be said to originate in the model, and how it is per­ formed. By way of example, these issues are addressed for a tower based on first-order logic. As a starting guess, one can imagine taking a given tower and pairing each level with a 'black box', which would carry out all of the reasoning required for that level. However, the original motivation in this area was that sentences expressed as part of a meta-theory should be able to guide inference with respect to a theory, but so far no procedural con­ nection between levels has been made.

To establish this connection, an approach described by Smith [1982] is considered, called procedural reflection. The main ideas of this approach may be summarized as follows . In procedural reflection, a processor for a lan­ guage is not regarded as a 'black box', but is instead definable in terms of a program which describes it. All programs, therefore, are considered to be executed indi­ rectly, by virtue of executing a program that represents the processor. A processor written in the same language it has been designed to implement is called meta-circular: 'meta', because of the property that the processor oper­ ates on formal program fragments, and 'circular', be­ cause an MCP does not, in itself, constitute a definition of the language.

2 0nly logics where the relation f- is recursive are guaran­ teed to return an answers to arbitrary ask operations. Where 1- is r.e., but not recursive, answers are in general returned only in the case of a yes.

The incentive for viewing computation in terms of a tower of MCPs is that it allows reflective procedures, written in the same language as the original program, to be included as part of the environment which executes the program. Hence, by changing the general description of the processor at level k + 1, for k ~ 0, the underly­ ing program situated at level k can give rise to different processes. For present concerns, the analogous idea is to axiomitize the proof procedure found in the 'black box' at level k (used to carry out inference at level k) as part of the axioms of provability APk+l expressed by Lk+l· In fact, the idea is to axiomitize the proof proce­ dure in such a way that the axioms themselves can be interpreted procedurally. Hence, inference performed on one level of the tower is viewed as being implemented by the level above. As with procedural reflection, where re­ flective procedures can be written to augment an MCP, this approach will allow sentences expressed in a meta­ theory to determine how inference proceeds with respect to a theory.

The ideas outlined above appear in various forms for several Horn-Clause systems ([Bowen and Kowal­ ski 1982], [Gallaire and Lasserre 1982], [Davis 1980], [Kramer 1985]). The novelty of this approach is the step up to full first-order logic; of particular interest is the fact that negation can be explicitly represented. This is important for control, since negation allows testing for properties that do not hold. It therefore becomes pos­ sible to block unwanted properties from entering into a resolution process. Also important is that resolution in the system presented is non-clausal. Therefore, the sen­ tences used to define the MCP, express control strategies, as well as express the original theories over which these operate, can maintain much of their original form usu­ ally lost when everything must be reduced into clausal form.

B. A First-Order MCP

The (full) first-order MCP to be described is based upon the rule ofN on-Clausal Resolution ([Murray 1982]) . Like its clausal counterpart ([Robinson 1962]) , NC-Resolution is a rule of refutation: given a set A ~ L and a sentence o: E L, if {AU -,o:} leads to a contradiction 'F' (false­ hood), then o: is said to follow from A. However, while clausal resolution resolves on unifiable, complimentary literals between clauses, NC-Resolution resolves on gen­ eral, quantifier-free formulas containing unifiable atoms of opposite polarity. An important property of NC­ Resolution, therefore, is that sets of formulas do not have to be converted into conjunctive normal form (although skolemization is still necessary); the standard connec­ tives (A, V, :::>, =:, ...,) are all available for resolution.

The first step in the design of the MCP is the selection of a proof procedure. The one adopted combines NC-Resolution in a connection graph format. One of the attractive features of these graphs, from the point of view of obtaining an MCP, is that they provide a convenient way of organizing the sentences of a theory. Informally, a set of well-formed formulas S can be represented as a connection graph < V, E >, where each vertex v; E V denotes one of the formulas s; E S, and each edge lk E E, joining a pair of vertices in V, represents a potential re­ solvent. The connection graph refinement to Robinson's resolution principle was introduced by Kowalski (1975]. Each vertex, therefore, denotes a formula in clausal form, and edges occur between those vertices containing unifi­ able, complimentary literals. The combination of NC­ and Connection Graph Resolution is described in (Stickel 1982]. In this case, V denotes a set of quantifier-free for­ mulas, and E is a set of edges joining vertices of V that contain unifiable atoms of opposite polarity.

A resolution step in < V, E > consists of selecting one of the edges lk E E, and forming the resolvent ncr asso­ ciated with the ends of lk. A new graph < V', E' > is then constructed by adjoining ncr to V, and by including among E the set of edges which ncr is said to 'inherit' from its two parent vertices. 3 It should be noted that there is no a priori constraints on how edges should be selected to obtain a proof, only that they should be se­ lected such that the completeness of the rule is preserved.

The previous discussion can be summarized in the form of two meta-language definitions, considered as a partial specification of the MCP: 4

• (i) VV,E,o: (provable(V,E,o:) = (3V', E', o:' ( skolem( not( o:), o:') A initialize-graph(V, E, o:', V', E') A cg-resolve(V', E'))))
• (ii) V l-', E ( cg-resolve(V, E) = icon(V) V (3/, ncr, V', E' ( select-edge(V, E, /) A nc-resolve(l, ncr) A inherit-node( ncr, V, V') A inherit-edges(/, ncr, E, E') A cg-resolve(V', E')))).

Note that provable defines the overall proof proce­ dure: by way of separate definitions, skolem and initialize-graph describe the addition of the skolemized form of ...,o: to the graph < V, E > leading to the extended graph < V', E' >. Next, cg-resolve defines the steps involved in a deduction. The definition of select-edge represents the selection of an edge I from the set of edges · E. With respect to nc-resolve, the term ncr denotes the NC-resolvent created by resolving on the atoms associated with the ends of I. The inclusion of ncr as a new vertex of the graph (mapping V to V') is represented by inherit-node, while the corresponding op­ eration for new edges (mapping E to E') is represented by inherit-edges. Testing for a contradiction is repre­ sented by icon, which looks for 'F' among the vertices of v.

3 A property of edge inheritance is that the edge lk used to form the resolvent at each step is removed from the graph. However, since the interest in connection graphs is on the data structure they provide, rather than on defining a new rule of inference, this particular aspect is ignored.

4 Note that quantifiers have been included for readability.

All further definitions required in order to give a com­ plete specification of the MCP follow as sub-definitions of either provable or cg-resolve. All MCP sub-definitions are considered to be defined in an analogous way to those given above, e.g. V o:, o:' ( skolem( o:, o:') _ ... ) or

C. Execution

The remaining question is how NC-Resolution on the MCP simulates the proof procedure. The approach uses a procedural interpretation on formulas and a form of parameter-passing similar to that found in many Horn­ clause systems. That is, literals of an MCP definition are refuted in a left-to-right order, with ground terms instantiated for variables at each step. Some subtlety is involved, however, since the specialized form of reason­ ing is used only with respect to copies of the MCP; to ensure completeness, general first-order theories must be treated more generally.

To illustrate, an NC-Resolution process associated with the MCP is initiated by a resolution step on an atomic sentence of the form:

where rv1, fE1, and fo:1 are (ground) meta-language terms which designate a set of vertices V, a set of edges E, and an object-language formula o:. This sen­ tence might be said to correspond to the initial 'state' of the process, with successive resolvents correspond­ ing to successive states. The only major rule for per­ forming resolution steps is that successive resolvents (i.e. states) are always created by resolving the left-most lit­ eral of the current state against its corresponding MCP definition. Therefore, the first resolution step consists of resolving ..,provable(rv1, r E1, fo: 1) against its defini­ tion in (i). Instantiation by a most general unifier { rv1 IV, r E1 IE, fo: 1 I 0:} leads to the NC-resolvent (and next state):

The result of the next series of resolution steps is the 'binding' of o:' to fo:'1, the term designating the formula( s) representing the skolemized form of -,o: . This series is initiated by resolving ..,skolem(not(fo:1), o:') against its associated MCP definition. Once all states have been passed through to introduce and resolve away all of the atoms associated with the definition of skolem, the next intermediate state reached is

Another series of resolution steps then results in an in­ stantiation of rv'1 for V' and fE'1 for E', representing the addition of the skolemized form of -,a: to < V, E >.

The single remaining literal,

indicates the start of the deductive process on the graph < V' E' >. With respect to the MCP, this process is initiated by a resolution step between this literal and its definition in ( ii).

The procedural interpretation placed on the MCP def­ initions corresponds to a form of depth-first search, so a question of completeness arises. In particular, it must be possible for the MCP to intera:t in a complete w.ay with general object-language theones. Search strategies expressed by the MCP are found as part of the definition of select-edge, a sub-definition of cg-resolve. Note that E might be regarded in terms of an ordere~ list .o~ sched­ ule: selecting the first element of E, and mhentmg ne.w edges by mapping them onto the front of E, results m depth-first search (DFS). Similarly, keeping inheritance the same, and selecting edges from the back of E, results in breath-first search (BFS).

In the full tower, each logic L;+l, i ~ 0, expresses the provability axioms AP;+l by a copy of the MCP. Now, the kind of search strategy expressed by the MCP found at a particular level depends on whether resolution is associated with some general theory, or a theory repre­ senting another copy of the MCP. By default, all ge~­ eral theories are expressed by L 0 , and completeness IS maintained for them by having the version of select-edge included in LI satisfy the general strategy of BFS. For the rest of the tower LA:, k > 1, which by default operate on other copies of the MCP, select-edge in LA: satisfies a special form of DFS (corresponding to the proof proce­ dure).

IV. Advancing Control

In this final section, a cursory overview is presented on two extensions to first-order reflective tower outlined in §III to allow more specialized forms of control. For a more complete description, the reader is referred to [Lownie 1990].

A. Control Strategies

Edge schedules are often useful for implementing general domain-independent control strategies such as depth­ first and breadth-first search. However, trying to design more complicated domain-dependent strategies based exclusively on ordering edges in a schedule can be dif­ ficult . A more structured approach is to allow control strategies, expressed for a copy of the MCP as part of select-edge(V, E, 1), to index the edges of a graph < V, E > through its set of vertices V. A~cor.di~gly, the vertices v; E V act in the role of 'goals withm a deduction, while the atoms ak E v; act in the role of 'sub-goals'. Note that an edge IE E can be described in terms of a 5-tuple:

where a0 and ai occur with opposite polarity in Vo and VI, respectively, and mgu is a most general unifier that unifies them. A new selection policy, therefore, can be based on indexing through the components of an edge as follows:

• select (in order) a combination of
• (i) a goal Vi E V, a sub-goal a1e E Vi, .
• (ii) an edge l E E incident on v; , a1e .

Of course, other ways of indexing edges are possible, e.g. selecting two goals followed by two sub-goals. A~­ ditionally, other structures can be used to extend this approach; for example, (i) a 'mini-scheduler' I, to allow control information to be communicated between resolu­ tion steps, e.g. in the form of complete edges or various components of edges, and (ii) a 'history' H, providing a record of the resolution steps performed, and used, for example, to implement selective backtracking, or to pur­ sue multiple lines of reasoning.

B. Subsidiary Deduction Rules

A subsidiary deduction rule can be described as a prop­ erty of the meta-theory in the role of an inference rule. For example, [Stickel 1986] presents a general (sound) deductive principle called theory resolution which can be used to test for inconsistency among selected sets of clauses or literals. Theory resolution allows specialized procedures to be included alongside general resolution to perform, for example, taxonomic reasoning or reasoning with partial-orders.

It is possible to express subsidiary deduction rules in the style set down for cg-resolve. Each subsidiary rule, therefore, comes equipped with its own set of edges (also extendible by a mini-scheduler and history) for express­ ing its own individual control strategies. All rules asso­ ciated with a particular meta-theory (mKB), however, share the same set of vertices. Let sdro, .. . , sdrp denote a set of (p + 1) subsidiary deduction rules contained in KB1e of the logic Ln (n > 1), for n, k,p EN' .. Then sdr; , 0 ~ i ~ p, may be defined as follows:

To each object-language inference there corresponds the particular rule selected to perform it . Since any language L;, i E N', can be isolated in terms of ~n object-language, this view naturally extends upward m the tower. To select and apply rules requires that a meta-language description of them be made available to the processor. A rule sequence RS has the form: [ rvl 2 1 cgr 1 rs0 1 .... 1 rsp ], where each element cgr or rs; is itself a 2-tuple: (0 ~ i ~ p)

The first element of each 2-tuple designates the name of the rule, while the second element refers to its set of edges. (Note that rvl 2 refers to two levels of designation above V; similarly for r E; 12 .)

With cg-resolve no longer the only rule available to a resolution process, it is no longer tied directly into the definition of the MCP:

Briefly, select-role represents the selectionS of one of the 2-tuples [ r cg-resolve1 I r Ecgr 1 2 ] or [ r sdr; 1 I r £; 1 2 ] from RS, while cg-apply represents a single application of the selected rule, which results (in part) in the formation of a new rule sequence RS' given by either

Copies of mcp2+ are included into the tower by ap­ pending its definition as part of AP;, for i ~ 2. In terms of upward compatibility in the tower, it is pos­ sible to view mcp 2 + as a rule which can be selected and applied like any other. Further consideration in this area involves: (i) a precise description how rules can be ap­ plied; (ii) 'cross inheritance', by which new edges for a rule are generated as a result of resolvents created by other rules; and (iii) an updated definition of provable which takes into account the the addition of copies of mcp 2 +. The details, while lengthy, are mostly straight­ forward ([Lownie 1990]).

V. Summary

This paper outlined a reflective architecture for declara­ tive languages, which includes Smith's procedural model ([1982]) as a special case for first-order languages based on Murray's NC-Resolution rule ([1982]). Its main con­ tribution over existing approaches is how this leads to various forms of selective control for KB-systems based on (full) first-order logic.

Several other topics warrant further consideration; for example, implementations which minimize compu­ tational overhead incurred by reflective inference by ex­ plicitly representing only those parts of the processor required for control. These are left to the later paper ([Lownie 1990]). However, a good reference which can found in this area is [des Rivieres and Smith 1984].

Acknowledgments

The author would like to thank, at the University of Toronto, Hector Levesque, Jim des Rivieres, Ray Reiter, and John Mylopoulos, and at Queen's University, Peter O'Hearn, for their comments and suggestions regarding earlier drafts of this work.