Reflective Reasoning with and between a Declarative Metatheory and the Implementation Code

1 Introduction

Reflective and metatheoretic reasoning are well known techniques applied in knowledge representation and au­ tomated deduction (see for instance [Bundy, 1988], [Con­ stable et al., 1986], [Bowen and Kowalski, 1982], [Smith, 1983], [Gordon et al., 1979]). Roughly speaking, in the past, metareasoning has been performed according to two different paradigms. In the first, from now on called procedural, the metalevel consists of a programming language and metareasoning is performed by computa­ tion in it. One example in AI is [Smith, 1983], an­ other in theorem proving is LCF and its metalanguage ML [Gordon et al., 1979]. In LCF the user can write control strategies as programs (usually called tactics) in ML to guide the search for a proof of a theorem. In the second paradigm, from now on called declarative, the metalevel is a logical metatheory and metareason­ ing is performed by deduction on metalevel statements. One example in AI is [Weyhrauch, 1980], one in theorem proving is [Howe, 1988]. Both approaches are sometimes incorporated and alternatively used; thus, for instance, in NuPrl [Constable et al., 1986] and Isabelle [Paulson, 1989] both ML and a declarative logical metatheory can be used to build derived inference rules. In logic pro.. gramming, metainterpreters [Bowen and Kowalski, 1982] can be seen both procedurally and declaratively.

In this paper, we present a system (called GETFOL 1 ) with both a procedural and a declarative metalevel. In this respect GETFOL is similar to NuPrl and Isabelle; on the other hand GETFOL has features which make it very different from any other system proposed so far:

(1) the metalevel programming language is the same as the underlying implementation language and the code implementing the object logic has been written to be its procedural metalevel.

(2) the logical declarative metatheory MT can be put in a one-to..one relation with the code and automatically generated from it (and viceversa).

1. MT is correct and complete in the sense that, for any object level deduction (performed by running the code implementing the object level logic), the wff repre­ senting it is a theorem of MT 2 · Such theorems, possibly proved automatically by metatheoretic theorem proving, can be "mapped back" into the underlying code as new reasoning modules . These modules, if executed, will pro.. duce the proof represented by the theorem they have been translated from.

As a consequence of these three facts, it is possible to generate (parts of) MT automatically from the imple­ mentation language, to prove in MT "certain" theorems and then to "transform" them into new code. The result is an extension or, possibly, a modification of the system itself. The GETFOL underlying code is not a "black box", fixed once and for all at the time of the development, but can change over time. This seems a first step towards "really" self-reflective systems, ie. systems able to rea­ son deductively about and thus, possibly, modify, their underlying reasoning strategies. As a side effect of this "reflective" relation existing between computation and deduction, the usual logical reflection rules (reflection up and reflection down) [Giunchiglia and Smaill, 1989] can be proved to be (a form of) derived inference rules.

1 GETFOL is a reimplementation/ extension of the FOL sys­ tem [Weyhrauch, 1980]. GETFOL has, with minor variations, all the functionalities of FOL plus extensions, some of which described here, to allow metatheoretic theorem proving.

2 The notions of correctness and completeness here in­ volved are sometimes called adequacy and faithfulness, respectively.

The paper is structured as follows. Section 2 describes how the implementation has been constructed to behave as the procedural metalevel of the system. Section 3 de­ scribes MT and how it can be automatically generated from the implementation code. In section 4, it is proved that MT represents all the object level deductions and that deduction in MT is the analogous operation of writ­ ing tactics in the implementation language. This is the fundamental property that allows the interpretation of theorems of MT in terms of the underlying code (sec­ tion 5) via the use of reflection up and down. Finally, section 6 gives some conclusions and a short discussion of the related work.

2 The system code as the procedural metalevel

GETFOL allows the definition of multiple distinct the­ ories. Each theory is formally defined as a triple (Language, Axioms, Set of inference rules}. To simplify things we consider here the case where we have only one object theory OT=(.C,.Az, 'R.} and one metatheory MT=(M.C, M.Az, 'R.} (see figure 1). MT and OT use a first order classical sequent logic. By sequent we mean here a pair (r,A), written also r 1- A, where A is a formula and r a set of formulas . For simplicity, in this paper we suppose MT and OT use the same set of in­ ference rules 'R.. The inference rules, which are a se­ quent version of Prawitz' natural deduction (ND) cal­ culus [Weyhrauch, 1980], allow introduction and elim­ ination only in the post-sequent A. In the following, to simplify notation, when not relevant, we write A for r 1- A. Thus, for instance

are respectively one of the two conjunction elimina­ tion rules (AE) and the universal quantifier introduction and elimination rules ('v' I ,'v' E). The functions in the un­ derlying GETFOL code implementing these inference rules are given in figure 2. Thus, for instance, when applica... ble, (alli-fun A(z2) Zt z2) returns 'v'ztA(zt) which is then added (by proof-add-theorem) to the current proof. Notice that, even if the underlying code has been written to treat errors ( eg. the application of (AE) to a disjunction), this issue is not dealt with in this paper.

Strategies and derived inference rules can be defined in a metalevel functional language, GET, which is a subset of the implementation language of GETFOL. To preserve correctness, the development environment is such that the user can write tactics which fail but that never assert a non-theorem. For instance, considering the code in figure 2, proof-add-theorem, ande-fun, alli-fun and alle-fun are not available to the user. In this respect, GET is similar to ML as used in LCF, Nuprl or Isabelle. For instance, the GET code implementing the (simple) derived inference rule that corresponds to the deduction

is:

Strategies can be defined by using conditionals and iterations:

where FORALL and COIJ are built-in GETFOL predi­ cates which evaluate to TRUE when their argument is, respectively, a universally quantified formula and a con­ junction, (repeat ·tactic args) iterates the applica... tion of tactic over args as many times as possible. strategy! can be described as: "if x1 is a universally quantified conjunction, then derive the first conjunct of x1, otherwise exhaustively apply tactic2", where tactic2 is a previously defined tactic.

What has been described so far suggests that GET can be used as the procedural metalevel of GETFOL, analo­ gously to what happens with ML in LCF, NuPrl or Is­ abelle, or even with metainterpreters in Prolog. This is, in fact, the case when writing tactics. The differ­ ence comes from the fact that (exploiting that GET is also GETFOL's implementation language), the built-in GET functions to perform logic inference are exactly those used to implement the basic inference rules, eg. those in figure 2. More generally, all the GETFOL code has been carefully written to allow the identification of the proceduml metalanguage with the implementation lan­ guage. Thus, for instance, the implementation provides GET with all the syntax manipulation routines (such as FORALL, COllJ, ande), with all the proof manipulation routines (such as IS-A-THEOREM), with all the theory ma­ nipulation routines and so on. Not only must the code produce extensionally the right behaviour (satisfying the usual correctness criteria), but it must also be written to be at the same time the procedural meta/eve/ of the logic it implements. In other words, it must have the right function and predicate symbols, the internal structure of the function and predicate definitions must be such that they can be put in a one-to-one relation with the axioms describing their behavior (all of this is described in section 3), and far harder, it must be such that com­ putation can be directly mapped into the metathereotic "representation" of the deduction it produces (described in section 4).

We call the production of code satisfying the require­ ments above, "the mechanization of the logic" (to dis­ tinguish it from the process of producing an implemen­ tation of the logic). Mechanizing a logic is far harder than implementing it. On the other hand, as the rest of the paper will show, the mechanization of the logic can be exploited to build really self-reflective systems, ie. systems able to reason deductively about and modify their computation mechanisms. In fact it becomes then possible to generate automatically a logical metatheory MT from the code and, viceversa, to compile certain theorems of MT as system implementation code. Mod­ ification of the system's underlying computation mech­ anism is achieved by re-writing already existing (parts of) procedures. Note that this is not done in any of the existing theorem provers or metainterpreters. From this perspective, the work which most closely resembles ours is Brian Smith's [Smith, 1983]. The fundamental difference is that our metalanguage is a logical metathe­ ory; this allows us to generate provably correct computa­ tion procedures automatically by metatheoretic theorem proving.

3 The declarative metatheory MT

MT's set of inference rules is fixed, being 'R. We need to define MT's language MC and axioms MAx . MC, has names for the elements of OT (axioms and assumptions s, formulas w, variables x and so on); this is achieved by having for any such element an individual constant ("s", "ul', "x" and so on) as part of MC. These constants are the "quotation mark names" [Giunchiglia and Traverso, 1990] of the objects of OT.

[ (DEFUM <fun> (11 . . . In) <body>] · V [11] ... V [In] ( [<body>]) [(IF <tl> THEN <t2>)] · [<t1>] -+ [<t2>] [(IF <t1> THEN <t2> ELSE <t3>)] · if [ <t1>] then [ <t2>] else [ <t3>] [(AND <t1> <t2>)] · [<t1>] 1\ [<t2>] [(IS-A-THEOREM <t>)] · T([<t>]) [ (proof-add-theorea <t>)] · T ( [ <t>]) [(CONJ 11)] · Conj([11]) [ (FORALL 11)] · Forall ( [11]) [(NO-FREE 11 X2)] · NoFree([X1],[X2]) [(IS-VAR 11)] · Var([11]) [(IS-TERM 11)] · Term([X1]) [(ande-fun X1)] · ande([X1]) [(alli-fun 11 X2 X3)] · alli([X1], [12], [X3]) [(alle-fun 11 X2 X3)] · alle([X1],[X2],[X3]) [11] · Xt [In] · Xn where functions and predicates in M£ (for instance Forall, N oFree, Var, Term, ande, alli, alle and so on) intuitively represent the computational operations per­ formed by the code they are mapped from. The T pred­ icate indicates "theoremhood".

Each inference rule of OT gets ''mapped up" to a distinct axiom of MAx. This mapping, called "mup", performs a one-to-one translation from the code into el­ ements of MT (see figure 3, mup(x) is written as [x]) Thus, for instance, the axioms generated by applying mup to the GET code implementing 1\E, VI and VE (see figure 2) are listed in figure 4. A complete definition of mup and the code over which it can operate is outside the goals of this paper. The important point to notice is the fact that mup (and its inverse) can be implemented to do the translation in either direction automatically.

We can observe in figure 3 that the two GET op­ erations of testing if something is a theorem al­ ready asserted in the object theory (performed by IS-A-THEOREM) and of asserting a proved theorem (per­ formed by proof-add-theorem) are translated into the same metatheoretic predicate r3. This is because OT, as represented in MT, is the minimal set closed under the application of the inference rules to the axioms. There­ fore, because MT is a metatheory of the transitive clo­ sure of OT, the procedural difference between a wff "be­ ing asserted" as a theorem and a wff "to-be asserted" as a theorem is lost.

3 Notice that this seems to contradict our previous state-

The assertion of the axioms generated by mup requires adding function and predicate symbols to M.C: for each inference rule of OT we have a function symbol in M.C with the appropriate arity, for instance ande, alii and aile for 1\E,VI and VE respectively. MC's predicates are Conj, Forall, Nofree, Var, Term and so on.

MT's logic allows the use of the construct if p then t1 else t 2, where pis a wff and t 1 , t 2 are terms. The if construct, very important in order to make the MT's axiomatization mirror very closely the underlying code, is actually not first order. On the other hand it can be easily proved that if can be defined in a conservative extension of classical ND. GETFOL allows the use of the if construct and has an introduction and an elimination inference rule for it.

4 Deduction in MT versus program definition

The goal of this section is to prove that, given a map­ ping between wffs in MT and deductions in OT, for any object level deduction (performed by running the code im­ plementing the object level logic), the corresponding wff is a theorem of the metatheory and viceversa. To do this we need to define how object level proofs are repre­ sented in the metatheory. This is achieved by defining a mapping w from sequent trees II in OT to wffs of MT. Sequent trees are trees of sequents, each labeled by an inference rule. Sequent tree leaves are axioms or as­ sumptions (sequents of the form A 1- A). Sequent trees are not necessarily deductions as the rule labelling a se­ quent may not be applicable. We say that II is a sequent tree of s if s is the endsequent of II. The endsequent is the ''root" of the sequent tree. The formulae mapped from sequent trees are called sequent tree formulas (in short twffs) and are of the form P -+ T(t), where P are the preconditions and t the sequent tree term of the twff. P and t are inductively defined over the complexity of II as follows:

Base: if II= s, then w(II) = T("s");

Step: as examples, let us consider the cases of 1\E and Vle1J. Let w(IIl) = P 1 -+ T(tl) be a twff. If II is a sequent tree built from II1 by adding the rule label 1\E, then w(II) = P1/\Conj(tl)-+ T(ande(t!)) . Ifthe added label is Vle1J, then w(II) = P 1 1\ Var("e") 1\ Var("TJ") 1\ NoFree(t 1, "11")-+ T(alli(t1, "e", "11")).

Notice that there is an isomorphism between twffs and the sequent trees they represent. In particular the se­ quent tree term records the tree of applications of infer­ ence rules while the preconditions record precisely the tests which allow the applications of inference rules.

ment that the mup is one-to-one. In certain cases (T is one of these) mup and its inverse distinguish between occurrences (in this case, corresponding either to IS-A-THEOREM or to proof-add-theorea).

Now we concentrate on showing that MT (which can be proved consistent) has the desired properties 4 :

Theorem 1 (MT correct and complete for OT) : Let II be any sequent tree of s in OT. Lett be the sequent tree term of the twff w(II). Then IMT T(t) <==> II is a proof of s.

Proof [Hinted]: (¢:): corollary of theorems 2 and 3 below.

(=>):similar to the proof of theorem 3. Q.E.D.

Theorem 1, guarantees that, for any provable T(t), there is a proof of a theorem in the object theory and viceversa 5 . As a consequence, given a GET program that succeeds in building an OT proof, theoremhood applied to a term corresponding to the proof itself can be proved in MT. Notice that theorem 1 considers only derived in­ ference rules. This result can be generalized to deal with an extension of MT, expressive enough to represent tac­ tics, written as programs with conditionals, iterations, failure detection and so on. This non-trivial issue, which assures a complete translation of GET into MT and vice v­ ersa is not discussed here.

Theorem 1 does not tell us anything about how to prove T(t), in other words; about how to construct in MT the derived inference rules. A possible technique is suggested by the following two theorems.

Theorem 2 (Twff provability) For any sequent tree formula P-+ T(t), IMT P-+ T(t).

Proof[hinted]: The proof is performed by induction over the complexity of II. As an example of step case, let us consider 1\E. Let us suppose that the induction hypothesis is P -+ T(t). From it we can derive that P 1- T(t) . From the instantiation of axiom (AA£1) in fig­ ure 4 we obtain T(t)/\Conj(t)-+ T(ande(t)), from which we can then derive (also considering the induction hy­ pothesis) P 1- Conj(t)-+ T(ande(t)). For the deduction theorem we derive thus P -+ (Conj(t) -+ T(ande(t))) which is equivalent toP 1\Conj(t) -+ T( ande(t)). Q.E.D.

The proof suggests how twffs can be deduced in the metatheory: basic twffs can be obtained directly as in­ stantiations of the axioms in figure 4; complex twffs can then be composed out of simpler ones following the steps hinted in the proof. This is not the only way to build twffs, [Giunchiglia and Traverso, 1990] describes some examples in detail.

The fact that all the twffs are provable in MT is ex­ actly what we should have expected. In fact, any twff corresponds to a program that can be defined by the user in the system code. To say that any twff can be derived in the metatheory is equivalent to say that any strategy can be written in the code. Derivation of a the­ orem in MT is the analogous operation of writing code in the implementation language. Notice that this suggests a new way to develop tactics: instead of coding them in the procedural metalanguage the user can theorem prove them in MT. The user can thus write the hardest steps and, interactively, generate tactics by theorem proving. This amounts to giving the user the possibility to derive not only the object level proofs but also the tactics (this idea has some resemblance with the work on proof plan­ ning [Bundy, 1988], see [Giunchiglia and Traverso, 1990] for a more in depth discussion) .

'For lack of space, only proof outlines are given.

5 1£ not desiderable, completeness can be easily dropped by generating MT only partially; for instance, we may not have the names of all the objects in OT.

A different matter is whether the strategy is success­ ful. In the programming language, a defined strategy may generate an object level proof or fail. Similarly, the sequent tree may or may not be a proof. For instance, a twff whose sequent tree term is ande("A A B") corre­ sponds to a proof, but that whose term is ande("AV B") does not. In metalevel programming languages (like ML [Gordon et al., 1979]), given two simple tactics corre­ sponding to the ones above, they need to be executed in order to know that the former succeeds whereas the latter fails. In MT, the derivability of preconditions de­ termines whether twffs correspond to proofs:

Theorem 3 (Preconditions) : Let II be any sequent tree of s in OT. Let P be the preconditions of the twff w(TI). Then IMT P ¢::::::} II is a proof of s.

Proof[hinted]. The proof is performed over the com­ plexity of II. As an example of the step case let us con­ sider AE. Let II be:

Let w(IIl) be P1 - T(tl).

( =>) If II is a proof then AE is applicable and the wff of s1 is a conjunction. This implies IMT Conj(tl). By the induction hypothesis we conclude IMT P1 . Then as Pis P1 A Conj(t1) we have IMT P.

(-¢::) IfiMT P 1 AConj(tl), then by induction hypothe­ ses we prove Il1 is a proof. We prove that IMT Conj(t1) implies that s1 is a conjunction. Then the AE rule is applicable and II is a proof. Q.E.D.

Notice that, because of theorem 3, the success of tac­ tics can be stated without executing them.

5 Metatheory interpretation as system code execution

Theorem 1 guarantees that, for any successful GET strat­ egy, the corresponding twff can be deduced. The idea is to map any twff into GET code and use it to prove the goal. This idea of mapping back can be seen in two ways:

(1} The inverse of mup can be defined and used to compile twffs back in the code (the "mapping down" arrow in figure 1}. For any twff, the result is a strategy available to the user.

(2} Twffs can be interpreted in terms of the GET code. The result is the assertion of the sequent as a theorem in OT.

In the remainder of the paper we concentrate on the interpretation of twffs. In w(II) = P - T(t) we can distinguish three parts: the preconditions P, the pred­ icate T and the sequent tree term t. The assertion of the theorem in OT can be seen as the sequence of three steps: (i) prove P and obtain T(t) (subsection 5.1), (ii) from t generate the name of the endsequent s of II, "s" (not described as very similar, in principle, to step (i) ), finally (iii), from T("s") asserts in OT (subsection 5.2) .

5.1 Proving P

Theorem 3 tells us that the preconditions of any twff rep­ resenting an object level proof can be proved by theorem proving in MT. This is the "usual" approach taken so far in theorem proving. A problem with this approach may be the size of the search space in MT which, even drop­ ping the completeness requirement, can explode when complex metareasoning is required. The correspondence existing between MT and the GET code provides us with an alternative technique for proving in MT facts about OT. The idea is to avoid the explicit axiomatization of parts of OT and to perform computation instead of de­ duction. As shown above, having a mechanization of the logic gives us a one-to-one mapping between elements of the signature of MT and GET functions (section 3, fig­ ure 3) and opens up the possibility to see deductions in MT in terms of computation in GET (section 4, the­ orems 1,2). For how twffs are defined, their syntactic structure explicitly resembles the structure of the com­ putation tree they represent. As a consequence we can compute in GET following the syntax of the twff. Let us consider, as an example, the case where one of the con­ juncts ofP is Conj("AAB"). Conj has been mapped up from the code function CONJ and "AAB" is the metathe­ oretic constant which denotes the theorem A A B . Ex­ ecuting (CONJ A A B) gives TRUE, this means that the metatheoretic sentence C onj ("A A B"} is true and can be rewritten to the constant for truth, True .

Notice that, in order to implement the machinery de­ scribed above, GETFOL must keep track of the link be­ tween the functions and predicates of the signature of MT and the GET functions they have been mapped from (by mup)· It must also remember which elements of OT the constants in M.C are names of. GETFOL has in its code a data structure where it memorizes the pairs ( "o", o}, where "o" is an MT constant, name of o, a syn­ tactic object in OT. The possibility to create pairs ( name, object } is implemented by the semantic attach­ ment functionality [Weyhrauch, 1980] shown in figure 1.

Let us give the formal definition of the interpreter im­ plemented in GETFOL, I, which maps twffs into computa­ tion. Let us restrict ourselves to terms and atomic wffs. Let us suppose that, for any object in OT, o, "o" is a constant in MT. Then I can be defined as follows 6 :

6 "o" means function composition. The notation should be made precise, by explaining how to denote function com­ position with functions with more than one argument. Since not relevant in this context, this issue is not faced.

Thus, for instance, instead of proving infinitely many metatheoretic theorems of the form Conj("A, 1\Bs"), we can apply I to Conj("A,AB/') to obtain I(Conj("A11\ B,")) = I(Conjj(I("A, 1\ Bs'')) = I(Conj)(A, 1\ B,) = (CON J A, 1\ B, ) .

Notice that for any atomic wff or term wt, I( wt) is the execution of the code c such that mup(c) = wt.

Supposing that, for any n-ary function and predicate symbol fp, fp computes the right extension (with n­ ary function symbols, the ( n + 1 )-element of their set theoretic definition; with predicate symbols, either TRUE or FALSE) then I performs exactly the interpretation of terms and atomic wffs in a first order model. This result can be generalized to twffs and, more in generai, to any sentence in MT. Thus the correctness and completeness of this translation of deduction into computation can be proved from the correctness and completeness results for first order logic 8 .

What said above amounts to saying that OT is the standard model for MT. This is, we think, a correct way to see things and very much in agreement with Tarski's original definition of interpretation [Tarski, 1956]. More on seeing interpretation, from a computational point of view (in terms of the recursive definition of I), as the process of extracting objects from (quotation-mark and structural- descriptive) names is in section 4 of [Giunchiglia and Traverso, 1990]).

5.2 MT-OT interaction via reflection

We can prove the following lemma:

Lemma 1 (Name equality) Let IT be any sequent tree of s in OT. Let "s" be the quotation mark name of s. Let t be the sequent tree term of the twff w(IT). Then fMr t = "s" '¢:::::::> IT is a proof of s.

A sequent tree term t, when corresponding to a proof IT in OT, can be proved equal to the quotation mark name of the theorem proved by IT and viceversa. From theorem 1 and lemma 1 we can thus derive the following result:

Corollary 1, (Reflection) : Let IT be any sequent tree of s in OT. Let "s" be the quotation mark name of s . Then fMr T("s") '¢:::::::> IT is a proof of s.

In other words fMr T("s") '¢:::::::> l-or s . Then the reflection rules [Giunchiglia and Smaill, 1989]

are (a sort of) derived inference rules between theories in the multitheory system MT- OT. Notice that the pro­ cedural distinction between "being an already asserted theorem" and " being a theorem to be asserted", lost by mup, is brought back by the reflection rules. In fact , Rup can be executed only on theorems already asserted in OT, while, viceversa, Rdown can be executed to assert new theorems in OT. Occurrences of T that in the com­ pilation down from MT to GET would be translated into IS-A-THEOREM correspond to applying Rup; viceversa, the occurrences of T that would be compiled down into proof-add-theorem correspond to applying Rdown· The use of reflection up and down allows us to give a declara­ tive explanation of the interaction between reasoning in OT and reasoning in MT and, in particular, of how (and why) it is possible to assert theorems in OT as a result of deduction in MT.

7 By (COlU A; 1\ B;) we mean the result of the application of the GET function COlU to its arguments.

8 Note that truth is tested in the standard model. It is well known that the set of wffs true in a model is larger than the set of valid wffs. On the other hand it can be proved that, the interpretation in GETFOL restricted to atomic ground wffs (the elements of P) returns TRUE iff the wff is valid in all models of MT and thus provable in MT.

5.3 Deducing in OT via reasoning in MT

In this section we show how a twff can be interpreted to prove a theorem in OT. As a prototypical example, let us consider the following twff:

Let us take s as a shorthand for 'v'x(A(x) 1\ B(x)). In this case the above twff is a theorem in MT and "represents" the proof implemented by the program (all-distr-conj s x x) (see section 2) . Given the sequent s asserted in OT we can apply Rup to obtain T("s") in MT. T("s") can be used to derive

The interpretation of Forall("s") leads to the ex­ ecution of (FORALL s) which evaluates to TRUE. The same happens with all the other conjuncts. Thus, by simple propositional reasoning, it is possible to derive T( alii( ande( aile ( "s", "x", "x")), "x", "x" )).

The interpretation of alle("s", "x" , "x") leads to the execution of (alle-fun s x x) which evaluates to A(x) 1\ B(x). The result of the interpretation of the whole term is then 'v'xA(x). Reflection down can thus be used to assert the new theorem in OT:

The code performing the above steps is implemented in GETFOL and can be run by the command REFLECT [Giunchiglia and Smaill, 1989]. Notice that running the code compiled by the "mapping down" would give the same result as running REFLECT. The inverse of mup is to REFLECT exactly what compilation is to interpreta­ tion: execution of code generated by the inverse of mup produces the same results as interpreting metalevel the­ orems via REFLECT.

6 Conclusions and related work

In this paper we have presented a theorem prover, GETFOL, where the underlying code has been written to behave as the procedural metalevel of the logic it im­ plements. This approach seems a first step towards the development of systems able to modify deductively and automatically their underlying computation machinery. In fact:

{a) a logical metatheory MT can be automatically generated from the code;

(b) (some of) the theorems of MT represent object level computations;

(c) these theorems can be automatically compiled back in the system code to extend or to modify it (modi­ fication is achieved by redefining GET function symbols);

(d) these theorems can be automatically interpreted to assert object level theorems. In this case, as a side effect, we have a proven correct way to mix, at run time, object and metalevel theorem proving via the use of re­ flection up and down. More on this issue can be found in [Giunchiglia and Traverso, 1990] which also has a long section on the related work, in particular with [Bundy, 1988; Weyhrauch, 1980].

As far as we know, this approach is new and has never been proposed before. However, some comparisons with existing systems can nevertheless be made.

The idea of a metatheory mapped directly from the system code is somehow similar to the idea underly­ ing the work on metafunctions [Boyer and Moore, 1981] (in the Boyer and Moore theorem prover the code is the metatheory). In [Boyer and Moore, 1981], user de­ fined term-rewriting functions can be checked to verify whether they preserve the "meaning" of terms. Aside from the technical differences, a fundamental difference is that we provide a metatheory in which we can perform automatic deduction to build correct control strategies, while Boyer and Moore verify the correctness of the user defined strategies.

Besides Boyer and Moore's work [Boyer and Moore, 1981], none of the existing theorem provers, has the pos­ sibility of using the results of deduction in the metathe­ ory to produce modifications of the underlying system code. This is, for instance, the case also in NuPrl [Con­ stable et al., 1986; Howe, 1988], even if in NuPrl the synthesis of new tactics can be obtained by metatheo­ retic theorem proving (via the "propositions-as-types" paradigm). Analogously, metainterpreters can control the Prolog search strategy but cannot modify it. That is, the user can write a metainterpreter for any desired search strategy, however the metainterpreter will be ex­ ecuted by using the Prolog built-in search strategy.

For whaf concerns the issue of self-modification, the work which most closely resembles ours is Brian Smith's [Smith, 1983]. The substantial difference is that, in GETFOL, metatheoretic statements are generated by met­ alevel deduction and not by computation and that the tactics derived are provably correct. No non-theorems can be proved.

Aknowledgments

The authors thank the Mechanized Reasoning Group at IRST and the Mathematical Reasoning Group in Edinburgh, in particular Alan Bundy, David Basin, Alessan­ dro Cimatti, Luciano Serafini, Alex Simpson and Alan Smaill. Vanni Criscuolo, Bob Kowalski, Carolyn Tal­ cott, Frank VanHarmelem and Richard Weyhrauch are also thanked.