--- title: "META-INTERPRETATION OF RECURSIVE LIST-PROCESSING PROGRAMS" authors: - "Daniel Goossens" doi: "" url: "https://ijcai.org/proceedings/1979/237" pdf: "https://ijcai.org/proceedings/1979/0237.pdf" venue: "Proceedings of the Sixth International Joint Conference on Artificial Intelligence" year: 1979 pages: "" track: "" keywords: --- # META-INTERPRETATION OF RECURSIVE LIST-PROCESSING PROGRAMS Daniel Goossens *Proceedings of the Sixth International Joint Conference on Artificial Intelligence*. ## Abstract Presented is an implemented program understanding system called CAN. CAN relies on a meta-interpretation process uhich brings to light tuo neu concepts concerning meta-interpretation of recursive programs: vicious circles and constructive i nduction. These notions express CAN's ability to extract from program code classes of data for uhich interpretation of the code uould not stop, and in general, to relate classes of data uith abstract values and environments. ## Full text ## 1. INTRODUCTION Works on program veri f i~at ion £101 £131 have brought many useful techniques for provin~ properties of programs, but all the lmplementeo sys tems uhich derived from them uere to be used by expert mathematicians rather than expert progr ammer s. That is, those systems may do nothing uith a program on its oun. They are intended to be interactively used by programmers uho are acquainted uith formal specifications manipulations and uho understand their programs. Recent uorks on program understanding have demonstrated the need of domain dependent knou ledge [71 [151 and other types of pragmatic knouledge [191 [201. Houever, systems in these areas are not equally efficient. More prec isely, t'le systems uhich support these works may fail on simple tasks uhich are beyond the scope of their effective specificity. That is, their domain of application is far from fit t ing uith uhat an expert programmer uould consider as "simple", or "visually under s tandable" . CAN is a pouerful tool for such systems s ince : - I t understands t r ad i tionnal under standing lmprovemen t) programs independently of applications for (verification, correction, - It is particularly uell su i ted for extracting on its oun only uhat is "visually understandable" in a program. Th is pr~vents CAN from gett ing stuck on intricate problems. This is a necessity if CAN is expected to be a tool for problem solvers. A part of CAN has been especially developed for the visual understanding of programs uhich manipulate flat lists. CAN meta-interprets program bodies in abstract environments [1 1 [21 [41 [51 [91 £141 £191 [211 . We use conceptual representations £211 in order to represent abstract values of program variables and relations among them. Our conceptual representations are either pat\nrns, or predicate-style assertions uhich may not be translated into patterns. Our patterns involve element-type and segment-type variables. segment-type variables include index mathematical notations for flat lists. They also involve auto-references. Conceptual representation of meanings is our bypass of the traditionnal "set of properties". Conceptual representations may be confronted and compared more easily than assertions, most often uith unification procedures, uh ich y ield va luable and non-tr ivial information [61. CAN involves a sophisticated unification prn=ess of conceptuaL representations. ## 2. META-INTERPRETATION When confronted uith LISP code, the meta-interpreter most often faces the case uhere a funct ion is applied on its arguments. The meta-interpretation of <F A1 A2 ··· An) invo lves the follou ing steps : first, CAN meta-interprets each of the Ais which should be evaluated on a simple interpretation. this yields a set of possible abstract values and environments for each Ai. Second, CAN confronts each combination of these values and environments with F's CAN definition. After this confrontation, CAN knows: - What conditions must hold on the Ais and the e~vironment so that F may apply - which features of the abstract values and the environment are relevant for the contruction of F's abstract value and ..; ide-effects. Third, CAN propagates this information over the current environment and on the "prototype" abstract value which is part of F's CAN definition. LISP functions within CAN. definitions of functions: are conceptually defined [21J Here are the conceptual the CAR, COR and MEMBER ("!"denotesan element variable and"?" a segment variable) That is, the CAR function returns tbe first element of a list, the CDR function returns the list without its first element. (MEMBER X Y> tests wether the element X is contained in the list Y, at the top-level. If it is the case, MEMBER returns the part of the list which starts from the first occurence of X. CAN also handles the cases where F is a control structure, a functional variable, an escape label, or en unknown atom. The mete-interpretation of a LISP program is expected to yield a conceptual representation of its meaning. Example: Suppose that F is MEMBER, and that the meta-interpretation of its tuo arguments gave the two abstract values: (on !1 !2) and (?3 ! 1). The application of MEMBER on "(on !1 !2)" end "(?3 !1)" amounts to checking whether the list (?3 !1) contains the structure (on !1 !2). The confrontation of these values wlth MEMBER's prototype values is performed by e unification process of conceptual representations [6]. since ! 1 in (?3 ! 1) may not contain (on ! 1 ! 2). The propagation of this information on the prototype value (!x ?b) of MEMBER gives the returned abstract value: «on !1 !2) ?b1 !1>. This value is still functionally related to the environment since ?3 is also replaced in the environment by what it is associated to. The reader is invited to perform the same task for the second rule of MEMBER's definition. ## 3. UNIFICATION QE CONCEPTUAL REPRESENTATIONS The problem ls, given tuo conceptual representations, to find the complete set of l ts unifiers (it's most general unifier [16] [17] [18]). For theorem proving purposes, The task of unification may be limited to checking wether two s trliC tures can fit or not [llJ · In that case, it suffices to find one unifier or show that there is none. Rather, CAN needs a conceptual representation of the complete set of unifiers of tuo conceptual representations, since it needs to know not only if they fit together, but under what exact constraints [5]. In the case where segment variables are restricted to ?-type variables (that is, when index notations are excluded), the problem amounts to solve an equation in a free monoid with a neutral element (the empty sequence). Our implemented unifier exhibits about the same performances as [161 and [171 (the neutral element makes very feu differences). It involves too the algorithm for A-C Unification [12] [18] and a splitting algorithm [17] extended for index mathematical notations. What is neu within CAN's unification procedure concerns the unification of patterns which include index notations, auto-references, element-type variables with restricted domain, end negation. A detailed description of its actual performances is given in [6]. ## 4. META-INTERPRETATION QE RECURSIVE PROGRAMS ITERATIVE At some stage of the process, the following program: ## is transformed into: This says among other things that if MEMBER's first argument is different from the CAR of its second argument, then the value is the recursive call: <MEMBER !x (?b)), If CAN were to go on like previously, it would confront the arguments !x end (?b) with each of the three cases. In fact, this is exactly what CAN will do, but more carefully, so as to avoid looping forever. Appli cation of rule 3 on !x and (?b) needs the following preconditions: ![Image](https://ijcai.org/proceedings/1979/fulltext/237/image_000000_9296ae0f9845e67a18f6b80b2110448bc1d7f47aa835416f4c718815ac83c8c4.png) in which case the value is (MEMBER !x' (?b')), But this is what CAN was meta-interpreting (modulo a c~ge of the variables'name). We consider ~ as a "vicious circle". The meta-interpretation process stops at each vicious circle, and CAN "multiplies" it by a ficti ve number n of recursions. From@, CAN is able to obtain abstract representations of flat lists: This says that if the second argument of MEMBER is a list whose n first elements are different from its first argument, then they will be deleted after the nth recursive call. The meta- interpreter will then go on with the two first rules of MEMBER, and obtain the final conceptual representation of MEMBER which we used in the second paragraph. The concept of vicious circle is important since it does n~t coincide with the first recursive call in a program. For the following example: the meta-inlerpreter will never reach a vicious circle , and yield the final conceptual representation: (under lined variables may not be assigned the NIL value) ## 5. VICIOUS CIRCLES A vicious circle is encountered when the meta-interpretation of some form f in an environment El leads to the meta-interpretation of f in an environment E2 such that El and E2 "may be identified". Formally, the two environments will be identifiable if their unification gives a unifier which contains no "transmitter". A transmitter is a couple of variables bindings of the form: With the restriction that if f(v2) contains vl and H contains v2, the couple is considered as a vicious circle. Here are some examples of LISP programs where the first recursive call does not coincide with a vicious circle: <DE FOP <X Y> <FOO Y X>> <DE FOP <L M> <IF <NULL L> NIL <FOO <CDR M> <CONS <CAR M> U > > > 6. CONSTRUCTIVE INDUCTION <multiplication by nnu) The notion of VlClOUS circle is motivated by the fact that if a substitution (unifler) is a vicious circle, it may be "multiplied by n" by a simple algorithm (i.e its general form after "n" recursive calls may be constructed). From a variable binding of the form: v · f(v) the algorithm will obtain: (* v n f{v)) which may be seen as a complex variable whose name is v and f(v) is a conceptual representation with auto- references (everywhere v is). In other words, f(v) restricts v's domain. "n" names the fictive number of successive recursive calls. It relates different complex variables to each other. In some cases, the induction algorithm may generate mathematical index notations such as those involved in MEMBER's CAN definition, instead of conceptual representations with auto-references. i.e in the case: the algorithm will obtain: (where -A­ conceptual and -B- are any sequence of representations. They may involve indexed elements and even sequences length depend on the index) whose The advantage is that the unification process of conceptual representations is particularly well suLted for the unification of such forms. ## 7. RECURS IV IIY From the program: <DE VECMAT <L Ml <IF <NULL U M <DCONS <CAR L) <VECMAT <CDR Ll (CONS NIL Ml)))) The meta-interpreter will get: Recursivity will be handled by the same processes. yields a vicious algorithm is applied. circle, the induct ion here, from: By propagation and with the initialisation: (the right conceptual representation is the abstract value of M when case 1 is encoutered. The initialisation is performed via the unification of the two conceptual representations and propagation of the results.) CAN finally obtains the conceptual representation of vecmat: where CAN gets: ## 8. TERMINATION The meta-interpretation of a program yields a set of rules which contain recursive calls, as a first approximation. As was shown, the same meta-interpretation process may be pursued. So CAN may find which rules data can "go" to, wh~n "coming out" of a recursive rule. That is find which rules refer to which rules. !f'a recursive rule refers only to itself, or if a group of rules which refer to one another refers to no rule "outside", then a class of data is determined for which simple interpretation of the program never ends. Here are some simple examples: example 1: ## CAN yields: !List !b)·!List <FOO !atom ! list) m ! list (FOO <FOO !atom1 !atom2) · infinite- loop example 2: CAN yields: example 3: ## CAN yields: (underlined variables may not be replaced by the Nl .L value) Here is an example of a different kind: <DE FOO <L M> (IF <EQUAL L M> T (FOO <CDR L> <CONS <CAR L> M>>>> ## CAN yields: For this last example, CAN is not able to explicitly describe the class of data for which there ls lnfinlte computation. It is implicitly defined by the set of cases which do not f i t the rules above, plus those which flt the second rule. ## 9. ~ CAN;\_ ASSI STANT. INTERACT! VE PROGRAMMER CAN ls an interactive program understanding sys t em. When CAN ls run, the user may type in LISP functions, or LISP expressions. When an expr ession ls typed in, CAN gives its abstract value. There may be several cases. If the expression is <ATOM X> for instance, CAN will respond: CASE 1: X· !atom1 VALUE: t CASE 2: X=!1 atom1 VALUE: nil The user can focus on any of the cases or keep them a ll. A pract leal use of the CAN system, then, is the fol lowing: the user first types in a program he has just written. Once the program LS unders tood by CAN, the user may type in any LISP express ion involving calls to the program. He wi ll get the corresponding abstract va lues. Note that CAN ls a s lmpllfler. That is, lf i t is not able to understand an expression E, E's abstract value ls E itself (with an impl ic i t met a- evaluation request). In other words, E may not be simplified further. If the expression is an assertion about the program, it may meta-evaluate to T or NIL, but CAN's performances ln this domain still ra ise the need for a theorem prover. One common use is to type a call to t he program on res tr icted classes of data. i.e i f the program has name FOO and argument X, the user may define a unary LISP predicate P wh ich is true for a restricted class of X's, then focus on the cases where (p X) may evaluate to T, and ca ll <FOO X> · For instance, lf FOO is in fac t a pattern- matching function MATCH wi th back-referenc ing (two occurences of the s ame variable must be assigned the same value) and the user wants to test wether back-referencing works fine, he may first build several kinds of abstract values for MATCH's arguments by the "focus on" technique described above, and then call MATCH on them One future work will be to develop a system for proving theorems about list structures by structural induct ion, which uses CAN as a simplification sub-system. We expect that CAN will greatly help the task of proving theorems by structural induc t ion since, for instance, many of the LISP theorems proved in [221 already meta-evaluate to the LISP truth-value T when given to CAN. ## 1 0. CONCLUSION We have designed a system whose job is to understand what an expert programmer could consider as "visually understandable". CAN does no problem solving. CAN's meta-interpretation process is straightforward, and simple interpretation is a simple case of meta-interpretation [5]. We then· th ink that CAN should be put in the service of eMpert programmers, or program understanding systems which would be specialised in narrow areas, since conceptual representations are much more easily manipulated than LISP code, for instance. It may effectively be expected that the size of program understanding systems is directly related to the number of ways of representing a relation with in a programming language. The CAN system is written in VLISP-10 [3] [8] and occupies about 20K words.