Search

Much work has been done towards characterizing the semantics of block structured programming languages using the lambda calculus [ 2 ] . Johnston [ 3 ] recently introduced a cell-based approach, called the contour model, for specifying the execution semantics of such languages. This paper relates the two approaches by giving a contour model evaluator for compiled lambda expressions. Section 2 gives the basic definitions needed from the lambda calculus to make the paper self-contained. Section 3 defines the Contour Model Lambda Calculus Machine (CMLCM). Unfortunately publication limitations preclude some worked examples which would greatly aid the reader's understanding. They will be provided in the talk itself and in an expanded version of this paper for the Tutorial Conference on Semantic Models of Computation. Section 4 outlines the structure of the proof of the CMLCM's correctness. And Section 5 is a set of concluding remarks on the significance of the CMLCM.

Some of the assertions about programs which we might be interested in proving are concerned with correctness, equivalence, accessibility of subroutines and guarantees of termination. We should like to develop techniques for determining such properties efficiently and intelligently wherever possible. Though theory tells us that for a realistic programming language almost any interesting property of the behaviour is effectively undecidable, this situation may not be intolerable in practice. An unsolvability result just gives us warning that we may not be able to solve all of the problems we are presented with, and that some of the ones we can solve will be very hard. In such circumstances it is very reasonable to try and determine necessary or sufficient conditions on programs for our techniques to be assured of success; however, in this paper we shall discuss a more qualitative, indirect, approach. We consider a range of more or less simplified computer models, chosen judiciously to exemplify some particular feature or features of computation. A demonstration of unsolvability in such a model reveals more accurately those sources which can contribute to unsolvability in a more complicated structure. On the other hand a decision procedure may illustrate a technique of practical use. It is our thesis that this kind of strategy of exploration can and will yield insight and practical advances in the theory of computation. Provided that the model retains some practical relevance, the dividends are the greater the nearer the decision problem lies to the frontier between solvability and unsolvability.

At the present time there is considerable interest in the general question of “automating programming:” there are a number of people actively doing research concerned with various aspects of the question and even a few projects exploring various practical issues via experimental implementations. The area encompassed by “automating programming” is a very broad one, particularly if one understands “programming” to include the entire spectrum of activities concerned with producing algorithms which are correct and effective in terms of certain design specifications. It is therefore to be expected that comparison of various techniques and integration of those techniques and the experimental facilities developed in a variety of institutions will be difficult and expensive unless there is some coordinated effort to provide a common framework to support such activities. We would note that at present it is relatively expensive just to construct sufficient programs to permit the investigation of and experimentation with some proposed technique of program automation; because of this many studies in the general area of programming automation are primarily “paper studies”. It is the purpose of this note to provide an overview of the project currently under way at Harvard's Center for Research in Computing Technology, directed toward the implementation of a laboratory for the study of programming automation techniques. A more detailed discussion of our approach is provided in [1]. In the four sections which follow we will discuss briefly our view of the use of a program automation laboratory, the basis for and basic components of the facility currently being implemented, and finally, suggest that there are a variety of research areas which are strongly related to the question of automating programming in which the laboratory might be employed as a research tool.

This paper contains the formal development of a correct algorithm from an implicit definition of the task to be performed. Each step of the development can be accompanied by a proof of its correctness. As well as ensuring the correctness of the final program, the structured development gives considerable insight into the algorithm and possible alternatives. The example used is a simplified form of the recognition algorithm due to Earley.

Based on the formal definition techniques of Lucas et al [1] which have been applied to the description of programming languages, this paper defines the algorithm of radix sorting and develops a proof of its validity.

A "Badly Nondeterministic" (BN) n-state acceptor is a machine for which any deterministic finite state acceptor for the same language requires 2 n states. A family of such machines, attributed to G. Ott, was described in (1). Taking liberties with the notation of that paper, we will call the family {R n }n>0 (see figure below). Another family of BN automata, which we will call {B n }n>0, was described in (2). These latter BN automata are the subject of this note.

Greg Chaitin, a frequent past contributor to SIGACT News, has produced a non-technical exposition of some of the concepts and methods in information-theoretic computational complexity, and some of his results, as presented in "Information Theoretic Limitations of Formal Systems". Both a revised version of the technical paper (see SIGACT News, December 1971, page 12, for an abstract) and the non-technical exposition should appear in the literature soon. Meanwhile, we excerpt - by permission - some of the philosophical implications which we find interesting. -Ed.

In a recent paper [1], Rosenberg conjectures that the results found in Holt and Reingold [2], can be generalized. Suppose that graphs are presented via their adjacency matrices. Then Holt and Reingold show that any algorithm which detects whether or not a graph is strongly connected (respectively, contains a cycle) must in worst case probe 0(n 2 ) entries of the given n x n adjacency matrix. Rosenberg then considers restrictions on graph property P such that any algorithm takes in worst case 0(n 2 ) probes to determine whether or not a n-node graph has property P.