Any expression M in ULC (the untyped λ-calculus) can be compiled into a rather low-level language we call LLL, whose programs contain none of the traditional implementation devices for functional languages: environments, thunks, closures, etc. A compiled program is first-order functional and has a fixed set of working variables, whose number is independent of M. The generated LLL code in effect traverses the subexpressions of M.

How to construct a general program obfuscator? We present a novel approach to automatically generating obfuscated code P2 from any program P whose source code is given. Start with a (program-executing) interpreter interp for the language in which P is written. Then "distort" interp so it is still correct, but its specialization P2 w.r.t. P is transformed code that is equivalent to the original program, but harder to understand or analyze. Potency of the obfuscator is proved with respect to a general model of the attacker, modeled as an approximate (abstract) interpreter. A systematic approach to distortion is to make program P obscure by transforming it to P2 on which (abstract) interpretation is incomplete. Interpreter distortion can be done by making residual in the specialization process sufficiently many interpreter operations to defeat an attacker in extracting sensible information from transformed code. Our method is applied to: code flattening, data-type obfuscation, and opaque predicate insertion. The technique is language independent and can be exploited for designing obfuscating compilers.

In this paper, we provide an improved basis for the "distillation" program transformation. It is known that superlinear speedups can be obtained using distillation, but cannot be obtained by other earlier automatic program transformation techniques such as deforestation, positive supercompilation and partial evaluation. We give distillation an improved semantic basis, and explain how superlinear speedups can occur.

We present a method for certifying that the values computed by an imperative program will be bounded by polynomials in the program's inputs. To this end, we introducemwp-matrices and define a semantic relation ⊧ C :M, where C is a program andMis anmwp-matrix. It follows straightforwardly from our definitions that there existsMsuch that ⊧ C :Mholds iff every value computed by C is bounded by a polynomial in the inputs. Furthermore, we provide a syntactical proof calculus and define the relation ⊢ C :Mto hold iff there exists a derivation in the calculus where C :Mis the bottom line. We prove that ⊢ C :Mimplies ⊧ C :M. By means of exhaustive proof search, an algorithm can decide if there existsMsuch that the relation ⊢ C :Mholds, and thus, our results yield a computational method.

A fully-automated algorithm is developed able to show that evaluation of a given untyped lambda-expression will terminate under CBV (call-by-value). The ``size-change principle'' from first-order programs is extended to arbitrary untyped lambda-expressions in two steps. The first step suffices to show CBV termination of a single, stand-alone lambda;-expression. The second suffices to show CBV termination of any member of a regular set of lambda-expressions, defined by a tree grammar. (A simple example is a minimum function, when applied to arbitrary Church numerals.) The algorithm is sound and proven so in this paper. The Halting Problem's undecidability implies that any sound algorithm is necessarily incomplete: some lambda-expressions may in fact terminate under CBV evaluation, but not be recognised as terminating. The intensional power of the termination algorithm is reasonably high. It certifies as terminating many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's ``minimum'' algorithm. Further, our type-free approach allows use of the Y combinator, and so can identify as terminating a substantial subset of PCF.

Recent research suggests that the goal of fully automatic and reliable program generation for a broad range of applications is coming nearer to feasibility. However, several interesting and challenging problems remain to be solved before it becomes a reality. Solving them is alsonecessary,if we hope ever to elevate software engineering from its current state (a highly developed handiwork) into a successful branch of engineering, capable of solving a wide range of new problems by systematic, well-automated and well-founded methods.A key problem in all program generation isterminationof the generation process. This article focuses on off-line partial evaluation and describes recent progress towards automatically solving the termination problem, first for individual programs, and then for specializers and “generating extensions,” the program generators that most offline partial evaluators produce.The technique is based onsize-change graphsthat approximate the changes in parameter sizes at function calls. We formulate a criterion,bounded anchoring,for detecting parameters known to be bounded during specialization: a bounded parameter can act as ananchorfor other parameters. Specialization points necessary for termination are computed by adding a parameter that tracks call depth, and then selecting a specialization point in every call loop where it is unanchored. By generalizing all unbounded parameters, we compute a binding-time division which together with the set of specialization pointsguaranteestermination.Contributions of this article include a proof, based on the operational semantics of partial evaluation with memoization, that the analysis guarantees termination; and an in-depth description of safety of the increasing size approximation operator required for termination analysis in partial evaluation.Initial experiments with a prototype shows that the analysis overall yields binding-time divisions that can achieve a high degree of specialization, while still guaranteeing termination.The article ends with a list of challenging problems whose solution would bring the community closer to the goal of broad-spectrum, fully automatic and reliable program generation.

Recent research suggests that the goal of fully automatic and reliable program generation for a broad range of applications is coming nearer to feasibility. However, several interesting and challenging problems remain to be solved before it becomes a reality.We first discuss the relations between problem specifications and their solutions in program form, and then narrow the discussion to an important special case: program transformation. Although the goal of fully automatic program generation is still far from fully achieved, there has been some success in a special case: partial evaluation, also known as program specialization.A key problem in all program generation is termination of the generation process. This paper (See the GPCE'02 proceedings for the full paper.} describes recent progress towards automatically solving the termination problem, first for individual programs, and then for specializers and "generating extensions," the program generators that most offline partial evaluators produce.

Many classical compiler optimizations can be elegantly expressed using rewrite rules of form: I ⇒ I ′ if φ , where I , I ′ are intermediate language instructions and φ is a property expressed in a temporal logic suitable for describing program data flow. Its reading: If the current program π contains an instruction of form I at some control point p , and if flow condition φ is satisfied at p , then replace I by I ′.The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations, dead code elimination, constant folding and code motion. The meaning of correctness is that for any program π, if Rewrite (π, π′, p , I ⇒ I ′ if φ) then [[π]] = [[π′]], i.e. π and π′ have exactly the same semantics.

Recent research suggests that the goal of fully automatic and reliable program generation for a broad range of applications is coming nearer to feasibility. However, several interesting and challenging problems remain to be solved before it becomes a reality. .We first discuss the relations between problem specifications and their solutions in program form, and then narrow the discussion to an important special case: program transformation. Although the goal of fully automatic program generation is still far from fully achieved, there has been some success in a special case: partial evaluation, also known as program specialization.A key problem in all program generation is termination of the generation process. This paper describes recent progress towards automatically solving the termination problem, first for individual programs, and then for specializers and "generating extensions," the program generators that most offline partial evaluators produce.

The "size-change termination" principle for a first-order functional language with well-founded data is: a program terminates on all inputs if every infinite call sequence (following program control flow) would cause an infinite descent in some data values.Size-change analysis is based only on local approximations to parameter size changes derivable from program syntax. The set of infinite call sequences that follow program flow and can be recognized as causing infinite descent is an ω-regular set, representable by a Büchi automaton. Algorithms for such automata can be used to decide size-change termination. We also give a direct algorithm operating on "size-change graphs" (without the passage to automata).Compared to other results in the literature, termination analysis based on the size-change principle is surprisingly simple and general: lexical orders (also called lexicographic orders), indirect function calls and permuted arguments (descent that is not in-situ) are all handled automatically and without special treatment, with no need for manually supplied argument orders, or theorem-proving methods not certain to terminate at analysis time.We establish the problem's intrinsic complexity. This turns out to be surprisingly high, complete for PSPACE, in spite of the simplicity of the principle. PSPACE hardness is proved by a reduction from Boolean program termination. An ineresting consequence: the same hardness result applies to many other analyses found in the termination and quasitermination literature.

Compare first-order functional programs with higher-order programs allowing functions as function parameters. Can the the first program class solve fewer problems than the second? The answer is no: both classes are Turing complete , meaning that they can compute all partial recursive functions. In particular, higher-order values may be first-order simulated by use of the list constructor ‘cons’ to build function closures. This paper uses complexity theory to prove some expressivity results about small programming languages that are less than Turing complete. Complexity classes of decision problems are used to characterize the expressive power of functional programming language features. An example: second-order programs are more powerful than first-order, since a function f of type [Bool]-〉Bool is computable by a cons-free first-order functional program if and only if f is in PTIME , whereas f is computable by a cons-free second-order program if and only if f is in EXPTIME . Exact characterizations are given for those problems of type [Bool]-〉Bool solvable by programs with several combinations of operations on data: presence or absence of constructors; the order of data values: 0, 1, or higher; and program control structures: general recursion, tail recursion, primitive recursion.

Using a simple programming language as a computational model, Neil Jones has shown that a constant-factor time hierarchy exists: thus a constant-factor difference in time makes a difference in problem-solving power, unlike the situation with Turing m

Abstract We introduce a positive supercompiler , a version of Turchin's supercompiler maintaining only positive information during transformation, and using folding without generalization. The positive supercompiler can also be regarded as a variant of Wadler's deforestation maintaining an increased amount of information. We compare our algorithm to deforestation and, in less detail, to partial evaluation, Turchin's supercompiler, Generalized Partial Computation (GPC), and partial deduction by classifying these transformers by the amount of information they maintain during transformation. This factor is significant, as a differentiating example reveals: positive supercompilation, Turchin's supercompiler, GPC and partial deduction can specialize a general pattern matcher with respect to a fixed pattern to obtain an efficient matcher very similar to the Knuth–Morris–Pratt algorithm. Deforestation and traditional partial evaluation achieve this effect only after a non-trivial hand rewriting of the general matcher.

The first article reporting a running nontrivial self-applicable

Logic-programming languages are based on a principle of separation “logic” and “control.”. This means that they can be given simple model-theoretic semantics without regard to any particular execution mechanism (or proof procedure, viewing execution as theorem proving). Although the separation is desirable from a semantical point of view, it makes sound, efficient implementation of logic-programming languages difficult. The lack of “control information” in programs calls for complex data-flow analysis techniques to guide execution. Since data-flow analysis furthermore finds extensive use in error-finding and transformation tools, there is a need for a simple and powerful theory of data-flow analysis of logic programs. This paper offers such a theory, based on F. Nielson's extension of P. Cousot and R. Cousot's abstract interpretation . We present a denotational definition of the semantics of definite logic programs. This definition is of interest in its own right because of its compactness. Stepwise we develop the definition into a generic data-flow analysis that encompasses a large class of data-flow analyses based on the SLD execution model. We exemplify one instance of the definition by developing a provably correct groundness analysis to predict how variables may be bound to ground terms during execution. We also discuss implementation issues and related work.

The constant speedup theorem, so well known from Turing machine based complexity theory, is shown false for a natural imperative programming language I that manipulates tree-structured data. This relieves a tension between general programming practice, where linear factors are essential, and complexity theory, where linear time changes are traditionally regarded as trivial. Specifically, there is a constant b such that for any a > 0 there is a set X recognizable in time a · b · n but not in time a · n. Thus LIN, the collection of all sets recognizable in linear time by deterministic I-programs, contains an infinite hierarchy ordered by constant coefficients. Constant hierarchies also exist for larger time bounds T (n), provided they are time-constructable. Second, a problem is exhibited which is complete for the nondeterministic linear time sets NLIN with respect to a natural notion of deterministic linear-time reduction. Third, Kleene’s Second Recursion Theorem in essence shows that for any program p defined with self-reference, there is an equivalent nonreflexive program q. This is proven for an extension I↑ of I. Further, q can be simulated by an I program at most constantly slower than p. Language I↑ allows calls to the language’s own interpretation function, and even to its running time function (without the usual high costs for nested levels of interpretation). The results all hold as well for a stronger language I allowing selective updating of tree-structured data. The results are robust in that classes LIN and NLIN are identical for I , Isu↑, Schonhage’s Storage Modification Machines, Knuth/Tarjan’s pointer machines, and successor RAMs [13,14,11]. where n is the size of the input. DIKU, Department of Computer Science, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen East, Denmark, E-mail: [email protected]. If the “more realistic and precise measure” of SMM computation time is used [13], and similarly for the other models.

Abstract This article describes theoretical and practical aspects of an implemented self-applicable partial evaluator for the untyped lambda-calculus with constants and a fixed point operator. To the best of our knowledge, it is the first partial evaluator that is simultaneously higher-order, non-trivial, and self-applicable. Partial evaluation produces a residual program from a source program and some of its input data. When given the remaining input data the residual program yields the same result that the source program would when given all its input data. Our partial evaluator produces a residual lambda-expression given a source lambda-expression and the values of some of its free variables. By self-application, the partial evaluator can be used to compile and to generate stand-alone compilers from a denotational or interpretive specification of a programming language. An essential component in our self-applicable partial evaluator is the use of explicit binding time information. We use this to annotate the source program, marking as residual the parts for which residual code is to be generated and marking as eliminable the parts that can be evaluated using only the data that is known during partial evaluation. We give a simple criterion, well-annotatedness, that can be used to check that the partial evaluator can handle the annotated higher-order programs without committing errors. Our partial evaluator is simple, is implemented in a side-effect free subset of Scheme, and has been used to compile and to generate compilers and a compiler generator. In this article we examine two machine-generated compilers and find that their structures are surprisingly natural.

Data or program flow analysis is concerned with the static analysis of programs, to obtain as much information as possible about their possible run time behavior without actually having to run the programs. Due to the unsolvability of the halting problem (and nearly any other question concerning program behavior), such analyses are necessarily only approximate whenever the analysis algorithm is guaranteed to terminate. Further, exact analysis may be impossible due to the lack of knowledge of input data values, so the analysis can at best yield information about sets of possible computations.

A new approach to data flow analysis of procedural programs and programs with recursive data structures is described. The method depends on simulation of the interpreter for the subject programming language using a retrieval function to approximate a program's data structures.

In [Math. Systems Theory, 13 (1979), pp. 29–43], the authors obtained a number of upper and lower bounds for various problems concerning L-systems. In most cases the bounds were rather close; however, for general $D0L$ membership the upper bound was $\mathcal{P}$, and the lower was deterministic log space. In this note we show that membership can be decided deterministically in $\log ^2 n$ space, which makes it very unlikely that the problem is complete for $\mathcal{P}$. We also show that nonmembership is as hard as any problem solvable in nondeterministic log n space. This is an improved lower bound unless ${\textbf{DSPACE}}(\log n) = {\textbf{NSPACE}}(\log n)$, which is also thought to be very unlikely.

Two different methods of flow analysis are discussed, one a significant generalization of the other. It is shown that the two methods have significantly different intrinsic computational complexities. As an outgrowth of our observations it is shown that a feature of the programming language used by Dijkstra in A Discipline of Programming makes it unsuitable for compile-time type checking, thus suggesting that flow analysis is applicable to the design of programming languages, as well as to their implementation. It is also shown that program verification by the method of inductive assertions is very likely to lead to assertions whose lengths and proofs are not polynomially bounded in the size of the program being verified, even for very simple programs. This last observation casts further doubt on the practicality and relevance of mechanized verification of arbitrary programs.

In [12] the authors introduced the concept of binding time optimization and presented a series of data flow analytic methods for determining some of the binding time characteristics of programs. In this paper we extend that work by providing methods for determining the class of shapes which an unbounded data object may assume during execution of a LISP-like program, and describe a number of uses to which that information may be put to improve storage allocation in compilers and interpreters for advanced programming languages.We are concerned chiefly with finding, for each program point and variable a finite description of a set of graphs which includes all the shapes of values the variable could assume at that point during the execution of a program. If this set is small or regular in structure, this information can be used to optimize the program's execution, mainly by use of more efficient storage allocation schemes.In the first part we show how to construct from a program without selective updating a tree grammar whose nonterminals generate the desired sets of graphs; in this case they will all be trees. The tree grammars are of a more general form than is usually studied [8, 19], so we show that they may be converted to the usual form. The resulting tree grammar could naturally be viewed as a recursive type definition [11] of the values the variables may assume. Further, standard algorithms may be employed to test for infiniteness, emptiness or linearity of the tree structure.In the second part selective updating is allowed, so an alternate semantics is introduced which more closely resembles traditional LISP implementations, and which is equivalent to the tree model for programs without selective updating. In this model data objects are directed graphs. We devise a finite approximation method which provides enough information to detect cell sharing and cyclic structures whenever they can possibly occur. This information can be used to recognize when the use of garbage collection or of reference counts may be avoided.The work reported in the second part of this paper extends that of Schwartz [17] and Cousot and Cousot [7]. They have developed methods for determining whether the values of two or more variables share cells, while we provide information on the detailed structure of what is shared. The ability to detect cycles is also new. It also extends the work of Kaplan [13], who distinguishes only binary relations among the variables of a program, does not handle cycles, and does not distinguish selectors (so that his analysis applies to nodes representing sets rather than ordered tuples).

In order to study the effects of recurston on the complexity of program analysis, a fimte memory machme wtth recurstve calls is defined, as well as two parameter passmg mechamsms whmch extend the power of the language Close upper and lower bounds on the complexity of determmmg whether a program accepts the empty language are gtven for each of the three program models It ts shown that such questtons as acceptance of the empty set, eqmvalence, and so on are retractable even for these relatively simple programs

A simple programming language which corresponds in computational power to the class of generalized sequential machines with final states is defined. It is shown that a variety of questions of practical programming interest about the language are of nondeterministic linear space complexity. Extensions to the language are defined (adding arithmetic and array data structures) and their complexity properties are explored. It is concluded that questions about halting, equivalence, optimization, and so on are intractable even for very simple programming languages.

A new approach to the design of a programming language and its processor is proposed and some of the techniques necessary to realize the design are investigated. The language would have a precisely specified syntax and semantics, with both designed to provide the programmer maximal expressive power and to be as easily understood as possible. The semantics would be based on extremely late binding times, which provide great power to the programmer and are consistent with ease of understanding of the execution process. It would be the responsibility of the processor to implement each program in the most efficient manner consistent with its being correctly executed. Implications of this design philosophy and some of the techniques to be used are discussed in greater detail, focusing particularly on data types and storage allocation.

It has long been known that most questions of interest about the behavior of programs are recursively undecidable. These questions include whether a program will halt, whether two programs are equivalent, whether one is an optimized form of another, and so on. On the other hand, it is possible to make some or all of these questions decidable by suitably restricting the computational ability of the programming language under consideration. The Loop language of Meyer and Ritchie [MR], for example, has a decidable halting problem, but undecidable equivalence. Restricting the computational ability still further, virtually all of these questions are decidable for finite automata and generalized sequential machines (except that Griffiths [Gri] has shown equivalence undecidable for nondeterministic gsms).A natural question to ask is how hard it is to solve these problems for programming languages for which they are decidable, and it is with this area that we are concerned in this paper. In particular we describe a programming language modeled on current higher-level languages which has exactly the computational power of deterministic finite state transducers with final states, and analyze the space and time required to decide various questions of programming interest about the language. We find that questions about halting, equivalence, and optimization are already intractable for this very simple language. We also study extensions to the language such as simple arithmetic capabilities, arrays, and recursive subroutines with both call-by-value and call-by-name parameter passing mechanisms, some of which extend the capabilities of the language and/or increase the complexity of its decidable problems. In one case, that of recursion with call-by-name, the previously decidable questions are seen to become undecidable.

The results of Cook and Karp ([K], [C]) aroused considerable interest for at least two reasons. First, the answer to a long-standing open question which had seemed peculiar to automata theory—whether deterministic and nondeterministic polynomial-time-bounded Turing machines are equivalent in power—was seen to be exactly equivalent to determining whether any of several familiar combinatorial problems can be solved by polynomial-time algorithms. Second, the existence of complete problems for NP1 made it possible to replace an entire class of questions by a question about a single representative.Thus all of these combinatorial and automata-theoretic problems were essentially restatements of a single problem, such as: can satisfiability of a propositional formula be decided in polynomial time.

H. Scholz [11] defined the spectrum of a formula φ of first-order logic with equality to be the set of all natural numbers n for which φ has a model of cardinality n. He then asked for a characterization of spectra. Only partial progress has been made. Computational aspects of this problem have been worked on by Gunter Asser [1], A. Mostowski [9], and J. H. Bennett [2]. It is known that spectra include the Grzegorczyk class and are properly included in . However, no progress has been made toward establishing whether spectra properly include , or whether spectra are closed under complementation. A possible connection with automata theory arises from the fact that contains just those sets which are accepted by deterministic linear-bounded Turing machines (Ritchie [10]). Another resemblance lies in the fact that the same two problems (closure under complement, and proper inclusion of ) have remained open for the class of context sensitive languages for several years. In this paper we show that these similarities are not accidental—that spectra and context sensitive languages are closely related, and that their open questions are merely special cases of a family of open questions which relate to the difference (if any) between deterministic and nondeterministic time or space bounded Turing machines. In particular we show that spectra are just those sets which are acceptable by nondeterministic Turing machines in time 2cx, where c is constant and x is the length of the input. Combining this result with results of Bennett [2], Ritchie [10], Kuroda [7], and Cook [3], we obtain the “hierarchy” of classes of sets shown in Figure 1. It is of interest to note that in all of these cases the amount of unrestricted read/write memory appears to be too small to allow diagonalization within the larger classes.

A course in discrete mathematical structures has been included as a necessary component of a program in all major curriculum studies in computer science. This paper discusses this type of course with respect to problems encountered in its implementation due to its central position in the curriculum. Recommendations are made regarding the level, content, and handling of the course, based on several years' experience in teaching the material.

In this paper we show that these similarities are not accidental - that spectra and context sensitive languages are closely related, and that their open questions are merely special cases of a family of open questions which relate to the difference (if any) between deterministic and non-deterministic time-or space-bounded Turing machines.