Procedural Embedding of knowledge in Planner

1. The Structural Foundations of Problem Solvlne

We would 1 ike to develop a foundation for problem solving analogous In some ways to the currently exlstlnp; foundations for mathematics. Thus we need to anal yze the struc~ure of foundations for mathematics. A foundation for mathematics must provide a definitional formal Ism In which mathematical objects can be defined and their existence proved, For example set theory as a foundat ion provides t ha t objects mu st he built out of sets. Then there must be a deductive f o rnal ism In 1·1hlch funda~. ,ental truths can be stated and the means provided to de duce additional truths from those already established. Current mathematical found~t l ons such as set theory seem quite natural and adequate for the vast body of classical mathematics. The objects and reas oning of most mathematical domains such as analysis and algebra can be easily founded on set theory, The ex istence of certain astronomically large cardinals poses some problems for set theoretic foundations, However, the problems posed seen to be of nr actlcal Importance only to certain category theorists, Foundations of mathematics have devoted a great deal of attention to the problems of consistency and comnleteness. The problem of consistency Is lmoortant since If the foundations are Inconsistent then any formula whats oever may he deduced thus tri v ia l izlng the foundations. Semantics for fo undations of

ma t hematics are defined model theoretically In terms of the notion of satlsflahlllty, The problem of completeness Is that, for a foundation of mathematics to be Intuitively satisfactory all the true formulas should be proveahle since a foundation mathematics alms to be a theory of mathematical truth, Similar fundamental questions must be faced by a foundation for problem solving, However there are some Important differences since a foundation of problem solving alms more to be a theory of actions and purposes than a theory of mathematical truth, A foundation for problem solving must specify a goal-oriented formal Ism In which problems can be stated, Furthermore there must be a formalism for speclfyln~ the allowable methods of solution of problems. As part of the definition of the fornallsms, the followlnn elements must be defined: the data structure, the control structure, and the primitive procedures, The problem of what are allowable data structures for facts about the world Immediately arises. Being a theory of actions, a foundation for prohlen solving must confront the problem of chanp;e: How can account be taken of the changing situation In the world? In order for there to be problem solvlnp;, there must be a problem solver. A foundation for problem solving must consider how much knowledge and what kind of knowledge problem solvers can have about themselves. In contrast to the foundation of mathematics, the semantics for a foundation for problem solvlne should be defined In terms of properties of procedures, \le would like to see mathematical Investigations on the adequacy of the foundations for problem solving provided by PLANNER, In chapter e of the dissertation, we have made the beglnnlnr.s of one kind of such an Investigation.

To he more specific a foundation for problem solving must concern Itself with the following

complex of topics.

f'flOCEDUI'AL E11 BEDDING: Hov, can "real v1orld" knov,ledge be effectively embedded In procedures. \Jha t are good ways to express problem solution methods and how can plans for the

solution of problems be formulated?

GENErALIZED C011PILATION: are good methods for transforming level p;oal-orlented language Into specific efficient algorithms. \/hat high VERIFICATIO~: How can It be verified that a procedure does what Is Intended.

PrOCEDURAL A !'IS TRACT I ON: \/hat are good Methods for abstracting r,eneral procedures from special cases.

One approach to foundations for probleM solving reQuires that there should be two distinct forMal Isms:

1: A IIETHODS forMal Ism which specifies the allow~hle Methods of solution

2: A PP.OFlLEII SPECIFICATION forMallsn In \·,hlch to pose problems.

The prohlen solver Is expected to flr,urc out h01. conhlne Its available Methods In order to produce a solution which s~tlsfles the prohlen speclflc~tlon. One of the aiMs of the above fornul~tlon of prohlern solvlnp, Is to clearly separate the methods of solution fror1 the prohlerns posed so thilt It is lnposslhle to "cheat" and p,lve the prohlen solver the methods for solvlnr, the prohlern alonp, with the statenent of the prohler1, lie propose to bridr,e the ch~sM het1·1een the methods forn~l lsn and the prohlen formal Ism. Consider More carefully the two extrene s in the specification of processlnr,:

A: Explicit processlnr, (c.!!;. methods) Is the ahlllty to specify ~nd control actions do11n to the finest details.

R: lnpliclt processlnp, (e.r,. prohlerns) Is the ability to specify the end result desired ~nd not h~ve to say very rTJuch ~bout ho1·1 It should he achieved.

PLfltHIEP ~ttenpts to provide ~ formill ism In which i1 problem solver can brldp,e the continuun het1·1een ex1111clt Clnd ln111iclt 11rocesslnr,. lie aln for a M~xlr1uM of flcxlhlllty so that \·,h~tever knowlcdp,c Is ~vallahle c~n be lncor11orated even If It Is fragmentary and heuristic.

Our \·,orl: on PLMHJEP. has been an investip,atlon In PROCEnurAL E P I S T E r 1n L n G Y, the s t u d y of h 01·1 knowledr,e Ciln he eMbedded In 11roccdures. The THESIS OF PP.OCEDUP.AL E ~:f'I EOI'liii� Is that Intellectual structures should he analyzed throur,h their P~OCEI'lllf>AL Ml/\LOGIJES. \!e 1' i 11 try to sho11 1·1h~t 1·1e r1ean throur,h exan11les:

DESCRIPTIONS arc procedures which recor,nlze how well sone candidate fits the description.

PATTEIWS arc

descriptions which match configurations of data. For exanplc <either 4 <atonic>> Is a procedure which will recop,nlze sonethlng which Is either 4 o r I s a t o~1 I c ·

DATA TYPES are patterns used In declariltlons of the allowilble ranee and dornaln of procedures and Identifiers. 1\ore p,enerally, data types have analoeues In the forn of procedures which create, destroy, recor,nlzc, and tr~nsforn d~ta,

Gr.AI1tl/\r.S: The PROGT1M1'1Ar. lanr,u~r,e of Terry l! lnop,rad represents the first ste11 to~ards one kind of 11roccdural analoP.ue for natural lanp,u~p,e r,r~nr1ar,

SCHEIIATIC DP. A~!I~I�S have as their procedural analoP.ue methods for recor,nlzlnr, when particular figures fit within the schenata.

PROOf-S correspond to procedures for recor,nlzlnP. ~nd expandinr, v~lld chains of deductions. Indeed many proofs can fruitfully be considered to define procedures which are proved to have certain properties.

1100ElS of rr.n�PN~S are procedures for defining properties of procedures and attenptlnp, to verify . these properties. llodels of pror.rans can be defined by procedures which state the relations that nust hold ~s control passes throur,h the pror.r~n.

PLA~S ~rc general, p,oal oriented procedures for atter1r1tlnr, to carry out sone tilsl:.

THEOI'EIIS of the l(l!MlTif.ICATIO'!AL CALCULUS h;we ~s their analor,ues procedures for carrying out the deductions ~,hJch nrc justified by the theorens. For exor1plc, consider a theorcr1 of thP. forr , ( HIPL I ES x y), One procedural analor,uP. of the theorP.n Is to consider whethP.r x should be nadc a subr,onl In order to try to prove sonethinr, of the forr1 y, lr~ Goldstein has shm.n that the theorcr1s of elP.r1cnt~ry plane r,conetry have very n~tur<Jl procedurnl ~nalor.ucs.

OR/\\!IIJGS: The procedurul analor;uc of a drav.tnr. Is a procedure for n~l:lnr. the dr~1·.lng, Rather sophisticated display processors have been constructed for making drawln~s on cathode ray tubes.

nECCH111HJDAT IONS: PLANNEn has primitives which allow recommendations as to how disparate sections of goal oriented language should he linked together In order to accomplIsh some particular task.

GOAL TnEES are represented hy a snapshot of the Instantaneous confl~uratlon of problen solving

processes.

One corollary of the thesis of procedural embedding Is that learning entails the learning of the procedures In which the knowledge to he learned Is emheddcd. Another aspect of the thesis of procedural embedding Is that the process of ~oln~ fron general goal oriented lan~uage which Is capable of accOMPI lshlnp; some task to a special purpose, efficient, algorithm for the task should Itself be Mechanized. By expressing the properties of the special purpose algorlthn In terms of their procedural analo~ues, we can use the analogues to estahl Ish that the special purpose routine does In fact do ~"'hat I t I s I n t c n d c d to do.

\le are concerned as to ho~, a theorcn prover can unify structural, prohlen solving methods with domain dependent algorlthns and data Into a coherent prohlen solvln~ process. By structural methods we mean those th~t arc concerned 1·dth the fornal structure of the arguMent rather than with the senantlcs of Its donaln dependent

content.

~n exanple of a structural method Is the "consequences of the consequent" heuristic. By the COtJSE')lJEtiCES OF THE COtiSEr)UHIT heuristic, we mean that a prohlen solver should look at the consequences of the ~oal that Is beln~ attempted In order to r,ct an Idea of some of the statements that could be useful In

estahl lshinr, or reject lnp, the r.oal.

lie need to discover more po1,erful structur<Jl nethods, PLMI~JEP Is Intended to provide a computational basis for expressinr, structural methods. One of the nost Important Ideas In PLAflf!Er. is that It brings sone of the structur<Jl methods of prohlem solving out Into the open v,here they can be analyzed and r,eneral ized, There are a few basic patterns of looping and recursion that arc in constant use anonr, pror.ranMcrs. ExaMples are

recursion on binary trees as In LISP

and the FIND statement of PLANNER. The primitive FIND will construct a. list of all the objects with certain properties. For example we can find five things which are on something which Is green by evaluating

<FIND 5 X <GOAL (ON X y)>

<GOAL (GnEEN y)>>

l·,hich reads "find 5 x's such that x Is OtJ y and y Is GnEEN."

The patterns of looping and recursion represent comnon structural methods used In pror,raMs. They specify hOI, comnands can be repeated Iteratively and recursively. One of the main problens In getting computers to write pror.rams Is hOI, to use these structural patterns l'dth the particular domain dependent connands that are avallahle, It Is difficult to decide 1'1hich, If any, of the basic patterns Is appropriate In any given prohlem. The prohlen of synthesizing pror.rams out of canned loops Is forr1a1ly Identical to t~e prohlen of flndlnr, proofs using ~1athenatlcal Induction. 1:e have approached the problem of constructing procedures out of goal oriented language fron two directions. The first Is to usc canned loops (such as the FIND statement) where we assume a­ priori the kind of control structure that Is needed. The second approach is to try to abstract the procedure from protocols of Its action In p<Jrtlcular cases.

~nothcr structural method is pror,resslvc refinement. The way prohlens arc solved hy pror,ressive ref I nef"1ent Is by repeated eviJ 1 uat I on. Instead of trying to do u complete search of the problcn sp<Jce all at once, repeated refinements ure made. For exanple In a r,ane like chess the same Purt of the r,ane tree might be lool:ed at several times. Each tine certain paths are more deeply explored In the llr,ht of ~,hat other searches hove rcvculed to he the key features of the position. Prohlcns In desir.n seen to he particularly suitable for the use of progressive rcflncncnt since proposed designs arc often themselves amenable to successive refiner1cnt. The way In which pror.rcsslve refinement typic<J11y is done In PLAtlt!EP is by rcpe<Jtcrl cvaluutlon. Thus the expression which Is evaluated to solve the nrohler1 1·, 111 Itself produce as Its

vulue an expression to be evaluated.

2. lnfornatlon Processing Overview Sor1e readers will prefer to reQd section 3 which has concrete exanples before the abstract discussion In this section.

There are many ways In which one can approach a description of PLArHJER. In this section 1ve vdll describe PLAtltJER fron an lnfornatlon Processlnr. VIewpoint. To do this we will describe the data structure and

the control structure of the fornal Ism.

Ofi TA STfHJCTUP.E:

ASSOCIATIVE r1Er\OP.Y ferns the basis for PLAtHIER's data space v·hlch consists of directed graphs with labeled arcs. The operation of PUTTING and GETTING the conponents of data objects have been generalized to apply to any data type whatsoever. For exanple to PUT the value CANONICAL on the expression (+ X Y (· X Z)) under the IndIcator S tr'PLI F I ED Is one way to record that (+X Y (· X Z)) has been canon ically sl r:-~ pllfled. Then the der,ree to which an expression Is sl nnl ifled can be deternlned by GETTING the value under the Indicator SI ~~ PLIFIED of the expression. The operation of PUT and GET can be lnplenented efficiently using hash codlnr,. Lists and vectors have been Introduce d t o r,aln r:-~ore efficiency for connon special case structures. The associative nenory Is useful to PLANNER In many v·ays. llonltorlng gives PLANNER the capability of trapping all read, write, and execute references to a particul a r data object. The monitor (wh ich Is found under the Indicator i 10~1 1 Torn of the data ·object can then take any action that It sees fit In order to handle the situation. The associative menory can be used to retrieve the value of an Identifier of a process p by GETTING the I conponent of p. Code can be conmented by slnply PUTTING the actual comMent

under the Indicator COIH1ENT.

0 AT A BASE : I I hat I s mo s t distinctive about the way In which PLANNER uses data Is that It has a data base In which data can be Inserted and removed. For example Inserting (AT Bl P2) Into the data base might signify that block Bl Is at the place P2. A coordinate of an expression Is defined to be an atom In some position. An expression Is detern lned by Its coordinates. Assertions are stored In buc kets by their coordinates using the associative mer:-~ory In order to provide

efficient retrieval. In addition a total ordering Is Imposed on the assertions so that the buckets can be sorted. Imperatives as V<ell as declaratlves can be stored In the data base. l/e might assert that whenever an expression of the form (At objectl pl acel) Is removed fro~1 the data base, then any expression In the data base of of the forn (ON objectl object2) should also be removed fron the data base. The data base can be tree structured so that It Is possible to slnultaneously have sever;tl local data bases which are lnconpatlhle. Furthernore assertions In the data base can have varying scopes so that some vd 11 1 as t the duration of a process while others are tenporary to a subroutine.

CONTROL STRUCTURE: PLfiNNER uses a pattern directed r:-~ultlprocess bac ktrac k control structure to tie the operation

of Its primitives together.

BfiC~TRACKIN�: PLANNER processes have the capab Ill ty of hacktrack lnp, to previous states. A process can backtrack Into a procedure activation (I.e. a specific Instance of an Invocation of the procedure) which has already returned with a result. Using the theory of comparative schematolor,y, we have proved In the dissertation that the use of backtrack control enables us to achieve e ffects that a language (such as LISP) which Is llnlted to recursive control structure cannot achieve. Backtrack ing cuts across the subroutine structure of PLANNEr.. Backtrack control allows the consequences of elaborate tentative hypotheses to he explored without losing the capability of rejecting the hypotheses and all of their consequences. A choice can be made on the basis of the available knowledge and If It doesn't wort: , a better choice can be made using the new Information discovered while Investigating the first choice. Also backtrack control makes PLANNER procedures easter to dehug since they can he run backwards as well as forwards enabling a problem

solver to "zero In" on bugs.

11ULTIPROCESSING gives PLANNER the capabll tty of having more than one locus of control In problem solving. By using multiple processes, arbitrary patterns of search through a conceptual problem space can be carried out. Processes can have the power to create, read, 1··r I te, Interrupt, resume, sIngle

step, and fork other processes.

PATTEnN DIRECTiON combines aspects of control and data structure. The fundamental principle of pattern directed computation Is that a procedure should be a pattern of what the procedure Is Intended to accomplIsh. In other words a procedure should not only do the right thing but It should appear to do the right thing as welll PLANNE~ uses pattern direction for the following operations:

CONSTnUCTION of structured data objects Is accomplI shed hy templates. \le can construct a list v1hose first element Is the value of x and whose second element Is the value of y by the procedure (x y). If x has the value 3 and y has the value (A B) then (x y) will evaluate to (3 (A B)),

DECOI1POS IT I ON Is accompli shed by matchlnr, the data object against a structured pattern. If the pattern (xl x2) Is matched against the data object ((3 4) A) then xl will be given the value (3 4) and x2 ~dll be given the value A.

nETniEVAl: An assertion Is retrieved from the data base by specifying a pattern which the assertion must match and thus bind the Identifiers In the pattern. For example we can determine If there Is anything In the data base of the form (Otr x A). If (ON B A) Is the only Item In the data base, then x Is bound to B. If there Is more than one Item In the data base which matches a retrieval pattern, then an arhltrary choice Is made. The fact that a choice was made Is remembered so that If a simple failure backtracks to the decision,

another choice can be made.

INVOCATION: Procedures can be Invoked by patterns of what they are supposed to accomplIsh. For example a procedure might be defined which attempts to satisfy patterns of the form (ON x y) by causing x to be ON y, Such a procedure could he Invoked by making (ON A B) a goal. The procedure mlr.ht or might not succeed In achieving Its goal depending on the environment In which It was called. Since many theorems mlr,ht match a goal, a recommendation Is allowed as to which of the candidate theorems might be useful. The recommendation Is a pattern which a candidate theorem must match In order to be Invoked.

r

EXAA/1 PL E AN ASSOCIATioN

L

3. An Extended exaMple

This section contains an extended description of a simple exanple In PLMit!ER. It Is partially based on a draft written by T. Wlnor;rad for the course 6 .545. If the reader would 1 Ike to see a nore loclcally systenatic presentation, he can consult the th~ athor's dissertation,

The easiest way to understand PLM!t!ER Is to 1-1atch hm·, It wor ks, so In this section v1e vd ll present a fev1 slnple exanples and explain the use of sane of Its Most elenentary features. These ex~nples are not Intended to represent TOY PD.Of3LE '\S to serve as test cases for "general problem solvers". The toy problen parad lp;n Is misleading because toy problens can be solved 1dthout any rc <1 l knovdedce of the donaln In which the toy probleM Is pos ed . Indeed, It seer1s gauche to use any thing as P011erful as r~al knoviledge on s uch slnple problens. In contrast 1·1e believe that real ·norld problems r equ ire vast anounts of procedural kno1·ilder;e for their so lution. \le see It as part of our tas k to provide the In tellectual capabilities needed for effective problen solvlnp . \/e 1·,ould lll:e to see the toy prob leM paradlgn replaced 11l th an I t!T ELLECTUAL CAPABILITY p<Jradlgn where the object Is to Illustrate the Intellectual capabilities needed so t l':at knOI·· ledge c <J n be effectively en~e de ded In procedures.

First v.e ~dll ta ke the Most venerable of trad itiona l deductions: Turinp; Is a hunan All hunans arc fallible

5 0

Turing Is fallible.

It Is easy enour; h to see how this coul d be expressed In the usual lop; lcal notation and hand led by a un iforn proof procedure. Instead, let us e xpress It In one possi ble way to PLAWJ ER by saying:

<ASS ERT (H Ut~ Atl TU f' ING }>

<ASSERT <DEF I t! E THEOREt1l <COt!S EI').tJEtJT (Y) (FALLIBLE ?Y}

. <GOAL (HUt\Atl ?Y) »»

Function calls are enclosed be t 11een " <" and ">". The proof 1vould be r;cnerated by asking PLANNER to evaluate the expressi on:

<GOAL (FALLI BLE TUR ING) >

\ lc IMnedlately see several points. First, there are at least tv.o different k inds of lnfornatlon stored In the data hase: declara t lves and lnperatlves.

tlot Ice that for complex sentences containing quantifiers or lop;lcal connectives we have a choice whether to express the sentence by declaratlves or by lnperatlves.

Second, one of the most IMportant points ahout PLANNER Is that It Is an evaluator for statenents. It accepts Input In the forn of expressions 1·1rltten In the PLMltiEP. lanr;uar.e and evaluates them, producing a value and side effects, ASSERT Is a function which, when evaluated, stores Its arr;unent In the data base of assertions, In this example we have defined a theoren of the CONSEQUENT type (we vd II see other types later}. This states that If we ever want to establish a r,oal of the forM (FALLIBLE ?Y}, we can do this by accoMpl lshlng the goal (HUt ~ AtJ ?Y}, 1·1here Y Is a Identifier. The stranp;~ prefix character "?" Is part of PLA'JNER's pattern matchlnp; capabll I tics (which are extensive and nake use of the pat tern-natch lnp; 1 anp;uap;e t\ATCHLESS which Is explained In chapter 4 of the dissertation). If we ask PLANNER to prove a r;oill of the forM (A Y), there Is no ohvlous way of knowing whether A and Y are constants (like Tl! R I~I� and HU~: Atl In the exilmple) or Identifiers. LISP solves this problem by using the function QUOTE to Indicate constants. In pattern natchlng this Is Inconvenient and makes most patterns nuch bulkier and more difficult to read, Instead, PLANNER uses the opposite convention --a constant Is represented by the atom Itself, while a Identifier nust be Indicated by adding an appropriate prefix. This prefix differs according to the exact use of the Identifier In the pattern, but for the tine belnr. let us just accept"?" as a prefix Indicating a Identifier. The definition of the theorem Indicates that It has one Identifier, Y by the

(Y) following CONSEQUENT.

The third statenent Illustrates the function GOAL, which tries to prove an assertion. This can function In several ways. If we had asked PLANNER to evaluate <GOAL (Hl!t1AN TURING)> It would have found the requested assertion lnmedlately In the data base and succeeded (returning as Its value sane Indicator that It had succeeded), Hm,ever, (FALLIBLE TURING) has not been asserted, so we must resort to theorems to prove lt. Later we vdll see that a GOAL statenent can give PLANNER various kinds of advice on which theorems are applicable to the goal and should be tried. For the monent, take the default case, In which the evaluator tries all theorems whose consequent Is of a forM which M<Jtches the goal (I.e.

a theorem with a consequent (?Z TURING) would be tried, but one of the form (HAPPY ?Z) or (FALLIBLE ?Y ?Z) would not). Assertions can have an arbitrary 1 1st structure for their format -- they are not 1 lnlted to two-member 1 lsts or three-Member lists as In these examples.) The theorem we have just defined would be found, and In trying It, the match of the consequence to the goal would cause the Identifier Y to be bound to the constant TURING. Therefore, the theorem sets up a new r;oal (HU11MI TURING) and thIs succeeds Immediately since It Is In the data base. In general, the success of a theorem will depend on evaluating a PLANNER pror.ram of arbitrary complexity, In this case It contains only a single GOAL statement, so Its success causes the entire theoreM to succeed, and the goal (FALLIBLE TURING) Is proved. The following Is the

protocol of the evaluation:

<GOAL (FALLIRLE TURING)> (FALLIBLE TUI'!ING) Is not In the data base so attenpt to Invoke a theorem to esahl Ish the goal enter THEOI'!Eill Y becoMes TUP.ING <GOAL (HU:lAII TURING)> Is satisfied since the goal Is In the

data hnse return (FALLIRLE TURING)

The way In which Identifiers are bound by matching Is of key Importance to PLMINEP.. Consider the question "Is anything fallible?", or In logic (EXISTS X (FALLIBLE X)), This could be expressed In PLANNER as:

<THPROG (X) <GOAL (FALLIBLE ?X)>> Notice that THPP.OG (PLANNER's equivalent of a LISP PROG, complete with GO stntements, tar:s, RETURN, etc.) In this case It acts as an existential quantifier. It provides a blndlnr;­ place for the Identifier X, but does not Initialize It-- It leaves It In a state particularly marked as unassigned. To answer the question, we ask PLANNEr. to evaluate the entire THPROG expression above. To do this It starts by evaluating the GOAL expression, This searches the data hase for an assertion of the form (FALLIOLE ?X) and falls. It then looks for a theorem with a consequent of that form, and finds the theorem we defined above. trm, \'1hen the theoren Is called, the Identifier Y In the theorem Is linked to the Identifier X In the goal, hut since X hils no value yet, Y does not receive a value. The theoren then sets up the r.onl (HlJIIMI ?Y) 1vl th Y as an Identifier. The PLANNER primitive GOAL uses the data-base searching mechanism to look for any assertion which matches that pattern (I.e. an Instantiation), and finds the assertion (HlJtiAN TURING). This causes Y (and therefore X) to be bound to the constant TURING, and the theorem succeeds, completing the proof and returnlnp, the value (FALLIBLE TURING), There seens to be sonethlng misslnr.. So far,the data base has contained only the relevant objects, and therefore PLANNER has found the right assertions Immediately. Consider the problem we would get If we added new Information by evaluatlnr; the statements:

<ASSEP.T (HUIIflrl SOCRfiTES)> <ASSERT (GREEK SOCRATES)>

Our data base now contains the assertions:

(HUI 1AN TURING) (HUI1AII SOCRATES) (GREE I-: SOCI'!ATES)

and theoreml:

<CotiSEQUEtJT (Y) ( FALLI OLE ?Y) <GOfiL ( HU il flll ?Y) »

\lhat If 1ve nob ask, "Is there a fallible Greet:?" In PLANNER 1ve 1vould do this by evaluating the expression:

<THPROG (X) <GOAL (FALLIOLE ?X)> <GOAL (GREEK ?X)>>

THPP.OG Is a wishy-washy ve~sion of the LISP function PROG. If THPI'!OG runs Into a failure trying to evaluate one of the expressions In Its body, then It backtracks to the last decison that was made and dumps the rcsponslhll lty of hob to proceed on the procedure l··hlch mane the decision. llotlce what mlr,ht happen, The first GOAL nay be satisfied by exactly the snme derluctlon as before, since we have not removed lnfornatlon. If the data­ base searcher happens to run Into TUR I riG before It fInds SOCRATES, the goal (HLJI1MI ?Y) 1·dll succeed, blndlnr. Y and thus X to TURING, After (FALLI£lLE ?X) succeeds, the TIIPROG 1vlll then establish the nev. r,onl (GP.EEK TURING), which Is dooned to fall since It has not been asserted, and there are no applicable theorens. If we thlnl: In LISP terns, this Is a serious problen, since the evaluntlon of the first GOAL has been completed before the second one Is called, nnd the "stack" nov, contains only the return address for THPP.OG and the Identifier X. If we try

FORMAT OF FUNCTION ACTIVATIONS IN SNAPSHOTS

to r,o back to the ber,lnnlnr. and start over, It vdll ilr,aln flnrl TURING and so on, arl InfinituM.

One of the Most IMportant features of the PLMHIEP. lanr,uage Is thilt backtrilcklnr. In case of failure Is always possible, and Moreover this hacktracklnr. can go to the last place where a decision of any sort was made. Here, the decision was to nick a particular assertion from the data base to match a goal. Another kind of decision Is the choice of a theorem to try to achieve a goal. PLANNER keeps enour.h Information to change any decision and send evaluation back down a ne11 path.

In our exannle the decision was Made Inside the theorem for FALLIBLE, v.hen the goal (HUriAtl ?Y) was matched to the assertion (HlJIIAN TURING). PLANNER vdll retrilce Its steps, try to find a different assertion which matches the goal, find (HlJIIAN SOCP.ATES), and continue with the proof. The theoreM will succeed with the value (FALLIBLE SOCP.ATES), ilnd the THPP.OG will proceed to the next expression, <GOAL (GREEK ?X) >. Since X has been bound to SOCP.ATES, this vdll set up the goal (GREEK SOCP.ATES) which will succeed lmnedlately hy finding the corresponding assertion In the data base. Since there are no more express Ions In the THPP.OG, It vd 11 succeed, returnlnr. as Its value the value of the last expression, (GREEK SOCRATES). The whole course of the deduction process depends on the failure mechanism for backtracking and trying thlnr.s over (this Is actually the process of trying different branches down the conceptual goal tree.) All of the functions like THCONO, THANO, THOP., etc. are controlled by success vs. failure, rather than NIL vs. non-NIL as In LISP. This then Is the PLANNER executive which estahl !shes ilnd Manipulates subgoals In looking for a proof.

\le wou 1 c1 now 1 Ike to gIve a soMewhat more fornal description of the behavior of PLANNER on the above problem. If we lntoduce suitable notation our probleM solving protocols can he made much more succinct and their structure marle visible. Also by formal lzlnr. the notions, we can make PLANNER construct and analyze protocols. This provides one kind of tool by which PLANNER can understand Its own behavior and make general lzatlons on how to proceed. In this case the protocol Is:

1: enter THPP.OG

2:

X Is rebound but not Initialized 3:

<GOAL (FALLIBLE ?X)> will attempt a pattern directed Invocation since nothing In the data base matches (FALLIBLE ?X). 4:

enter THEOREtll

5:

match (FALLIBLE ?Y) with (FALLIBLE ?X) thus linking Y to X the situation Is shown In snapshot number 1 6:

<GOAL (HUfiAN ?Y)> finds (HUtlAtl TURING) In the data base 7:

Y gets the value TURING thus giving X the value TURING 8:

return (HUI1AN TURING)

9:

THEOREf11 returns (FALLIBLE TUP.I tiG) 10:

<GOAL (GREEK TURitiG)' falls since It Is not In the data base and there are no matching consequents

Thus PLANNER must bilcktrack to step 7 and try again. The situation Is shown In snapshot nunbe r 2. For the convenience of the reader, we will repeat the first six steps from above and then continue the protocol.

1: enter THPROG

2:

X Is rebound but not Initialized

<GOAL (FALLIBLE ?X)>

enter THEOREf11

3:

4:

5:

match (FALLIBLE ?Y) with (FALLIBLE ?X) thus linking Y to X 6:

<GOAL (HlJ11AN ?Y)> finds

(HU11AN TUP.I NG) In the data base

11:

Y gets the value SOCRATES thus glvlnr. X the value SOCRATES 12:

13:

return (FALLIBLE SOCRATES)

THEDr!Ef11 returns (FALLIBLE SOCRATES) 14:

<GOAL (GREEK SOCRATES)> 15: return (GREEK SOCRATES) as the top level value

The situation Is shown In snapshot

number 3.

So far we have seen that although PLANNER Is \·,rltten as an evaluator, It differs In several critical w~ys from anything which Is normally considered a programnlng language. First, It Is goal-directed. Theorems can be thour,ht of as subroutines, but they can be cal len by speclfylnp, the goal which Is to be satisfied. This Is 1 Ike having the abllltly to say "Call a subroutine which will achieve the neslred result at this point." Second, the evaluator has the mechanism of success and failure to handle the exploration of the conceptual goal tree. In PLMJNER there Is no explicit goal tree. The conceptual goal tree Is representen by a SNAPSHOT of a Cat!F I GlHlAT I 0~1 of PROCESSES. Thus PLANNER has powerful control structure primitives tn allow the conceptional p,oal structure to be eilslly and naturally reflecten In the execution of PLAtJNEr. processes, Other evaluators, such as LISP, with a h~slc recursive evaluator have no way to do this. Third, PLANNER contains a large set of primitive comm~nds for matching patterns ann m~nlpulatlng a data base, and fo-r hand! lnp; that data base efficiently.

On the other sine, we can ask how It differs fron other theorem provers. \/hat Is galnen by writing theorems In the forn of prop;rams, ~nd giving then power to call other progr~ms which manipulate data? The key Is In the forn of the nata the theorem-prover can accept. t~ost systems take neclaratlve Information, as In predicate calculus. This Is in the form of expressions 1·,h I ch represent "facts" about the worln. These are manipulated by the theorem-prover accornlng to some fixed uniform process set by the system. PLANNER can make use .of Imperative Information, telling It how to go about provlnr. a subr,oal, or to make use of an assertion. This produces what Is callerl HIErAP.CHICI\L control structure. Thnt is, any theorem can Indicate what the theoren prover Is supposed to do as It continues the proof. It has the full POI·er to evaluate expressions which can depend on both the data base and the subr,oi11 tree, and to use Its results to control the further proof by milklnr, assertions, neclnlnr. what theorems are tn be userl, and specifylnp; a sequence of steps to be followed.

4. Current Ann! !cations for PLANNER The PLAtlrJEr. formalism Is currently helnr. userl In a variety of nppllciltlons. It Is belnp; usen as part of the conceptual machinery of a robot at r ~ .I.T. and Stanford. The for n<t llsm Is used fnr the fo!Jm,lng purposes In a robot:

semantic basis for natural language formulating and executing plans of

act I on flnnlng high level descriptions of visual scenes Other applications are Its use as a procedural model for: architecture design children stories models of pror,rans elementary Eucl !dean geometry

5. BIBLIOGPIIPHY

Balzer, R. EXDAt1S- Extendable Debugglnp, and t1onltorlng System. Proc. SJCC 1969, 34. 1·1ay, 1969.

Balzer, R. 11., On the Future of Computer Prop,ram Specification and Organization. December 1~70.

Dennis, Jack B. Prop;rammlng Generality, Parallelism and Computer Archltectue. Computation Structures Group t1emo tJo. 32. August 19GB.

Earley Jay, Toward an

Understanding of Data Structures. Computer Science Departement, University of California, Berkeley.

Fikes, R., Ref-Arf: A System for Solvlnp; Problems Stated as Procedures Artificial lntelllr,ence (1970).

Fisher, D. A., Control Sturctures for Programming Languages. 1'l70.

Hevdtt, C., PLANNER: a Language for Provlnp, Theorens, Artificial lntelllr,ence t1eno 137, t1assachusetts Institute of Technology (project t1AC), July 1%7.

Hel"lltt, C. PLMJtJEP.: A Language for t1anlpulatlnp, t1odels and Proving Theorems In a Robot, Proceed Jngs of the International Joint Conference on Artificial Intelligence. \lashlngton D. c. t1ay l9(iq,

Hel"lltt, C. Teaching Procedures In Humans and Robots. Conference on Structural Learning. llprll 5, 1970. Philadelphia, Pa.

Hewitt, C. Description and Theoretical Analysis (using Schemas) of PLAtltJER: A Lanp,uap,e for Proving Theorens and t1anlpulatlng t1odels In a Robot. Phd. Feb. l'l7l.

He1dtt, C. and Patterson t1. Comparative Schematolop,y, Record of Project t111C Conference on Concurrent Systems and Parallel Compuatlon. June 2-5, 1'l70. Avaflable from ACti.

Kay, Alan C., Reactive Engine, Ph. D. thesis University of Utah, 1970. t1cCarthy, J.; Abrahams, Paul

II.; Edl·,ards, Daniel J.; Hart, Timothy P.; and Levin, t11chael I, 1%2. Lisp 1.5 Pros;rammer's t1anual, t.1. I. T. Press.

t1cCarthy, J. and Hayes, P., Sone Philosophical Problems form the Standpoint of Artificial Intelligence. Stanford A. I. rleno 73.

~le1·,e11, A., Shaw, J. C., and Simon, H. A., 1q59, Report on a General Prohlen-solvlng Progran, Proceedings of the International Conference on lnfornatlon Processing, Parts: UNESCO

House, pp, 256-2611,

Perils, A. J. The Synthesis of Algorithmic Systems. JACrl, Jan. 1967,

Wlnonrad, T. Procedures as a neprcsentatlon for Data In a Computer Pror.ran for Understanding Natural Languar.e. IIAC Tn-r.l!. February 1971.