Program Understanding with the Lambda Calculus

PROGRAM UNDERSTANDING WITH THE LAMBDA CALCULUS

Stanley Letovsky Department of Computer Science Yale University New Haven, CT 06520

some sort augmented with pattern-matching variables. Plane are represented as incomplete programs, with variable parts. This approach lends itself well to syntactic matching on programs written in the base programming language, but the reasoning is subject to various types of errors, because the syntactic pat­ tern matching can generate semantic nonsense. In particular, schema variables can be instantiated with code segments which destroy the dataflow relationships &BIIumed by other parts of the schema.

ABSTRACT

A prerequisite of any attempt to build intelligent tools to as­ sist in the programming process is a representation language for encoding programming knowledge. Languages that have been used for this purpose include the predicate calculus [5] and var­ ious program-schema languages [1,4]. This paper advocates a new candidate which is as expressive as the predicate calculus but more intimately connected with programming: the lambda calculus. Its advantages lie in its close resemblance to conven­ tional programming languages, and in a straighforward model of inference by rewriting, which can be applied to automatic pro­ gramming and program understanding. The use of the lambda calculus in an automatic program understander is described.

I INTRODUCTION

The general goal of research in AI/Software Engineering (AI/SW) is to construct tools which automate aspects of the software development proce811 that are presently carried out by expert programmers. Such tools need knowledge bases which encode the expertise currently pOBBessed only by programmers. One important category of programming knowledge is the stan­ dard plans of programming: this category includes algorithms, data structures and associated operations, and simple cliches such as summing and counting. This paper describes an ap­ proach to notating these plane, and to performing mtichanical inference with them.

n METHODS OF REPRESENTING PLANS

One might think that a programming language would suffice to notate the plans used by programmers: after all, program­ ming languages are languages for notating programming knowl­ edge. There are two problems with this idea. First, the syntax and semantics of programming languages tends to be rather too clunky and complex for the needs of mechanical inference. More importantly, the types of composition of concepts supported by programming languages, via language constucts such as subrou­ tines, packages, abstract data types, or objects, correspond to only a subset of the ways that concepts can combine in a pro­ grammer's mind.

These limitations on the expressivity of programming lan­ guages have led AI/SW researchers to use more expre118ive lan­ guages for writing down the knowledge. These include a vari­ ety of program schema languages and the predicate calculus. A schema language (eg.,[4,1]) is usually a programming language of Another approach is to r~present the knowledge in the pred­ icate calculus (PC). This method requires a PC representation of the semantics of the target programming language: axioms which state how variables behave, what conditionals do, and so forth. These axioms can be used to translate programs into com­ plex assertions which decribe the behavior of the program. Plans can also be represented by complex axioms. [5,6] Problems with this approach are first, the difficulties of doing general purpose mechanical inference in the predicate calculus, and second, the unreadability of PC translations of programs. This unreadabil­ ity makes it hard for programmers or designers of knowledge­ based tools to write knowledge bases or to follow intermediate stages of a tool's reasoning.

1 Thia research waa aupported by NSF under IST grant #8505019.

In the remainder of the paper I describe another approach to representing programming knowledge using the lambda calculus (.>.C). The lambda calculus posessee both the semantic precision missing from the schema languages and the readability and ease of inference missing from the predicate calculus. It has been my experience in conctructing a series of prototype program analyzers based on each of the above types of representations that the lambda calculus lends itself far more easily than the other two candidates to the development of simple and powerful inference tools.

m THE LAMBDA CALCULUS

The lambda calculus is basically an idealized programming language. It was invented by Church [3] to analyze the mathe­ matical underpinnings of computation. Since then it has been used to analyze the semantics of programming languages [9] and as t?e explicit model for several programming languages, in­ cludmg LISP, and more recently T [7] and Scheme [8] . The .>.-calculus is a language of functional expressions over a set of symbols, eg., (+ 1 3) or (f x), together with .>., an operator for creating functions. For example, (.>.(x) (+ x 1)) denotes a function which adds 1 to its ar~tument.

The two most important kinds of inference in .>.C are .>.­ abstraction and its opposite, P-reduction.

(+ 2 1) ~ ((.>.(x)(+ x 1)) 2)

P-reduction ~ .>.-abstraction Abstraction creates new functions, whereas ,8-reduction simpli­ fies functions away. Interpreters for ~C-based languages perform simulated ,8-reduction, usually augmented with primitive arith­ metic procedures and the like. Compilers are also largely based on ,8-reduction. Abstraction, by contrast, has little mechanical application at present; constructing abstractions is the busine· of programmers. The program analyzer developed by the author relies heavily on ~-abstraction for understanding programs.

It should be noted that parameters of ~-expressions play a role analogous to schema variables of schema languages, and to universally quantified variables in the predicate calculus. The ~-calculus is expressive enough to represent all quantification; no additional constructs are needed [2] .

IV PROGRAM ANALYSIS IN THE ~-CALCULUS

In reasoning about programs, two important tasks are pro­ gram analysis and synthesis, which are the analogs of classical AI models planning and understanding in the programming do­ main. In these models a planner or understander has a knowl­ edge base of plan· which are used to solve a given problem or analyze a given solution. Planning consists of replacing (or ex­ panding) top level goals with selected plans from the knowl­ edge base. Understanding is the opposite process: a set of ob­ served actions is identified as being an instance of some library plan. Both the planning and understanding processes produce the same final data structure: a hierarchical representation of the design of a program. The top layer of this hierarchy is called the apecifiC4tion, the bottom layer is the code.

In the author's program analyzer, the code, plans, and spec­ ifications are all represented using ~C. The code and specifica­ tions are both sets of function definitions, which are semanti­ cally equivalent for a correct program. The design hierarchy is represented as a set of ~C rewritings which transform one to the other. This section briefly describes the techniques used to represent code, specs, and plans, and the inference mechanisms used in analysis.

A. Representing Code

Representing code in ~C requires a translation procedure from the target language into ~C; because of ~C's similar­ ity to programming languages, such translation is not difficult. Loops are represented by recursions; GOTO'e by funct1on calls as described in [8] . Imperative language constructs related to dataflow by side effect, such as reference or assignment to vari­ ables, pose a more difficult problem. Memory allows causal ef­ fects to propagate during program execution in a way which the notation refleets only implicitly; to understand what is going on in such programs an analyzer needs to make the flow of data through memory explicit so it can be reasoned about. In the analyzer this is done by translating the imperative code into ~C-expressions which represent memory explicitly, an approach which is sometimes used in the analysis of programming lan­ guage semantics [9] . Memory is viewed as a function from point­ era to values. Pointers are arbitrary objects: symbols, say, or numbers. States of memory will be represented by ~-expressions of the form:

(A (pointer) (if (· pointer pointer1) value1 (if (· pointer pointer2) value2) ... ))

which I will refer to as M-ezpre88iona. The value of a pointer in some state (i.e., a variable reference) is found by applying theM­ exprelllion for that state to the pouiter. Functions which depend on state must take an M-expression as an argument; action· which modify state must take an M-expression as an argument and return one. Actions are thus functions from states to states.

Within this framework &SIIignment is defined as followe: (define ( :· loe M value)

(A (pointer)

(if (· pointer loe) value (M pointer))))

The function : · takes 3 arguments rather than the usual 2: the extra argument M is theM-expression describing memory juat prior to the a~~~ignment. : · returns a new M-expression which describes the state of memory after the &~~~ignment.

As an example, consider a program to compute the triangle of a number n, that is, the sum of the integers from 1 through n. In FORTRAN, it would look something like this:

100

subroutine TliANOLE ( n , anawer) answer · 0 do 100 i · 1,n return end anawer · anawer + i

The translation of this into ~C is as follows. Symbols beginning with M are M-expressions.

(define (triansle NO n anawer) (define (do-loop M) (if(> (N i)(N n)) N (let ((N1 (:· anawer N (+ (N anawer) (N i))))) (let ((N2 (:· i N1 (+ (N1 i) 1)))) (do-loop N2))))) (triangle1 ( :· i ( :· anawer M 0) 1)) )

Notice the way consecutive assignments get transformed to nested leta or aeta; this pattern replaces the statement-block constructe of conventional languages. I111ues relating to the scop­ ing of the variable 1 are ignored here in the interests of brevity.

B. Analyzing Code

The goal of analysis is to recognize code in terms of standard plans. Analysis may thus be viewed as a proce· of factrring nt known plans from a given program, or rewriting the program in the moet concise p0111ible form, using standard plans in the knowledge base. Several types of rewritings are used in the course of analysis:

Knowledge-Based ~-Abstraction: The knowledge base contains definitions of standard plans, data objects and algo­ rithms. When a subexpression of the target program matchea the body of auch a definition, the aubexpression is replaced by a call to the library function, with arguments dervied from the match bindings. So for example, if the knowledge base contains the definition ·

(define add1 (~ (x)(+ x 1)))

then knowledge-based abstraction entitles us to rewrite the ex­ pression ( + a 1) to (add1 a) .

Rewrite Rulea: The knowledge base contains rewrite rulea of the general form

(~ (param.) llu} ~ (~ (param.) rlu)

which encode a variety of simplifications and theorems. When a code subexpression can be parametrized to match IM, it is rewritten to the rha form.

,8-Reduction: Used to simplify the target program in a variety of ways so that other kinds of analysis can proceed. In particular, reduction of complex M-expressions simplifies away dataflow through memory.

Recursion Ell.mination: The simple methods just de­ scribed fail on recursive definitions, because recursive defini­ tions can occur in arbitrarily many syntactic forms, and it is not feasible to anticipate each of these forms in the plan library. Recursion elimination transforms a recursive definition into an equivalent definition which is expressed in terms of operations on streams of data values - the sequence of values taken on by the loop variables during loop execution. Definitions expre88ed in this form can be further analyzed using the above methods.

The recursion elimination transformation is a ).Q adapta­ tion of a technique developed by Waters [10] to analyze loops in the plan calculus. He showed that most loops can be viewed as compositions of a few primitive looping plans: enumerators, accumulators, filters, terminators, and maps. These plans can be viewed as operations on streams of data. For example, an enumerator generates a stream by repeatedly applying an op­ eration to the previous element in the stream: an example is counting, which enumerates using the add1 operation, starting with 1 as an intial value. A running total is an accumulation with the operator +; accumulation is the same as APL's acan operator.

In the·analysis of TRIANGLE, a few applications of ,8-reduction simplify the body of the do-loop subdefinition significantly. In the resulting definition, the argument to the recursive call is a simple M-expression which specifies the values of each loop variable at the end of each iteration as a function of the values at the start of the iteration. The recursion elimination algorithm is applied to definitions of this form. Space constraints permit only a brief sketch of the algorithm.

The first step is to construct aemi-ateam expressions for each loop variable: these are the potentially infinite (aem .. finite) streams of values which each variable would take on if the loop never terminated. The semi-stream expressions are formed from the basic looping plans, plus fragments of the original definition, .>.-abstracted according to the pattern of interdependence among the variables. For the d~loop in TRIANGLE, the semi-streams are:

(define i-·eai- ·treaa

(enumerate (). (a)(+ a 1)) (M i))) (define an·wer- ·emi-·treaa

(accumulate + (M anewer) i - ·eai- ·tream))

These semi-streams must be truncated as dictated by the exit teste to yield streams. Each semi-stream must be truncated once for each exit test. There are two basic truncate operations: truncate and extrude. Truncate truncates a stream at the point where a predicate is satisfied, while extrude extrudes a stream to a specified length. Variables which are not explicitly tested by an exit test are extruded up to a length determined by the variables which are tested. The predieates supplied to these operations are formed by .>.-abstracting the exit tests in the original definition. The streams for do-loop are:

(define i-·treaa (truncate (). (a)(> a (M n))) i-·emi-·tream)) (define an·wer-·treaa (extrude (length i-·tream) an·wer-·emi-·tream))

A new nonrecursive definition is constructed from these ele­ ments, in which each loop variable is set to the last element of its corresponding stream.

(define (do-loop M) ( :· i ( :· an·wer M (la·t anewer-·tream)) (la·t i - ·tream)))

Application of the other rewrite methods can then proceed until the following specification is produced for the original program: (define (triangle M n answer)

( :· anewer M (·ua (integer·-between 1 n))))

V CONCLUSIONS

The .>.-calculus is a useful vehicle for encoding the planning knowledge needed by intelligent programming tools. An impor­ tant strength of the language is the existence of a notation which is similar to conventional programming languages, but more ex­ pressive and more amenable to machine manipulation. A pr~ gram analyzer based on these ideas has been constructed which is currently able to transform simple programs into compositions of standard plans.