Stanford Computer Science Department Technical Reports from the 1980
The authors have given permission to make their technical reports available on this server. If a report waspublished in print and is not here it may be that the author published it elsewhere.
Report Number: CS-TR-80-768
Institution: Stanford University, Department of Computer Science
Title: Causal nets or what is a deterministic computation
Author: Gacs, Peter
Author: Levin, Leonid A.
Date: October 1980
Abstract: We introduce the concept of causal nets - it can be considered as the most general and elementary concept of the history of a deterministic computation (sequential or parallel). Causality and locality are distinguished as the only important properties of nets representing such records. Different types of complexities of computations correspond to different geometrical characteristics of the corresponding causal nets - which have the advantage of being finite objects. Synchrony becomes a relative notion. Nets can have symmetries; therefore it will make sense to ask what can be computed from arbitrary symmetric inputs. Here, we obtain a complete group-theoretical characterization of the kind of symmetries that can be allowed in parallel computations.
CS-TR-80-768
Report Number: CS-TR-80-779
Institution: Stanford University, Department of Computer Science
Title: Problematic features of programming languages: a situational-calculus approach
Author: Manna, Z ohar
Author: Waldinger, Richard J.
Date: September 1980
Abstract: Certain features of programming languages, such as data structure operations and procedure call mechanisms, have been found to resist formalization by classical techniques. An alternate approach is presented, based on a "situational calculus," which makes explicit reference to the states of a computation. For each state, a distinction is drawn between an expression, its value, and the location of the value. Within this conceptual framework, the features of a programming language can be described axiomatically. Programs in the language can then be synthesized, executed, verified, or transformed by performing deductions in this axiomatic system. Properties of entire classes of programs, and of programming languages, can also be expressed and proved in this way. The approach is amenable to machine implementation. In a situational-calculus formalism it is possible to model precisely many "problematic" features of programming langauges, including operations on such data structures as arrays, pointers, lists, and records, and such procedure call mechanisms as call-by-reference, call-by-value, and call-by-name. No particular obstacle is presented by aliasing between variables, by declarations, or by recursive procedures. The paper is divided into three parts, focusing respectively on the assignment statement, on data structure operations, and on procedure call mechanisms. In this first part, we introduce the conceptual framework to be applied throughout and present the axiomatic definition of the assignment statement. If suitable restrictions on the programming language are imposed, the well-known Hoare assignment axiom can then be proved as a theorem. However, our definition can also describe the assignment statement of unrestricted programming languages, for which the Hoare axiom does not hold.
CS-TR-80-779
Report Number: CS-TR-80-780
Institution: Stanford University, Department of Computer Science
Title: The Computer Modern family of typefaces
Author: Knuth, Donald E.
Date: January 1980
Abstract: This report gives machine-independent definitions of all the styles of type planned for use in future editions of "The Art of Computer Programming." Its main purpose is to provide a detailed example of a complete family of font definitions using METAFONT, so that people who want new symbols for their own books and papers will understand how to incorporate them easily. The fonts are intended to have the same spirit as those used in earlier editions of "The Art of Computer Programming," but each character has been redesigned and defined in the METAFONT idiom. It is hoped that some readers will be inspired to make similar definitions of other important familites of fonts. The bulk of this report consists of about 400 short METAFONT programs for the various symbols needed, and as such it is pretty boring, but there are some nice illustrations.
CS-TR-80-780
Report Number: CS-TR-80-785
Institution: Stanford University, Department of Computer Science
Title: Equations and rewrite rules: a survey
Author: Huet, Gerard
Author: Oppen, Derek C.
Date: January 1980
Abstract: Equations occur frequently in mathematics, logic and computer science. In this paper, we survey the main results concerning equations, and the methods available for reasoning about them and computing with them. The survey is self-contained and unified, using traditional abstract algebra. Reasoning about equations may involve deciding if an equation follows from a given set of equations (axioms), or if an equation is true in a given theory. When used in this manner, equations state properties that hold between objects. Equations may also be used as definitions; this use is well known in computer science: programs written in applicative languages, abstract interpreter definitions, and algebraic data type definitions are clearly of this nature. When these equations are regarded as oriented "rewrite rules," we may actually use them to compute. In addition to covering these topics, we discuss the problem of "solving" equations (the "unification" problem), the problem of proving termination of sets of rewrite rules, and the decidability and complexity of word problems and of combinations of equational theories. We restrict ourselves to first-order equations, and do not treat equations which define non-terminating computations or recent work on rewrite rules applied to equational congruence classes.
CS-TR-80-785
Report Number: CS-TR-80-786
Institution: Stanford University, Department of Computer Science
Title: Algorithms in modern mathematics and computer science
Author: Knuth, Donald E.
Date: January 1980
Abstract: The life and work of the ninth century scientist al-Khwarizmi, "the father of algebra and algorithms," is surveyed briefly. Then a random sampling technique is used in an attempt to better understand the kinds of thinking that good mathematicians and computer scientists do and to analyze whether such thinking is significantly "algorithmic" in nature. (This is the text of a talk given at the opening session of a symposium on "Algorithms in Modern Mathamatics and Computer Science" held in Urgench, Khorezm Oblast', Uzbek S.S.R., during the week of September 16-22, 1979.)
CS-TR-80-786
Report Number: CS-TR-80-788
Institution: Stanford University, Department of Computer Science
Title: Circumscription - a form of non-monotonic reasoning
Author: McCarthy, John
Date: February 1980
Abstract: Humans and intelligent computer programs must often jump to the conclusion that the objects they can determine to have certain properties or relations are the only objects that do. Circumscripion formalizes such conjectural reasoning.
CS-TR-80-788
Report Number: CS-TR-80-789
Institution: Stanford University, Department of Computer Science
Title: ADA exceptions: specification and proof techniques
Author: Luckham, David C.
Author: Polak, Wolfgang
Date: February 1980
Abstract: A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications. This permits documentation of those exceptions that can be propagated by a subprogram. Exception handlers are documented by entry assertions. Axioms and proof rules for Ada exceptions are given. These rules are simple extensions of previous rules for Pascal and define an axiomatic semantics of Ada exceptions. As a result, Ada programs specified according to the method can be analysed by formal proof techniques for consistency with their specifications, even if they employ exception propagation and handling to achieve required results (i.e. non-error situations). Example verifications are given.
CS-TR-80-789
Report Number: CS-TR-80-790
Institution: Stanford University, Department of Computer Science
Title: Databases in healthcare
Author: Wiederhold, Gio
Date: March 1980
Abstract: This report defines database design and implementation technology as applicable to healthcare. The relationship of technology to various healthcare settings is explored, and the effectiveness on healthcare costs, quality and access is evaluated. A summary of relevant development directions is included. Detailed examples of 5 typical clinical applications (public health, clinical trials, clinical research, ambulatory care, and hospitals) are appended. There is an extended bibliography.
CS-TR-80-790
Report Number: CS-TR-80-792
Institution: Stanford University, Department of Computer Science
Title: MAINSAIL implementation overview
Author: Wilcox, Clark R.
Author: Dageforde, Mary L.
Author: Jirak, Gregory A.
Date: March 1980
Abstract: The MAINSAIL programming language and the supporting implementations have been developed over the past five years as an integrated approach to a viable machine-independent system suitable for the development of large, portable programs. Particular emphasis has been placed on minimizing the effort involved in moving the system to a new machine and/or operating system. For this reason, almost all of the compiler and runtime support is written in MAINSAIL, and is utilized in each implementation without alteration. This use of a high-level language to support its own implementation has proved to be a significant advantage in terms of documentation and maintenance, without unduly affecting the execution speed. This paper gives an overview of the compiler and runtime implementation strategies, and indicates what an implementation requires for the machine-dependent and operating-system-dependent parts.
CS-TR-80-792
Report Number: CS-TR-80-794
Institution: Stanford University, Department of Computer Science
Title: Recent developments in the complexity of combinatorial algorithms
Author: Tarjan, Robert Endre
Date: June 1980
Abstract: The last three years have witnessed several major advances in the area of combinatorial algorithms. These include improved algorithms for matrix multiplication and maximum network flow, a polynomial-time algorithm for linear programming, and steps toward a polynomial-time algorithm for graph isomorphism. This paper surveys these results and suggests directions for future research. Included is a discussion of recent work by the author and his students on dynamic dictionaries, network flow problems, and related questions.
CS-TR-80-794
Report Number: CS-TR-80-796
Institution: Stanford University, Department of Computer Science
Title: Essential E
Author: Samuel, Arthur L.
Date: March 1980
Abstract: This is an introductory manual describing the display-oriented text editor E that is available on the Stanford A.I. Laboratory PDP-10 computer. The present manual is intended to be used as an aid for the beginner as well as for experienced computer users who either are unfamiliar with the E editor or use it infrequently. Reference is made to the two on-line manuals that help the beginner to get started and that provide a complete description of the editor for the experienced user. E is commonly used for writing computer programs and for preparing reports and memoranda. It is not a document editor, although it does provide some facilities for getting a document into a pleasing format. The primary emphasis is that of speed, both in terms of the number of key strokes required of the user and in terms of the demands made on the computer system. At the same time, E is easy to learn and it offers a large range of facilities that are not available on many editors.
CS-TR-80-796
Report Number: CS-TR-80-797
Institution: Stanford University, Department of Computer Science
Title: Read-only transactions in a distributed database
Author: Garcia-Molina, Hector
Author: Wiederhold, Gio
Date: April 1980
Abstract: A read-only transaction or query is a transaction which does not modify any data. Read-only transactions could be processed with general transaction processing algorithms, but in many cases it is more efficient to process read-only transactions with special algorithms which take advantage of the knowledge that the transaction only reads. This paper defines the various consistency and currency requirements that read-only transactions may have. The processing of the different classes of read-only transactions in a distributed database is discussed. The concept of R insularity is introduced to characterize both the read-only and update algorithms. Several simple update and read-only transaction processing algorithms are presented to illustrate how the query requirements and the update algorithms affect the read-only transaction processing algorithms.
CS-TR-80-797
Report Number: CS-TR-80-799
Institution: Stanford University, Department of Computer Science
Title: Multidimensional additive spline approximation
Author: Friedman, Jerome H.
Author: Grosse, Eric
Author: Stuetzle, Werner
Date: May 1980
Abstract: We describe an adaptive procedure that approximates a function of many variables by a sum of (univariate) spline functions $s_m$ of selected linear combinations $a_m \cdot x$ of the coordinates $\theta (x) = \sum_{1\le m\le M} s_m (a_m \cdot x)$. The procedure is nonlinear in that not only the spline coefficients but also the linear combinations are optimized for the particular problem. The sample need not lie on a regular grid, and the approximation is affine invariant, smooth, and lends itself to graphical interpretation. Function values, derivatives, and integrals are cheap to evaluate.
CS-TR-80-799
Report Number: CS-TR-80-807
Institution: Stanford University, Department of Computer Science
Title: Path-regular graphs
Author: Matula, David W.
Author: Dolev, Danny
Date: June 1980
Abstract: A graph is vertex-[edge-]path-regular if a list of shortest paths, allowing multiple copies of paths, exists where every pair of vertices are the endvertices of the same number of paths and each vertex [edge] occurs in the same number of paths of the list. The dependencies and independencies between the various path-regularity, regularity of degree, and symmetry properties are investigated. We show that every connected vertex-[edge-]symmetric graph is vertex-[edge-]path-regular, but not conversely. We show that the product of any two vertex-path-regular graphs is vertex-path-regular but not conversely, and the iterated product G x G x ... x G is edge-path-regular if and only if G is edge-path-regular. An interpretation of path-regular graphs is given regarding the efficient design of concurrent communication networks.
CS-TR-80-807
Report Number: CS-TR-80-808
Institution: Stanford University, Department of Computer Science
Title: Final report: Basic Research in Artificial Intelligence and Foundations of Programming
Author: McCarthy, John
Author: Binford, Thomas O.
Author: Luckham, David C.
Author: Manna, Z ohar
Author: Weyhrauch, Richard W.
Author: Earnest, Les
Date: May 1980
Abstract: Recent research results are reviewed in the areas of formal reasoning, mathematical theory of computation, program verification, and image understanding.
CS-TR-80-808
Report Number: CS-TR-80-811
Institution: Stanford University, Department of Computer Science
Title: An extended semantic definition of Pascal for proving the absence of common runtime errors
Author: German, Steven M.
Date: June 1980
Abstract: We present an axiomatic definition of Pascal which is the logical basis of the Runcheck system, a working verifier for proving the absence of runtime errors such as arlthmetic overflow, array subscripting out of range, and accessing an uninitialized variable. Such errors cannot be detected at compile time by most compilers. Because the occurrence of a runtime error may depend on the values of data supplied to a program, techniques for assuring the absence of errors must be based on program specifications. Runcheck accepts Pascal programs documented with assertions, and proves that the specifications are consistent with the program and that no runtime errors can occur. Our axiomatic definition is similar to Hoare's axiom system, but it takes into account certain restrictions that have not been considered in previous definitions. For instance, our definition accurately models uninitialized variables, and requires a variable to have a well defined value before it can be accessed. The logical problems of introducing the concept of uninitialized variables are discussed. Our definition of expression evaluation deals more fully with function calls than previous axiomatic definitions. Some generalizations of our semantics are presented, including a new method for verifying programs with procedure and function parameters. Our semantics can be easily adopted to similar languages, such as ADA. One of the main potential problems for the user of a verifier is the need to write detailed, repetitious assertions. We develop some simple logical properties of our definition which are exploited by Runcheck to reduce the need for such detailed assertions.
CS-TR-80-811
Report Number: CS-TR-80-821
Institution: Stanford University, Department of Computer Science
Title: Semiantichains and unichain coverings in direct products of partial orders
Author: West, Douglas B.
Author: Tovey, Craig A.
Date: September 1980
Abstract: We conjecture a generalization of Dilworth's theorem to direct products of partial orders. In particular, we conjecture that the largest "semiantichain" and the smallest "unichain covering" have the same size. We consider a special class of semiantichains and unichain coverings and determine when equality holds for them. This conjecture implies the existence of k-saturated partitions. A stronger conjecture, for which we also prove a special case, implies the Greene-Kleitman result on simultaneous k and (k + 1)-saturated partitions.
CS-TR-80-821
Report Number: CS-TR-80-824
Institution: Stanford University, Department of Computer Science
Title: LCCD, a language for Chinese character design
Author: Mei, Tung Yun
Date: October 1980
Abstract: LCCD is a computer system able to produce aesthetically pleasing Chinese characters for use on raster-oriented printing devices. It is analogous to METAFONT, in that the user writes a little program that explains how to draw each character; but it uses different types of simulated 'pens' that are more appropriate to the Chinese idiom, and it includes special scaling features so that a complex character can easily be built up from simpler ones, in an interactive manner. This report contains a user's manual for LCCD, together with many illustrative examples and a discussion of the algorithms used.
CS-TR-80-824
Report Number: CS-TR-80-826
Institution: Stanford University, Department of Computer Science
Title: A database approach to communication in VLSI design
Author: Wiederhold, Gio
Author: Beetem, Anne
Author: Short, Garrett
Date: October 1980
Abstract: This paper describes recent and planned work at Stanford in applying database technology to the problems of VLSI design. In particular, it addresses the issue of communication within a design's different representations and hierarchical levels in a multiple designer environment. We demonstrate the heretofore questioned utility of using commercial database systems, at least while developing a versatile, flexible, and generally efficient model and its associated communication paths. Completed work and results from initial work using DEC DBMS-20 is presented, including macro expansion within the database, and signalling of changes to higher structural levels. Considerable discussion regarding overall philosophy for continued work is also included.
CS-TR-80-826
Report Number: CS-TR-80-827
Institution: Stanford University, Department of Computer Science
Title: On the parallel computation for the knapsack problem
Author: Yao, Andrew Chi-Chih
Date: November 1980
Abstract: We are interested in the complexity of solving the knapsack problem with n input real numbers on a parallel computer with real arithmetic and branching operations. A processor-time tradeoff constraint is derived; in particular, it is shown that an exponential number of processors have to be used if the problem is to be solved in time $t \le {\sqrt{n}}/2$.
CS-TR-80-827
Report Number: CS-TR-80-829
Institution: Stanford University, Department of Computer Science
Title: The dinner table problem
Author: Aspvall, Bengt
Author: Liang, Frank M.
Date: December 1980
Abstract: This report contains two papers inspired by the "dinner table problem": If n people are seated randomly around a circular table for two meals, what is the probability that no two people sit together at both meals? We show that this probability approaches $e^{-2}$ as $n \rightarrow \infty$, and also give a closed form. We then observe that in many similar problems on permutations with restricted position, the number of permutations satisfying a given number of properties is approximately Poisson distributed. We generalize our asymptotic argument to prove such a limit theorem, and mention applications to the problems of derangements, menages, and the asymptotic number of Latin rectangles.
CS-TR-80-829
Report Number: CS-TR-80-830
Institution: Stanford University, Department of Computer Science
Title: Two linear-time algorithms for five-coloring a planar graph
Author: Matula, David W.
Author: Shiloach, Yossi
Author: Tarjan, Robert E.
Date: November 1980
Abstract: A "sequential processing" algorithm using bicolor interchange that five-colors an n vertex planar graph in $O(n^2)$ time was given by Matula, Marble, and Isaacson [1972]. Lipton and Miller used a "batch processing" algorithm with bicolor interchange for the same problem and achieved an improved O(n log n) time bound [1978]. In this paper we use graph contraction arguments instead of bicolor interchange and improve both the sequential processing and batch processing methods to obtain five-coloring algorithms that operate in O(n) time.
CS-TR-80-830
Report Number: CS-TR-80-832
Institution: Stanford University, Department of Computer Science
Title: Scheduling wide graphs
Author: Dolev, Danny
Date: December 1980
Abstract: The problem of scheduling a partially ordered set of unit length tasks on m identical processors is known to be NP-complete. There are efficient algorithms for only a few special cases of this problem. In this paper we explore the relations between the structure of the precedence graph (the partial order) and optimal schedules. We prove that in finding an optimal schedule for certain systems it suffices to consider at each step high roots which belong to at most the m-1 highest components of the precedence graph. This result reduces the number of cases we have to check during the construction of an optimal schedule. Our method may lead to the development of linear scheduling algorithms for many practical cases and to better bounds for complex algorithms. In particular, in the case the precedence graph contains only inforest and outforest components, this result leads to efficient algorithms for obtaining an optimal schedule on two or three processors.
CS-TR-80-832
Report Number: CS-TR-80-850
Institution: Stanford University, Department of Computer Science
Title: Performing remote operations efficiently on a local computer network
Author: Spector, Alfred Z .
Date: December 1980
Abstract: This paper presents a communication model for local networks, whereby processes execute generalized remote references that cause operations to be performed by remote processes. This remote reference/remote operation model provides a taxonomy of primitives that (1) are naturally useful in many applications and (2) can be efficiently implemented. The motivation for this work is our desire to develop systems architectures for local network based multiprocessors that support distributed applications requiring frequent interprocessor communication. After a section containing a brief overview, Section 2 of this paper discusses the remote reference/remote operation model. In it, we derive a set of remote reference types that can be supported by a communication system carefully integrated with the local network interface. The third section exemplifies a communication system that provides one remote reference type. These references (i.e., remote load, store, compare-and-swap, enqueue, and dequeue) take about 150 microseconds, or 50 average instruction times, to perform on Xerox Alto computers connected by a 2.94 megabit Ethernet. The last section summarizes this work and proposes a complete implementation resulting in a highly efficient communication system.
CS-TR-80-850
Report Number: CS-TR-81-836
Institution: Stanford University, Department of Computer Science
Title: Verification of concurrent programs, Part I: The temporal framework
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: June 1981
Abstract: This is the first in a series of reports describing the application of temporal logic to the specification and verification of concurrent programs. We first introduce temporal logic as a tool for reasoning about sequences of states. Models of concurrent programs based both on transition graphs and on linear-text representations are presented and the notions of concurrent and fair executions are defined. The general temporal language is then specialized to reason aboaut those execution sequences that are fair computations of a concurrent program. Subsequently, the language is used to describe properties of concurrent programs. The set of interesting properties is classified into invariance (safety), eventuality (liveness), and precedence (until) properties. Among the properties studied are: partial correctness, global invariance, clean behavior, mutual exclusion, absence of deadlock, termination, total correctness, intermittent assertions, accessibility, responsiveness, safe liveness, absence of unsolicited response, fair responsiveness, and precedence. In the following reports of this series, we will use the temporal formalism to develop proof methodologies for proving the properties discussed here.
CS-TR-81-836
Report Number: CS-TR-81-837
Institution: Stanford University, Department of Computer Science
Title: Research on expert systems
Author: Buchanan, Bruce G.
Date: March 1981
Abstract: All AI programs are essentially reasoning programs. And, to the extent that they reason well about a problem area, all exhibit some expertise at problem solving. Programs that solve the Tower of Hanoi puzzle, for example, reason about the goal state and the initial state in order to find "expert-level" solutions. Unlike other programs, however, the claims about expert systems are related to questions of usefulness and understandability as well as performance.
CS-TR-81-837
Report Number: CS-TR-81-838
Institution: Stanford University, Department of Computer Science
Title: Dynamic program building
Author: Brown, Peter
Date: February 1981
Abstract: This report argues that programs are better regarded as dynamic running objects rather than as static textual ones. The concept of dynamic building, whereby a program is constructed as it runs, is described. The report then describes the Build system, which is an implementation of dynamic building for an interactive algebraic programming language. Dynamic building aids the locating of run-time errors, and is especially valuable in environments where programs are relatively short but run-time errors are frequent and/or costly.
CS-TR-81-838
Report Number: CS-TR-81-839
Institution: Stanford University, Department of Computer Science
Title: Short WAITS
Author: Samuel, Arthur L.
Date: February 1981
Abstract: This is an introductory manual describing the SU-AI timesharing system that is available primarily for sponsored research in the Computer Science Department. The present manual is written for the beginner and the user interested primarily in the message handling capability as well as for the experienced computer user and programmer who either is unfamiliar with the SU-AI computer or who uses it infrequently. References are made to the available hard-copy manuals and to the extensive on-line document files where more complete information can be obtained. The principal advantages of this system are: 1) The availability of a large repertoire of useful system features; 2) The large memory; 3) The large file storage system; 4) The ease with which one can access other computers via the ARPA net; 5) The file transfer facilities via the EFTP program and the ETHERNET; 6) The XGP and the DOVER printers and the large collections of fonts available for them; and 7) The fast and convenient E editor with its macro facilities.
CS-TR-81-839
Report Number: CS-TR-81-846
Institution: Stanford University, Department of Computer Science
Title: The Byzantine Generals strike again
Author: Dolev, Danny
Date: March 1981
Abstract: Can unanimity be achieved in an unreliable distributed system? This problem was named "The Byzantine Generals Problem," by Lamport, Pease and Shostak [1980]. The results obtained in the present paper prove that unanimity is achievable in any distributed system if and only if the number of faulty processors in the system is: 1) less than one third of the total number of processors; and 2) less than one half of the connectivity of the system's network. In cases where unanimity is achievable, algorithms to obtain it are given. This result forms a complete characterization of networks in light of the Byzantine Problem.
CS-TR-81-846
Report Number: CS-TR-81-847
Institution: Stanford University, Department of Computer Science
Title: The optimal locking problem in a directed acyclic graph
Author: Korth, Henry F.
Date: March 1981
Abstract: We assume a multiple granularity database locking scheme similar to that of Gray, et al. [197S] in which a rooted directed acyclic graph is used to represent the levels of granularity. We prove that even if it is known in advance exactly what database references the transaction will make, it is NP-complete to find the optimal locking strategy for the transaction.
CS-TR-81-847
Report Number: CS-TR-81-848
Institution: Stanford University, Department of Computer Science
Title: On the problem of inputting Chinese characters
Author: Tang, Chih-sung
Date: April 1981
Abstract: If Chinese-speaking society is to make the best use of computers, it is important to develop an easy, quick, and convenient way to input Chinese characters together with other conventional characters. Many people have tried to approach this problem by designing special typewriters for Chinese character input, but such methods have serious deficiencies and they do not take advantage of the fact that the input process is just part of a larger system in which a powerful computer lies behind the keyboard. The purpose of this note is to clarify the problem and to illustrate a promising solution based entirely on a standard ASCII keyboard.
CS-TR-81-848
Report Number: CS-TR-81-849
Institution: Stanford University, Department of Computer Science
Title: Experiments on the Knee Criterion in a multiprogrammed computer system
Author: Nishigaki, Tohru
Date: March 1981
Abstract: Although the effectiveness of the Knee Criterion as a virtual memory management strategy is widely accepted, it has been impossible to take advantage of it in a practical system, because little information is available about the program behavior of executing jobs. A new memory management technique to achieve the Knee Criterion in a multiprogrammed virtual memory system is developed. The technique, termed the Optimum Working-set Estimator (OWE), abstracts the programs' behavior from their past histories by exponential smoothing, and modifies their working set window sizes in order to attain the Knee Criterion. The OWE method was implemented and investigated. Measurements demonstrate its ability to control a variety of jobs. Furthermore, the results also reveal that the throughput improvement is possible in a space-squeezing environment. This technique is expected to increase the efficiency of multiprogrammed virtual memory systems.
CS-TR-81-849
Report Number: CS-TR-81-851
Institution: Stanford University, Department of Computer Science
Title: Binding in information processing
Author: Wiederhold, Gio
Date: May 1981
Abstract: The concept of binding, as used in programming systems, is analyzed and defined in a number of contexts. The attributes of variables to be bound and the phases of binding are enumerated. The definition is then broadened to cover general issues in information systems. Its applicability is demonstrated in a wide range of system design and implementation issues. A number of Database Management Systems are categorized according to the terms defined. A first-order quantitative model is developed and compared with current practice. The concepts and the model are considered helpful when used as a tool for the global design phase of large information systems.
CS-TR-81-851
Report Number: CS-TR-81-854
Institution: Stanford University, Department of Computer Science
Title: On the security of public key protocols
Author: Dolev, Danny
Author: Yao, Andrew C.
Date: May 1981
Abstract: Recently, the use of public key encryption to provide secure network communication has received considerable attention. Such public key systems are usually effective against passive eavesdroppers, who merely tap the lines and try to decipher the message. It has been pointed out, however, that an improperly designed protocol could be vulnerable to an active saboteur, one who may impersonate another user or alter the message being transmitted. In this paper we formulate several models in which the security of protocols can be discussed precisely. Algorithms and characterizations that can be used to determine protocol security in these models will be given.
CS-TR-81-854
Report Number: CS-TR-81-863
Institution: Stanford University, Department of Computer Science
Title: A programming and problem-solving seminar
Author: Knuth, Donald E.
Author: Miller, Allan A.
Date: June 1981
Abstract: This report contains a record of the autumn 1980 session of CS 204, a problem-solving and programming seminar taught at Stanford that is primarily intended for first-year Ph.D. students. The seminar covers a large range of topics, research paradigms, and programming paradigms in computer science, so these notes will be of interest to graduate students, professors, and professional computer scientists.
CS-TR-81-863
Report Number: CS-TR-81-865
Institution: Stanford University, Department of Computer Science
Title: Toward a unified logical basis for programming languages
Author: Tang, Chih-sung
Date: June 1981
Abstract: In recent years, more and more computer scientists have been paying attention to temporal logic, since there are many properties of programs that can be described only by bringing the time parameter into consideration. But existing temporal logic languages, such as Lucid, in spite of their mathematical elegance, are still far from practical. I believe that a practical temporal-logic language, once it came into being, would have a wide spectrum of applications. XYZ /E is a temporal-logic language. Like other logic languages, it is a logic system as well as a programming language. But unlike them, it can express all conventional data structures and control structures, nondeterminate or concurrent programs, even programs with branching-time order. We find that the difficulties met in other logic languages often stem from the fact that they try to deal with these structures in a higher level. XYZ /E adopts another approach. We divide the language into two forms: the internal form and the external form. The former is lower level, while the latter is higher. Just as any logic system contains rules of abbreviation, so also in XYZ /E there are rules of abbreviation to transform the internal form into the external form, and vice versa. These two forms can be considered to be different representations of the same thing. We find that this approach can ameliorate many problems of formalization.
CS-TR-81-865
Report Number: CS-TR-81-867
Institution: Stanford University, Department of Computer Science
Title: ADAM - an Ada based language for multi-processing
Author: Luckham, David C.
Author: Larsen, Howard J.
Author: Stevenson, David R.
Author: Henke, Friedrich W. von
Date: July 1981
Abstract: Adam is an experimental language derived from Ada. It was developed to facilitate study of issues in Ada implementation. The two primary objectives which motivated the development of Adam were: to program supervisory packages for multitask scheduling, and to formulate algorithms for compilation of Ada tasking. Adam is a subset of the sequential program constructs of Ada combined wlth a set of parallel processing constructs which are lower level than Ada tasking. In addition, Adam places strong restrictions on sharing of global objects between processes. Import declarations and propagate declarations are included. A compiler has been implemented in Maclisp on a DEC PDP-10. It produces assembly code for a PDP-10. It supports separate compilatlon, generics, exceptions, and parallel processes. Algorithms translating Ada tasking into Adam parallel processing have been developed and implemented. An experimental compiler for most of the final Ada language design, including task types and task rendezvous constructs, based on the Adam compiler, is presently available on PDP-10's. This compiler uses a procedure call implementation of task rendezvous, but wlll be used to develop and study alternate implementatlons.
CS-TR-81-867
Report Number: CS-TR-81-868
Institution: Stanford University, Department of Computer Science
Title: The Last Whole Errata Catalog
Author: Knuth, Donald E.
Date: July 1981
Abstract: This list supplements previous errata published in Stanford reports CS551 (1976) and CS712 (1979). It includes the first corrections and changes to the second edition of volume two (published January, 1981) as well as to the most recent printings of volumes one and three (first published in 1975). In addition to the errors listed here, about half of the occurrences of 'which' in volumes one and three should be changed to 'that'.
CS-TR-81-868
Report Number: CS-TR-81-869
Institution: Stanford University, Department of Computer Science
Title: Computer Science comprehensive examinations, 1978/79-1980/81
Author: Tajnai, Carolyn E.
Date: August 1981
Abstract: The Stanford Computer Science Comprehensive Examination was conceived Spring Quarter 1971/72 and since then has been given winter and spring quarters each year. The 'Comp' serves several purposes in the department. There are no course requirements in the Ph.D. and the Ph.D. Minor programs, and only one (CS293, Computer Laboratory) in the Master's program. Therefore, the 'Comp' fulfills the breadth and depth requirements. The Ph.D. Minor and Master's student must pass at the Master's level to be eligible for the degree. For the Ph.D. student it serves as a "Rite of Passage"; the exam must be passed at the Ph.D. level by the end of six quarters of full-time study (excluding summers) for the student to continue in the program. This report is a collection of comprehensive examinations from Winter Quarter 1978/79 through Spring Quarter 1980/81.
CS-TR-81-869
Report Number: CS-TR-81-871
Institution: Stanford University, Department of Computer Science
Title: Good layouts for pattern recognizers
Author: Trickey, Howard W.
Date: August 1981
Abstract: A system to lay out custom circuits that recognize regular languages can be a useful VLSI design automation tool. This paper describes the algorithms used in an implementation of a regular expression compiler. Layouts that use a network of programmable logic arrays (PLA's) have smaller areas than those of some other methods, but there are the problems of partitioning the circuit and then placing the individual PLA's. Regular expressions have a structure which allows a novel solution to these problems: dynamic programming can be used to find layouts which are in some sense optimal. Various search pruning heuristics have been used to increase thc speed of the compiler, and the experience with these is reported in the conclusions.
CS-TR-81-871
Report Number: CS-TR-81-875
Institution: Stanford University, Department of Computer Science
Title: Computation of matrix chain products: Part I, Part II
Author: Hu, T. C.
Author: Shing, M. T.
Date: September 1981
Abstract: This paper considers the computation of matrix chain products of the form $M_1 x M_2 x ... x M_{n-1}$. If the matrices are of different dimensions, the order in which the product is computed affects the number of operations. An optimum order is an order which minimizes the total number of operations. Some theorems about an optimum order of computing the matrices are presented in part I. Based on these theorems, an O(n log n) algorithm for finding an optimum order is presented in part II.
CS-TR-81-875
Report Number: CS-TR-81-876
Institution: Stanford University, Department of Computer Science
Title: On linear area embedding of planar graphs
Author: Dolev, Danny
Author: Trickey, Howard W.
Date: September 1981
Abstract: Planar embedding with minimal area of graphs on an integer grid is one of the major issues in VLSI. Valiant [1981] gave an algorithm to construct a planar embedding for trees in linear area; he also proved that there are planar graphs that require quadratic area. We give an algorithm to embed outerplanar graphs in linear area. We extend this algorithm to work for every planar graph that has the following property: for every vertex there exists a path of length less than K to the exterior face, where K is a constant. Finally, finding a minimal embedding area is shown to be NP-complete for forests, and hence for more general types of graphs.
CS-TR-81-876
Report Number: CS-TR-81-879
Institution: Stanford University, Department of Computer Science
Title: Interlisp-VAX: a report
Author: Masinter, Larry M.
Date: August 1981
Abstract: This report documents the results of a study to evaluate the feasibility of implementing the Interlisp language to run on the DEC VAX computer. Specific goals of the study were to: 1) assess the technical status of the on-going implementation project at USC-ISI; 2) estimate the expected performance of Interlisp on the VAX famility of machines as compared to Interlisp-10, other Lisp systems for the VAX, and other Interlisp implementations where performance data were available; and 3) identify serious obstacles and alternatives to the timely completion of an effective Interlisp-VAX system.
CS-TR-81-879
Report Number: CS-TR-81-880
Institution: Stanford University, Department of Computer Science
Title: Well structured parallel programs are not easier to schedule
Author: Mayr, Ernst W.
Date: September 1981
Abstract: The scheduling problem for unit time task systems with arbitrary precedence constrainls is known to be NP-complete. We show that the same is true even if the precedence constraints are restricted to certain subclasses which make the corresponding parallel programs more structured. Among these classes are those derived from hierarchic cobegin-coend programming constructs, level graph forests, and the parallel or serial composition of an out-tree and an in-tree. In each case, the completeness proof depends heavily on the number of processors being part of the problem instances.
CS-TR-81-880
Report Number: CS-TR-81-883
Institution: Stanford University, Department of Computer Science
Title: On program transformations for abstract data types and concurrency
Author: Pepper, P.
Date: October 1981
Abstract: We study transformation rules for a particular class of abstract data types, namely types that are representable by recursive mode declarations. The transformations are tailored to the development of efficient tree traversal and they allow for concurrency. The techniques are exemplified by an implementation of concurrent insertion and deletion in 2-3-trees.
CS-TR-81-883
Report Number: CS-TR-81-887
Institution: Stanford University, Department of Computer Science
Title: Finding the convex hull of a simple polygon
Author: Graham, Ronald L.
Author: Yao, Frances
Date: November 1981
Abstract: It is well known that the convex hull of a set of n points in the (Euclidean) plane can be found by an algorithm having worst-case complexity O(n log n). In this note we give a short linear algorithm for finding the convex hull in the case that the (ordered) set of points from the vertices of a simple (i.e., non-self-intersecting) polygon.
CS-TR-81-887
Report Number: CS-TR-81-889
Institution: Stanford University, Department of Computer Science
Title: AL users' manual
Author: Mujtaba, Shahid
Author: Goldman, Ron
Date: December 1981
Abstract: AL is a high-level programming language for manipulator control useful in industrial assembly research. This document describes the current state of the AL system now in operation at the Stanford Artificial Intelligence Laboratory, and teaches the reader how to use it. The system consists of the AL compiler and runtime system and the source code interpreter, POINTY, which facilitates specifying representation of parts, and interactive execution of AL statements.
CS-TR-81-889
Report Number: CS-TR-81-894
Institution: Stanford University, Department of Computer Science
Title: Methodology for building an intelligent tutoring system
Author: Clancey, William J.
Date: October 1981
Abstract: Over the past 6 years we have been developing a computer program to teach medical diagnosis. Our research synthesizes and extends results in artlficlal intelligence (Al), medicine, and cognitive psychology. This paper describes the progression of the research, and explalns how theories from these fields are combined in a computational model. The general problem has been to develop an "intelligent tutoring system" by adapting the MYCIN "expert system." Thls conversion requires a deeper understanding of the nature of expertise and explanatlon than origlnally requlred for developlng MYCIN, and a concomitant shift in perspective from slmple performance goals to attaining psychologlcal validity in the program's reasoning process. Others have written extensively about the relatlon of artificlal intelligence to cognltive sclence (e.g., [Pylyshyn, 1978] [Boden, 1977]). Our purpose here is not to repeat those arguments, but to present a case study which will provide a common point for further dlscusslon. To this end, to help evaluate the state of cognitive science, we will outline our methodology and survey what resources and viewpoints have helped our research. We will also discuss pitfalls that other Al-oriented cognitive scientists may encounter. Finally, we will present some questions coming out of our work whlch might suggest possible collaboration with other fields of research.
CS-TR-81-894
Report Number: CS-TR-81-896
Institution: Stanford University, Department of Computer Science
Title: The epistemology of a rule-based expert system: a framework for explanation
Author: Clancey, William J.
Date: November 1981
Abstract: Production rules are a popular representation for encoding heuristic knowledge in programs for scientific and medical problem solving. However, experience with one of these programs, MYCIN, indicates that the representation has serious limitations: people other than the original rule authors find it difficult to modify the rule set, and the rules are unsuitable for use in other settings, such as for application to teaching. These paroblems are rooted in fundamental limitations in MYCIN's original rule representation: the view that expert knowledge can be encoded as a uniform, weakly-structured set of if/then associations is found to be wanting. To illustrate these problems, this paper examines MYCIN's rujles from the perspective of a teacher trying to justify them and to convey a problem-solving approach. We discover that individual rules play different roles, have different kinds of justifications, and are constructed using different rationales for the ordering and choice of premise clauses. This design knowledge, consisting of structural and strategic concepts which lie outside the representation, is shown to be procedurally embedded in the rules. Moreover, because the data/hypothesis associations are themselves a proceduralized form of underlying disease models, they can only be supported by appealing to this deeper level of knowledge. Making explicit this structural, strategic and support knowledge enhances the ability to understand and modify the system.
CS-TR-81-896
Report Number: CS-TR-81-898
Institution: Stanford University, Department of Computer Science
Title: Separability as a physical database design methodology
Author: Whang, Kyu-Young
Author: Wiederhold, Gio
Author: Sagalowicz, Daniel
Date: October 1981
Abstract: A theoretical approach to the optimal design of large multifile physical databases is presented. The design algorithm is based on the theory that, given a set of join methods that satisfy a certain property called "separability," the problem of optimal assignment of access structures to the whole database can be reduced to the subproblem of optimizing individual relations independently of one another. Coupling factors are defined to represent all the interactions among the relations. This approach not only reduces the complexity of the problem significantly, but also provides a better understanding of underlying mechanisms. A closed noniterative formula is introduced for estimating the number of block accesses in a database organization, and the error analyzed. This formula, an approximation of Yao's exact formula, has a maximum error of 3.7%, and significantly reduces the computation time by eliminating the iterative loop. It also achieves a much higher accuracy than an approximation proposed by Cardenas.
CS-TR-81-898
Report Number: CS-TR-82-892
Institution: Stanford University, Department of Computer Science
Title: An algorithm for reducing acyclic hypergraphs
Author: Kuper, Gabriel M.
Date: January 1982
Abstract: This report is a description of an algorithm to compute efflciently the Graham reduction of an acyclic hypergraph with sacred nodes. To apply the algorithm we must already have a tree representation of the hypergraphs, and therefore it is useful when we have a fixed hypergraph and wish to compute Graham reductions many times, as we do in the Systern/U query interpretation algorithm.
CS-TR-82-892
Report Number: CS-TR-82-895
Institution: Stanford University, Department of Computer Science
Title: GLISP users' manual
Author: Novak, Gordon S., Jr.
Date: January 1982
Abstract: GLISP is a high-level, LISP-based language which is compiled into LISP. GLISP provides a powerful abstract datatype facility, allowing description and use of both LISP objects and objects in A.I. representation languages. GLISP language features include PASCAL-like control structures, infix expressions with operators which facilitate list manipulation, and reference to objects in PASCAL-like or English-like syntax. English-like definite reference to features of objects which are in the current computational context is allowed; definite references are understood and compiled relative to a knowledge base of object descriptions. Object-centered programming is supported; GLISP can substantially improve runtime performance of object-centered programs by optimized compilation of references to objects. This manual describes the GLISP language and use of GLISP within INTERLISP.
CS-TR-82-895
Report Number: CS-TR-82-903
Institution: Stanford University, Department of Computer Science
Title: Coloring maps and the Kowalski doctrine
Author: McCarthy, John
Date: April 1982
Abstract: It is attractive to regard an algorithm as composed of the logic determining what the results are and the control determining how the result is obtained. Logic programmers like to regard programming as controlled deduction, and there have been several proposals for controlling the deduction expressed by a Prolog program and not always using Prolog's normal backtracking algorithm. The present note discusses a map coloring program proposed by Pereira and Porto and two coloring algorithms that can be regarded as control applied to its logic. However, the control mechanisms required go far beyond those that have been contemplated in the Prolog literature.
CS-TR-82-903
Report Number: CS-TR-82-908
Institution: Stanford University, Department of Computer Science
Title: Neomycin: reconfiguring a rule-based expert system for application to teaching
Author: Clancey, William J.
Author: Letsinger, Reed
Date: May 1982
Abstract: NEOMYClN is a medical consultation system in which MYClN's knowledge base is reorganized and extended for use in GUIDON, a teaching program. The new system constitutes a psychological model for doing diagnosis designed to provide a basis for interpreting student behavior and teaching diagnostic strategy. The model separates out kinds of knowledge that are procedurally embedded in MYClN's rules and so inaccessible to the teaching program. The key idea is to represent explicitly and separately a domain-independent diagnostic strategy in the form of meta-rules, knowledge about the structure of the problem space, causal and data/hypothesis rules and world facts. As a psychological model, NEOMYCIN captures the forward-directed, "compiled associations" mode of reasoning that characterizes expert behavior. Collection and interpretation of data are focused by the "differential" or working memory of hypotheses. Moreover, the knowledge base is broadened so that GUIDON can teach a student when to consider a specific infectious dlsease and what competing hypotheses to consider, essentially the knowledge a human would need in order to use the MYCIN consultation system properly.
CS-TR-82-908
Report Number: CS-TR-82-909
Institution: Stanford University, Department of Computer Science
Title: Plan recognition strategies in student modeling: prediction and description
Author: London, Bob
Author: Clancey, William J.
Date: May 1982
Abstract: This paper describes the student modeler of the GUIDON2 tutor, which understands plans by a dual search strategy. It first produces multiple predictions of student behavior by a model-driven simulation of the expert. Focused, data-driven searches then explain incongruities. By supplementing each other, these methods lead to an efficient and robust plan understander for a complex domain.
CS-TR-82-909
Report Number: CS-TR-82-910
Institution: Stanford University, Department of Computer Science
Title: Exploration of Teaching and Problem-Solving Strategies, 1979-1982
Author: Clancey, William J.
Author: Buchanan, Bruce
Date: May 1982
Abstract: This is the final report for Contract N-00014-79-C-0302, covering the period of 15 March 1979 through 14 March 1982. The goal of the project was to develop methods for representing teaching and problem-solving knowledge in computer-based tutorial systems. One focus of the work was formulation of principles for managing a case method tutorial dialogue; the other major focus was investigation of the use of a production rule representation for the subject material of a tutorial program. The main theme pursued by this research is that representing teaching and problem-solving knowledge separately and explicitly enhances the ability to build, modify and test complex tutorial programs. Two major computer programs were constructed. One was the tutorial program, GUIDON, which uses a set of explicit "discourse procedures" for carrying on a case method dialogue with a student. GUIDON uses the original MYCIN knowledge base as subject material, and as such, was an experiment in exploring the ways in which production rules can be used in tutoring. GUlDON's teaching knowledge is separate from and compatible with any knowledge base that is encoded in MYClN's rule language. Demonstrations of GUIDON were given for two medical and one engineering application. Thus, the generality of this kind of system goes beyond being able to teach about any problem in a "case library"--it also allows teaching expertise to be transferred and tested in multiple problem domains. The second major program is the consultation program, NEOMYCIN. This is a second generation system in which MYClN's knowledge has been reconfigured to make explicit distinctions that are important for teaching. Unlike MYCIN, the program uses the hypothesis-oriented approach and predominantly forward-directed reasoning. As such, NEOMYCIN is consistent with and extends psychological models of diagnostic problem-solving. The program differs from other knowledge-based Al systems in that reasoning is completely controlled by a set of explicit meta-rules. These meta-rules are domain independent and constitute the diagnostic procedure to be taught to students: the tasks of diagnosis and heuristics for attending to and confirming relevant diagnostic hypotheses.
CS-TR-82-910
Report Number: CS-TR-82-911
Institution: Stanford University, Department of Computer Science
Title: Bibliography of Stanford Computer Science reports, 1963-1982
Author: Roberts, Barbara J.
Author: Marashian, Irris
Date: May 1982
Abstract: This report lists, in chronological order, all reports published by the Stanford Computer Science Department since 1963. Each report is identified by a Computer Science number, author's name, title, National Technical Information Service (NTIS) retrieval number (i.e., AD-XXXXXX), date, and number of pages. If the NTIS number is not given, it means that the report is probably not available from NTIS.
CS-TR-82-911
Report Number: CS-TR-82-912
Institution: Stanford University, Department of Computer Science
Title: The implication and finite implication problems for typed template dependencies
Author: Varde, Moshe Y.
Date: May 1982
Abstract: The class of typed template dependencies is a class of data dependencies that includes embedded multivalued and join dependencies. We show that the implication and the finite implication problems for this class are unsolvable. An immediate corollary is that this class has no formal system for finite implication. We also show how to construct a finite set of typed template dependencies whose implication and finite implication problems are unsolvable. The class of projected join dependencies is a proper subclass of the above class, and it generalizes slightly embedded join dependencies. It is shown that the implication and the finite implication problems for this class are also unsolvable. An immediate corollary is that this class has no universe-bounded formal system for either impllication or finite implication.
CS-TR-82-912
Report Number: CS-TR-82-914
Institution: Stanford University, Department of Computer Science
Title: Using string matching to compress Chinese characters
Author: Guoan, Gu
Author: Hobby, John
Date: May 1982
Abstract: A new method for font compression is introduced and compared to existing methods. A very compact representation is achieved by using a variant of McCreight's string matching algorithm to compress the bounding contour. Results from an actual implementation are given showing the improvement over other methods and how this varies with resolution and character complexity. Compression ratios of up to 150 are achieved for Chinese characters.
CS-TR-82-914
Report Number: CS-TR-82-915
Institution: Stanford University, Department of Computer Science
Title: Verification of concurrent programs: proving eventualities by well-founded ranking
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: May 1982
Abstract: In this paper, one of a series on verification of concurrent programs, we present proof methods for establishing eventuality and until properties. The methods are based on well-founded ranking and are applicable to both "just" and "fair" computations. These methods do not assume a decrcase of the rank at each computation step. It is sufficient that there exists one process which decreases the rank when activated. Fairness then ensures that the program will eventually attain its goal.
CS-TR-82-915
Report Number: CS-TR-82-922
Institution: Stanford University, Department of Computer Science
Title: An approach to verifying completeness and consistency in a rule-based expert system
Author: Suwa, Motoi
Author: Scott, A. Carlisle
Author: Shortliffe, Edward H.
Date: June 1982
Abstract: We describe a program for verifying that a set of rules in an expert system comprehensively spans the knowledge of a specialized domain. The program has been devised and tested within the context of the ONCOCIN System, a rule-based consultant for clinical oncology. The stylized format of ONCOCIN's rules has allowed the automatic detection of a number of common errors as the knowledge base has been developed. This capability suggests a general mechanism for correcting many problems with knowledge base completeness and consistency before they can cause performance errors.
CS-TR-82-922
Report Number: CS-TR-82-923
Institution: Stanford University, Department of Computer Science
Title: Explanatory power for medical expert systems: studies in the representation of causal relationships for clinical consultations
Author: Wallis, Jerold W.
Author: Shortliffe, Edward H.
Date: July 1982
Abstract: This paper reports on experiments designed to identify and implement mechanisms for enhancing the explanation capabilities of reasoning programs for medical consultation. The goals of an explanation system are discussed, as is the additional knowledge needed to meet these goals in a medical domain. We have focussed on the generation of explanations that are appropriate for different types of system users. This task requires a knowledge of what is complex and what is important; it is further strengthened by a classification of the associations or causal mechanisms inherent in the inference rules. A causal representation can also be used to aid in refining a comprehensive knowledge base so that the reasoning and explanations are more adequate. We describe a prototype system which reasons from causal inference rules and generates explanations that are appropriate for the user.
CS-TR-82-923
Report Number: CS-TR-82-926
Institution: Stanford University, Department of Computer Science
Title: Principles of rule-based expert systems
Author: Buchanan, Bruce G.
Author: Duda, Richard O.
Date: August 1982
Abstract: Rule-based expert systems are surveyed. The most important considerations are representation and inference. Rule-based systems make strong assumptions about the representation of knowledge as conditional sentences and about the control of inference in one of three ways. The problem of reasoning with incomplete or inexact information is also discussed, as are several other issues regarding the design of expert systems.
CS-TR-82-926
Report Number: CS-TR-82-927
Institution: Stanford University, Department of Computer Science
Title: Combining state machines and regular expressions for automatic synthesis of VLSI circuits
Author: Ullman, Jeffrey D.
Date: September 1982
Abstract: We discuss a system for translating regular expressions into logic equations or PLA's, with particular attention to how we can obtain both the benefits of regular expressions and state machines as input languages. An extended example of the method is given, and the results of our approach is compared with hand design; in this example we use less than twice the area of a hand-designed, machine optimized PLA.
CS-TR-82-927
Report Number: CS-TR-82-928
Institution: Stanford University, Department of Computer Science
Title: Automated ambulatory medical record systems in the U.S.
Author: Kuhn, Ingeborg M.
Author: Wiederhold, Gio
Author: Rodnick, Jonathan E.
Author: Ramsey-Klee, Diane M.
Author: Benett, Sanford
Author: Beck, Donald D.
Date: August 1982
Abstract: This report presents an overview of the developments in Automated Ambulatory Medical Record Systems (AAMRS) from 1975 to the present. A summary of findings from a 1975 state-of-the-art review is presented along with the current findings of a follow-up study of a selected number of the AAMRS operating today. The studies revealed that effective automated medical record systems have been developed for ambulatory care settings and that they are now in the process of being transferred to other sites or users, either privately or as a commericial product. Since 1975 there have been no significant advances in system design. However, progress has been substantial in terms of achieving production goals. Even though a variety of systems are commercially available, there is a continuing need for research and development to improve the effectiveness of the systems in use today.
CS-TR-82-928
Report Number: CS-TR-82-931
Institution: Stanford University, Department of Computer Science
Title: PUFF: an expert system for interpretation of pulmonary function data
Author: Aikins, Janice S.
Author: Kunz, John C.
Author: Shortliffe, Edward H.
Author: Fallat, Robert J.
Date: September 1982
Abstract: The application of Artificial Intelligence techniques to real-world problems has produced promising research results, but seldom has a system become a useful tool in its domain of expertise. Notable exceptions are the DENDRAL and MOLGEN systems. This paper describes PUFF, a program that interprets lung function test data and has become a working tool in the pulmonary physiology lab of a large hospital. Elements of the problem that paved the way for its success are examined, as are significant limitations of the solution that warrant further study.
CS-TR-82-931
Report Number: CS-TR-82-932
Institution: Stanford University, Department of Computer Science
Title: Expert systems research: modeling the medical decision making process
Author: Shortliffe, Edward H.
Author: Fagan, Lawrence M.
Date: September 1982
Abstract: During the quarter century since the birth of the branch of computer science known as artificial intelligence (AI), much of the research has focused on developing symbolic models of human inference. In the last decade several related AI research themes have come together to form what is now known as "expert systems research." In this paper we review AI and expert systems to acquaint the reader with the field and to suggest ways in which this research will eventually be applied to advanced medical monitoring.
CS-TR-82-932
Report Number: CS-TR-82-933
Institution: Stanford University, Department of Computer Science
Title: An algorithmic method for studying percolation clusters
Author: Klein, Shmuel T.
Author: Shamir, Eli
Date: September 1982
Abstract: In percolation theory one studies configurations, based on some infinite lattice, where the sites of the lattice are randomly made F (full) with probability p or E (empty) with probability 1-p. For p > $p_c$, the set of configurations which contain an infinite cluster (a connectivity component) has probability 1. Using an algorithmic method and a rearrangement lemma for Bernoulli sequences, we compute the boundary-to-body quotient of infinite clusters and prove it has the definite value (1-p)/p with probability 1.
CS-TR-82-933
Report Number: CS-TR-82-947
Institution: Stanford University, Department of Computer Science
Title: Modelling degrees of item interest for a general database query system
Author: Rowe, Neil C.
Date: April 1982
Abstract: Many databases support decision-making. Often this means choices between alternatives according to partly subjective or conflicting criteria. Database query languages are generally designed for precise, logical specification of the data of interest, and tend to be awkward in the aforementioned circumstances. Information retrieval research suggests several solutions, but there are obstacles to generalizing these ideas to most databases. To address this problem we propose a methodology for automatically deriving and monitoring "degrees of interest" among alternatives for a user of a database system. This includes (a) a decision theory model of the value of information to the user, and (b) inference mechanisms, based in part on ideas from artificial intelligence, that can tune the model to observed user behavior. This theory has important applications to improving efficiency and cooperativeness of the interface between a decision-maker and a database system.
CS-TR-82-947
Report Number: CS-TR-82-949
Institution: Stanford University, Department of Computer Science
Title: The r-Stirling numbers
Author: Broder, Andrei Z .
Date: December 1982
Abstract: The r-Stirling numbers of the first and second kind count restricted permutations and respectively restricted partitions, the restriction being that the first r elements must be in distinct cycles and respectively distinct subsets. The combinatorial and algebraic properties of these numbers, which is most cases generalize similar properties of the regular Stirling numbers, are explored starting from the above definition.
CS-TR-82-949
Report Number: CS-TR-82-950
Institution: Stanford University, Department of Computer Science
Title: Learning physical description from functional definitions, examples and precedents
Author: Winston, Patrick H.
Author: Binford, Thomas O.
Author: Katz, Boris
Author: Lowry, Michael
Date: January 1983
Abstract: It is too hard to tell vision systems what things look like. It is easier to talk about purpose and what things are for. Consequently, we want vision systems to use functional descriptions to identify things, when necessary, and we want them to learn physical descriptions for themselves, when possible. This paper describes a theory that explains how to make such systems work. The theory is a synthesis of two sets of ideas: ideas about learning from precedents and exercises developed at MIT and ideas about physical description developed at Stanford. The strength of the synthesis is illustrated by way of representative experiments. All of these experiments have been performed with an implementation system.
CS-TR-82-950
Report Number: CS-TR-82-951
Institution: Stanford University, Department of Computer Science
Title: Five paradigm shifts in programming language design and their realization in Viron, a dataflow programming environment
Author: Pratt, Vaughan
Date: December 1982
Abstract: We describe five paradigm shifts in programming language design, some old and some relatively new, namely Effect to Entity, Serial to Parallel, Partition Types to Predicate Types, Computable to Definable, and Syntactic Consistency to Semantic Consistency. We argue for the adoption of each. We exhibit a programming language, Viron, lhat capitalizes on these shifts.
CS-TR-82-951
Report Number: CS-TR-82-953
Institution: Stanford University, Department of Computer Science
Title: Partial bibliography of work on expert systems
Author: Buchanan, Bruce G.
Date: December 1982
Abstract: Since 1971 many publications on expert systems have appeared in conference proceedings and the technical literature. Over 200 titles are listed in the bibliography. Many relevant publications are omitted because they overlap publications on the list; others should be called to my attention.
CS-TR-82-953
Report Number: CS-TR-82-998
Institution: Stanford University, Department of Computer Science
Title: Knowledge engineering: a daily activity on a hospital ward
Author: Mulsant, Benoit
Author: Servan-Schreiber, David
Date: September 1983
Abstract: Two common barriers against the development and diffusion of Expert Systems in Medicine are the difficulty of design and the low level of acceptance. This paper reports on an original experience which entails potential solutions of these issues: the task of Knowledge Engineering is performed by medical students and residents on a hospital ward using a sophisticated Knowledge Acquisition System, EMYCIN. The Knowledge Engineering sessions are analysed in detail and a structured method is proposed. A transcript of a sample run of the resulting program is presented along with an evaluation of its performance, acceptance, educational potential and amount of endeavour required. The impact of the Knowledge Engineering process itself is then assessed both from the residents and the medical students standpoint. Finally, the possibility of generalizing the experiment is examined.
CS-TR-82-998
Report Number: CS-TR-83-945
Institution: Stanford University, Department of Computer Science
Title: Perseus: retrospective on a portable operating system
Author: Z waenepoel, Willy
Author: Lantz, Keith A.
Date: February 1983
Abstract: We describe the operating system Perseus, developed as part of a study into the issues of computer communications and their impact on operating system and programming language design. Perseus was designed to be portable by virtue of its kernel-based structure and its implementation in Pascal. In particular, machine-dependent code is limited to the kernel and most operating systems functions are provided by server processes, running in user mode. Perseus was designed to evolve into a distributed operating system by virtue of its interprocess communication facilities, based on message-passing. This paper presents an overview of the system and gives an assessment of how far it satisfied its original goals. Specifically, we evaluate its interprocess communication facilities and kernel-based structure, followed by a discussion of portability. We close with a brief history of the project, pointing out major milestones and stumbling blocks along the way.
CS-TR-83-945
Report Number: CS-TR-83-962
Institution: Stanford University, Department of Computer Science
Title: Bibliography of Stanford Computer Science reports, 1963-1983
Author: Berg, Kathryn A.
Date: March 1983
Abstract: This report lists, in chronological order, all reports published by the Stanford Computer Science Department since 1963. Each report is identified by a Computer Science number, author's name, title, National Technical Information Service (NTIS) retrieval number (i.e., AD-XXXXXX), date, and number of pages. If an NTIS number is not given, it means that the report is probably not available from NTIS.
CS-TR-83-962
Report Number: CS-TR-83-963
Institution: Stanford University, Department of Computer Science
Title: A hardware semantics based on temporal intervals
Author: Halpern, Joseph
Author: Manna, Z ohar
Author: Moszkowski, Ben
Date: March 1983
Abstract: We present an interval-based temporal logic that permits the rigorous specification of a variety of hardware components and facilitates describing properties such as correctness of implementation. Conceptual levels of circuit operation ranging from detailed quantitative timing and signal propagation up to functional behavior are integrated in a unified way. After giving some motivation for reasoning about hardware, we present the propositional and first-order syntax and semantics of the temporal logic. In addition we illustrate techniques for describing signal transitions as well as for formally specifying and comparing a number of delay models. Throughout the discussion, the formalism provides a means for examining such concepts as device equivalence and internal states.
CS-TR-83-963
Report Number: CS-TR-83-964
Institution: Stanford University, Department of Computer Science
Title: Proving precedence properties: the temporal way
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: April 1983
Abstract: This paper explores the three important classes of temporal properties of concurrent programs: invariance, liveness and precedence. It presents the first methodological approach to the precedence properties, while providing a review of the invariance and liveness properties. The approach is based on the 'unless' operator, which is a weak version of the 'until' operator. For each class of properties, we present a single complete proof principle. Finally, we show that the properties of each class are decidable over finite state programs.
CS-TR-83-964
Report Number: CS-TR-83-965
Institution: Stanford University, Department of Computer Science
Title: An approach to type design and text composition in Indian scripts
Author: Ghosh, Pijush K.
Date: April 1983
Abstract: The knowledge of letters exerts a dual enchantment. When it uncovers the relationships between a series of arbitrary symbols and the sounds of speech, it fills us with joy. For others the visible expression of the letters, their graphical forms, their history and their development become fascinating. The advent of digital information technology has opened new vistas in the concept of letter forms. Unfortunately the graphics industry in India has remained almost unaffected by these technological advances, especially in the field of type design and text composition. This report strives to demonstrate how to use various tools and techniques, so that the new technology can cope with the plurality of Indian scripts. To start with all you need to know is the basic shapes of the letters of the Roman alphabet and the sounds they represent. With this slender thread of knowledge an enjoyable study of letter design and text composition in Indian scripts can begin.
CS-TR-83-965
Report Number: CS-TR-83-966
Institution: Stanford University, Department of Computer Science
Title: A formal approach to lettershape description for type design
Author: Ghosh, Pijush K.
Author: Bigelow, Charles A.
Date: May 1983
Abstract: This report is designed to explore some analytic means of specifying lettershapes. Computer representation and analysis of lettershape have made use of two diametrically different approaches, one representing a shape by its boundary, the other by its skeleton or medial axis. Generally speaking, the boundary representation is conceptually simpler to the designer, but the skeletal representation provides more insight into the "piecedness" of the shape. Donald Knuth's METAFONT is one of the sophisticated lettering design systems which has basically adopted the medial axis approach. Moreover, the METAFONT system has introduced the idea of metafont-description of a letter, i.e., to give a rigorous definition of the shape of a letter in such a way that many styles are obtained from a single definition by changing only a few user-defined parameters. That is why we have considered the METAFONT system as our starting point and have shown how we can arrive at the definition of a formal language for specifying lettershapes. We have also introduced a simple mathematical model for decomposing a letter into its constituent elements.
CS-TR-83-966
Report Number: CS-TR-83-967
Institution: Stanford University, Department of Computer Science
Title: Verification of concurrent programs: a temporal proof system
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: June 1983
Abstract: A proof system based on temporal logic is presented for proving properties of concurrent programs based on the shared-variables computation model. The system consists of three parts: the general uninterpreted part, the domain dependent part and the program dependent part. In the general part we give a complete proof system for first-order temporal logic with detailed proofs of useful theorems. This logic enables reasoning about general time sequences. The domain dependent part characterizes the special properties of the domain over which the program operates. The program dependent part introduces program axioms which restrict the time sequences considered to be execution sequences of a given program. The utility of the full system is demonstrated by proving invariance, liveness and precedence properties of several concurrent programs. Derived proof principles for these classes of properties are obtained and lead to a compact representation of proofs.
CS-TR-83-967
Report Number: CS-TR-83-969
Institution: Stanford University, Department of Computer Science
Title: Reasoning in interval temporal logic
Author: Moszkowski, Ben
Author: Manna, Z ohar
Date: July 1983
Abstract: Predicate logic is a powerful and general descriptive formalism with a long history of development. However, since the logic's underlying semantics have no notion of time, statements such as "I increases by 2" cannot be directly expressed. We discuss interval temporal logic (ITL), a formalism that augments standard predicate logic with operators for time-dependent concepts. Our earlier work used ITL to specify and reason about hardware. In this paper we show how ITL can also directly capture various control structures found in conventional programming languages. Constructs are given for treating assignment, iteration, sequential and parallel computations and scoping. The techniques used permit specification and reasoning about such algorithms as concurrent Quicksort. We compare ITL with the logic-based programming languages Lucid and Prolog.
CS-TR-83-969
Report Number: CS-TR-83-971
Institution: Stanford University, Department of Computer Science
Title: Letterform design systems
Author: Ruggles, Lynn
Date: April 1983
Abstract: The design of letterforms requires a skilled hand, an eye for fine detail and an understanding of the letterforms themselves. This work has traditionally been done by experienced artisans, but in the last fifteen years there have been attempts to integrate the design process with the use of computers in order to create digital type forms. The use of design systems for the creation of these digital forms has led to an analysis of the way type designs are created by type designers. Their methods have been integrated into a variety of systems for creating digital forms. This paper describes these design systems and discusses the relevant issues for the success of the systems that exist and are used today.
CS-TR-83-971
Report Number: CS-TR-83-972
Institution: Stanford University, Department of Computer Science
Title: Experience with a regular expression compiler
Author: Karlin, Anna R.
Author: Trickey, Howard W.
Author: Ullman, Jeffrey D.
Date: June 1983
Abstract: The language of regular expressions is a useful one for specifying certain sequebtial processes at a very high level. They allow easy modification of designs for circuits, like controllers, that are described by patterns of events they must recognize and the responses they must make to those patterns. This paper discusses the compilation of such expressions into reasonably compact layouts. The translation of regular expressions into nondeterministic automata by two different methods is discussed, along with the advantages of each method. A major part of the compilation problem is selection of good state codes for the nondeterministic automata; one successful strategy is explained in the paper.
CS-TR-83-972
Report Number: CS-TR-83-973
Institution: Stanford University, Department of Computer Science
Title: The distributed V kernel and its performance for diskless workstations
Author: Cheriton, David R.
Author: Z waenepoel, Willy
Date: July 1983
Abstract: The distributed V kernel is a message-oriented kernel that provides uniform local and network interprocess communication. It is primarily being used in an environment of diskless workstations connected by a high-speed local network to a set of file servers. We describe a performance evaluation of the kernel, with particular emphasis on the cost of network file access. Our results show that over a local network: 1. Diskless workstations can access remole files with minimal performance penalty. 2. The V message facility can be used to access remote files at comparable cost to any well-tuned specialized file access protocol. We conclude that it is feasible to build a distributed system with all network communication using the V message facility even when most of the network nodes have no secondary storage.
CS-TR-83-973
Report Number: CS-TR-83-974
Institution: Stanford University, Department of Computer Science
Title: A Chinese Meta-Font
Author: Hobby, John
Author: Guoan, Gu
Date: July 1983
Abstract: METAFONT is Donald E. Knuth's system for alphabet design. The system allows an entire family of fonts or "meta-fonts" to be specified precisely and mathematically so that it can be produced in different sizes and styles for different raster devices. We present a new technique for defining Chinese characters hierarchically with METAFONT. We define METAFONT subroutines for commonly used portions of strokes and then combine some of these into routines for drawing complete strokes. Parameters describe the skeletons of the strokes and the stroke routines are carefully designed to transform themselves appropriately. This allows us to handle all of the basic strokes with only 14 different routines. The stroke routines in turn are used to build up groups of strokes and radicals. Special routines for positioning control points ensure that the strokes will join properly in a variety of different styles. The radical routines are parameterized to allow them to be placed at different locations in the typeface and to allow for adjusting their size and shape. Key points are positioned relative to the bounding box for the radical, and the special positioning routines find other points that must be passed to the stroke routines. We use this method to design high quality Song style characters. Global parameters control the style, and we show how these can be used to create Song and Long Song from the same designs. Other settings can produce other familiar styles or even new styles. We show how it is possible to create completely different styles, such as Bold style, merely by substituting different stroke routines. The global parameters can be used to augment simple scaling by altering stroke width and other details to account for changes in size. We can adjust stroke widths to help even out the overall darkness of the characters. We also show how it is possible to experiment with new ideas such as adjusting character widths individually. While many of our characters are based on existing designs, the stroke routines facilitate the design of new characters without the need to refer to detailed drawings. The skeletal parameters and special positioning routines make it easy to position the strokes properly. In our previous paper, in contrast to this, we parameterized the strokes according to their boundaries and copied an existing design. The previous approach made it very difficult to create different styles with the same METAFONT program.
CS-TR-83-974
Report Number: CS-TR-83-980
Institution: Stanford University, Department of Computer Science
Title: The WEB system of structured documentation
Author: Knuth, Donald E.
Date: September 1983
Abstract: This memo describes how to write programs in the WEB language (Version 2.3, September 1983); and it also includes the full WEB documentation for WEAVE and TANGLE, the programs that read WEB input and produce TEX and PASCAL output, respectively.
CS-TR-83-980
Report Number: CS-TR-83-985
Institution: Stanford University, Department of Computer Science
Title: First grade TEX: a beginner's TEX manual
Author: Samuel, Arthur L.
Date: November 1983
Abstract: This is an introductory ready-reference TEX82 manual for the beginner who would like to do First Grade TEX work. Only the most basic features of the TEX system are discussed in detail. Other features are summarized in an appendix and references are given to the more complete documentation available elsewhere.
CS-TR-83-985
Report Number: CS-TR-83-989
Institution: Stanford University, Department of Computer Science
Title: A programming and problem-solving seminar
Author: Knuth, Donald E.
Author: Weening, Joseph S.
Date: December 1983
Abstract: This report contains edited transcripts of the discussions held in Stanford's course CS 204, Problem Seminar, during autumn quarter 1981. Since the topics span a large range of ideas in computer science, and since most of the important research paradigms and programming paradigms were touched on during the discussions, these notes may be of interest to graduate students of computer science at other universities, as well as to their professors and to professional people in the "real world." The present report is the fourth in a series of such transcripts, continuing the tradition established in CS606 (Michael J. Clancy, 1977), CS707 (Chris Van Wyk, 1979), and CS863 (Allan A. Miller, 1981).
CS-TR-83-989
Report Number: CS-TR-83-990
Institution: Stanford University, Department of Computer Science
Title: A programming and problem-solving seminar
Author: Hobby, John D.
Author: Knuth, Donald E.
Date: December 1983
Abstract: This report contains edited transcripts of the discussions held in Stanford's course CS204, Problem Seminar, during autumn quarter 1982. Since the topics span a large range of ideas in computer science, and since most of the important research paradigms and programming paradigms were touched on during the discussions, these notes may be of interest to graduate students of computer science at other universities, as well as to their professors and to professional people in the "real world." The present report is the fifth in a series of such transcripts, continuing the tradition established in STAN-CS-77-606 (Michael J. Clancy, 1977), STAN-CS-79-707 (Chris Van Wyk, 1979), STAN-CS-81-863 (Allan A. Miller, 1981), STAN-CS-83-989 (Joseph S. Weening, 1983).
CS-TR-83-990
Report Number: CS-TR-83-991
Institution: Stanford University, Department of Computer Science
Title: Parallel algorithms for arithmetics, irreducibility and factoring of GFq-polynomials
Author: Morgensteren, Moshe
Author: Shamir, Eli
Date: December 1983
Abstract: A new algorithm for testing irreducibility of polynomials over finite fields without gcd computations makes it possible to devise efficient parallel algorithms for polynomial factorization. We also study the probability that a random polynomial over a finite field has no factors of small degree.
CS-TR-83-991
Report Number: CS-TR-83-992
Institution: Stanford University, Department of Computer Science
Title: The language of an interactive proof checker
Author: Ketonen, Jussi
Author: Weening, Joseph S.
Date: December 1983
Abstract: We describe the underlying language for EKL, an interactive theorem-proving system currently under development at the Stanford Artificial Intelligence Laboratory. Some of the reasons for its development as well as its mathematical properties are discussed.
CS-TR-83-992
Report Number: CS-TR-83-994
Institution: Stanford University, Department of Computer Science
Title: Sorting by recursive partitioning
Author: Chapiro, Daniel M.
Date: December 1983
Abstract: We present a new O(n lg lg n) time sort algorithm that is more robust than O(n) distribution sorting algorithms. The algorithm uses a recursive partition-concatenate approach, partitioning each set into a variable number of subsets using information gathered dynamically during execution. Sequences are partitioned using statistical information computed during the sort for each sequence. Space complexity is O(n) and is independent from the order and distributlon of the data. lf the data is originally in a list, only O($\sqrt{n}$) extra space is necessary. The algorithm is insensitive to the initial ordering of the data, and it is much less sensitive to the distribution of the values of the sorting keys than distribution sorting algorithms. Its worst-case time is O(n lg lg n) across all distributions that satisfy a new "fractalness" criterion. This condition, which is sufficient but not necessary, is satisfied by any set with bounded length keys and bounded repetition of each key. If this condition is not satisfied, its worst case performance degrades gracefully to O(n lg n). In practice, this occurs when the density of the distribution over $\Omega$(n) of the keys is a fractal curve (for sets of numbers whose values are bounded), or when the distribution has very heavy tails with arbitrarily long keys (for sets of numbers whose precision is bounded). In some preliminary tests, it was faster than Quicksort for sets of more than 150 elements. The algorithm is practical, works basically "in place", can be easily implemented and is particularly well suited both for parallel processing and for external sorting.
CS-TR-83-994
Report Number: CS-TR-83-995
Institution: Stanford University, Department of Computer Science
Title: The advantages of abstract control knowledge in expert system design
Author: Clancey, William J.
Date: November 1983
Abstract: A poorly designed knowledge base can be as cryptic as an arbitrary program and just as difficult to maintain. Representing control knowledge abstractly, separately from domain facts and relations, makes the design more transparent and explainable. A body of abstract control knowledge provides a generic framework for constructing knowledge bases for related problems in other domains and also provides a useful starting point for studying the nature of strategies.
CS-TR-83-995
Report Number: CS-TR-83-996
Institution: Stanford University, Department of Computer Science
Title: Strategic explanations for a diagnostic consultation system
Author: Hasling, Diane Warner
Author: Clancey, William J.
Author: Rennels, Glenn
Date: November 1983
Abstract: This paper examines the problem of automatic explanation of reasoning, especially as it relates to expert systems. By explanation we mean the ability of a program to discuss what it is doing in some understandable way. We first present a general framework in which to view explanation and review some of the research done in this area. We then focus on the explanation system for NEOMYCIN, a medical consultation program. A consultation program interactively helps a user to solve a problem. Our goal is to have NEOMYCIN explain its problem-solving strategies. An explanation of strategy describes the plan the program is using to reach a solution. Such an explanation is usually concrete, referring to aspects of the current problem situation. Abstract explanations articulate a general principle, which can be applied in different situations; such explanations are useful in teaching and in explaining by analogy. We describe the aspects of NEOMYCIN that make abstract strategic explanations possible--the representation of strategic knowledge explicitly and separately from domain knowledge--and demonstrate how this representation can be used to generate explanations.
CS-TR-83-996
Report Number: CS-TR-84-1003
Institution: Stanford University, Department of Computer Science
Title: Parallelism and greedy algorithms
Author: Anderson, Richard
Author: Mayr, Ernst
Date: April 1984
Abstract: A number of greedy algorithms are examined and are shown to be probably inherently sequential. Greedy algorithms are presented for finding a maximal path, for finding a maximal set of disjoint paths in a layered dag, and for finding the largest induced subgraph of a graph that has all vertices of degree at least k. It is shown that for all of these algorithms, the problem of determining if a given node is in the solution set of the algorithm is P-complete. This means that it is unlikely that these sequential algorithms can be sped up significantly using parallelism.
CS-TR-84-1003
Report Number: CS-TR-84-1004
Institution: Stanford University, Department of Computer Science
Title: A computational theory of higher brain function
Author: Goldschlager, Leslie M.
Date: April 1984
Abstract: The higher functions of the brain are believed to occur in the cortex. This region of the brain is modelled as a memory surface which performs both storage and computation. Concepts are modelled as patterns of activity on the memory surface, and the model explains how these patterns interact with one another to give the computations which the brain performs. The method of interaction can explain the formation of abstract concepts, association of ideas and train of thought. It is shown that creativity, self, consciousness and free will are explainable within the same framework. A theory of sleep is presented which is consistent with the model.
CS-TR-84-1004
Report Number: CS-TR-84-1005
Institution: Stanford University, Department of Computer Science
Title: Adequate proof principles for invariance and liveness properties of concurrent programs
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: May 1984
Abstract: This paper presents proof principles for establishing invariance and liveness properties of concurrent programs. Invariance properties are established by systematically checking that they are preserved by every atomic instruction in the program. The methods for establishing liveness properties are based on 'well-founded asserations' and are applicable to both "just" and "fair" computations. These methods do not assume a decrease of the rank at each computation step. It is sufficient that there exists one process which decreases the rank when activated. Fairness then ensures that the program will eventually attain its goal. In the finite state case such proofs can be represented by diagrams. Several examples are given.
CS-TR-84-1005
Report Number: CS-TR-84-1006
Institution: Stanford University, Department of Computer Science
Title: EKL - an interactive proof checker user's reference manual
Author: Ketonen, Jussi
Author: Weening, Joseph S.
Date: June 1984
Abstract: EKL is an interactive proof checker and constructor. Its main goal is to facilitate the checking of mathematical proofs. Some of the special features of EKL are: * The language of EKL can be extended all the way to finite-order predicate logic with typed lambda-calculus. * Several proofs can be handled at the same time. * Metatheoretic reasoning allows formal extensions of the capabilities of EKL. * EKL is a programmable system. The MACLISP language is available to the user, and LISP functions can be written to create input to EKL, thereby allowing expression of proofs in an arbitrary input language. This document is a reference manual for EKL. Each of the sections discusses a major part of the language, beginning with an overview of that area, and proceeding to a detailed discussion of available features. To gain an acquaintance with EKL, it is recommended that you read only the introductory part of each section. EKL may be used both at the Stanford Artificial Intelligence Laboratory (SAIL) computer system, and on DEC TOPS-20 systems that support MACLISP.
CS-TR-84-1006
Report Number: CS-TR-84-1007
Institution: Stanford University, Department of Computer Science
Title: Queue-based multi-processing Lisp
Author: Gabriel, Richard P.
Author: McCarthy, John
Date: June 1984
Abstract: This report presents a dialect of Lisp, called QLAMBDA, which supports multi-processing. Along with the definition of the dialect, the report presents programming examples and performance studies of some programs written in QLAMBDA. Unlike other proposed multi-processing Lisps, QLAMBDA provides only a few very powerful and intuitive primitives rather than a number of parallel variants of familiar constructs.
CS-TR-84-1007
Report Number: CS-TR-84-1009
Institution: Stanford University, Department of Computer Science
Title: Complexity of a top-down capture rule
Author: Sagiv, Yehoshua
Author: Ullman, Jeffrey D.
Date: July 1984
Abstract: Capture rules were introduced in [U] as a method for planning the evaluation of a query expressed in first-order logic. We examine a capture rule that is substantiated by a simple top-down implementation of restricted Horn clause logic. A necessary and sufficient condition for the top-down algorithm to converge is shown. It is proved that, provided there is a bound on the number of arguments of predicates, the test can be performed in polynomial time; however, if the arity of predicates is made part of the input, then the problem of deciding whether the top-down algorithm converges is NP-hard. We then consider relaxation of some of our constraints on the form of the logic, showing that success of the top-down algorithm can still be tested in polynomial time if the number of arguments is limited and in exponential time if not.
CS-TR-84-1009
Report Number: CS-TR-84-1012
Institution: Stanford University, Department of Computer Science
Title: TABLOG: the deductive-tableau programming language
Author: Malachi, Yonathan
Author: Manna, Z ohar
Author: Waldinger, Richard
Date: June 1984
Abstract: TABLOG (Tableau Logic Programming Language) is a language based on first-order predicate logic with equality that combines functional and logic programming. TABLOG incorporates advantages of LISP and PROLOG. A program in TABLOG is a list of formulas in a first-order logic (including equality, negation, and equivalence) that is more general and more expressive than PROLOG's Horn clauses. Whereas PROLOG programs must be relational, TABLOG programs may define either relations or functions. While LISP programs yield results of a computation by returning a single output value, TABLOG programs can be relations and can produce several results simultaneously through their arguments. TABLOG employs the Manna-Waldinger deductive-tableau proof system as an interpreter in the same way that PROLOG uses a resolution-based proof system. Unification is used by TABLOG to match a call with a line in the program and to bind arguments. The basic rules of deduction used for computing are nonclausal resolution and rewriting by means of equality and equivalence. A pilot interpreter for the language has been implemented.
CS-TR-84-1012
Report Number: CS-TR-84-1014
Institution: Stanford University, Department of Computer Science
Title: A P-complete problem and approximations to it
Author: Anderson, Richard
Author: Mayr, Ernst W.
Date: September 1984
Abstract: The P-complete problem that we will consider is the High Degree Subgraph Problem. This problem is: given a graph G = (V,E) and an integer k, find the maximum induced subgraph of G that has all nodes of degree at least k. After showing that this problem is P-complete, we will discuss two approaches to finding approximate solutions to it in NC. We will give a variant of the problem that is also P-complete that can be approximated to within a factor of c in NC, for any c < 1/2, but cannot be approximated by a factor of better than 1/2 unless P = NC. We will also give an algorithm that finds a subgraph with moderately high minimum degree. This algorithm exhibits an interesting relationship between its performance and the time it takes.
CS-TR-84-1014
Report Number: CS-TR-84-1018
Institution: Stanford University, Department of Computer Science
Title: Classification problem solving
Author: Clancey, William J.
Date: July 1984
Abstract: A broad range of heuristic programs--embracing forms of diagnosis. catalog selection, and skeletal planning--accomplish a kind of well-structured problem solving called classification. These programs have a characteristic inference structure that systematically relates data to a pre-enumerated set of solutions by abstraction, heuristic association, and refinement. This level of description specifies the knowledge needed to solve a problem, independent of its representation in a particular computer language. The classification problem-solv