perm filename ELEVEN.PUB[BIB,CSR]4 blob sn#576647 filedate 1981-04-06 generic text, type C, neo UTF8
C00001 00001
C00003 00002	.require  "setup.csr[bib,csr]"  source   file  
C00006 00003	%3STAN-CS-80-828:  
C00008 00004	%3STAN-CS-80-829:  
C00010 00005	%3STAN-CS-80-830:  
C00012 00006	%3STAN-CS-80-831:
C00015 00007	%3STAN-CS-80-832:  
C00017 00008	%3STAN-CS-80-833:
C00020 00009	%3STAN-CS-80-834:
C00023 00010	%3STAN-CS-80-835:
C00026 00011	%3STAN-CS-81-836:  
C00029 00012	%3STAN-CS-81-837:  
C00030 00013	%3STAN-CS-81-838:  
C00032 00014	%3STAN-CS-81-839:  
C00034 00015	%3STAN-CS-81-840:  
C00036 00016	%3STAN-CS-81-841:  
C00037 00017	%3STAN-CS-80-842:
C00039 00018	%3STAN-CS-81-843:
C00044 00019	%3STAN-CS-81-844:
C00046 00020	%3STAN-CS-81-845:
C00049 ENDMK
.require  "setup.csr[bib,csr]"  source   file;  
.once  center   
%3Stanford University Computer Science Reports%1
List Number 11↔April 1981

Listed here are  abstracts of  the most  recent reports  published by  the
Department of Computer Science at Stanford University.

%3Request Reports:%1  Complete the  enclosed order  form, and  return  the
entire order form page (including mailing label) as soon as possible.   In
many cases we can print only a limited number of copies, and requests will
be filled  on a  first come,  first  served basis  as the  reports  become
available.  If the code (FREE) is printed on your mailing label, you  will
not be charged  for hardcopy.   be charged for  hardcopy.  This  exemption
from payment is limited  primarily to university  libraries which have  an
exchange  agreement  with  our  Computer  Science  Library.   Because   of
increased costs, we have had  to reduce the number  of people in the  FREE
category.  (California sales tax will be  added at the time of  invoicing.
%2Please send no money now, wait until you get an invoice.%1)

%3Alternatively:%1 Copies of most Stanford  CS Reports may be obtained  by
writing (about 2 months after the  ''Most Recent CS Reports'' listing)  to
National Technical Information Service, 5285 Port Royal Road, Springfield,
Virginia 22161.   Stanford Ph.D.   theses  are available  from  University
Microfilms, 300 North Zeeb Road, Ann Arbor, Michigan 48106.

%2Breaking Paragraphs Into  Lines%1
by Donald E.  Knuth and Michael F. Plass (66 pages, November 1980)

This paper discusses a new approach to the problem of dividing the text of
a paragraph into lines  of approximately equal  length. Instead of  simply
making decisions one line at a time, the method considers the paragraph as
a whole, so that the final appearance of a given line might be  influenced
by the text on succeeding lines. A system based on three simple  primitive
concepts called 'boxes', 'glue', and  'penalties' provides the ability  to
deal satisfactorily  with a  wide  variety of  typesetting problems  in  a
unified framework,  using  a  single  algorithm  that  determines  optimum
breakpoints. This algorithm avoids backtracking by a judicious use of  the
techniques of  dynamic  programming.  Extensive  computational  experience
confirms that the approach  is both efficient  and effective in  producing
high-quality  output.  The  paper  concludes  with  a  brief  history   of
line-breaking methods,  and an  appendix presents  a simplified  algorithm
that requires comparatively few resources.

%2The Dinner Table Problem%1 
by Bengt Aspvall and Frank Liang (13 pages, December 1980)

This report contains two  papers inspired by  the "dinner table  problem":
If %2n%1 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 %2e∩[-2]%1 as %2n → %5α∞%1, 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.

%2Two Linear-Time Algorithms for Five-Coloring a Planar Graph%1 
by  David Matula,  Yossi  Shiloach and  Robert Tarjan  (23  pages, December 1980)

A "sequential processing" algorithm  using bicolor interchange that  five-
colors an  %2n%1 vertex  planar  graph in  O(%2n%1↑2)  time was  given  by
Matula, Marble, and  Isaacson [MMI 72].   Lipton and Miller  used a  "bach
processing" algorithm with  bicolor interchange for  the same problem  and
achieved an improved O(%2n%1 log %2n%1) time bound [LM 78].  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(%2n%1) time.

%2An O(nm log n) Algorithm for Maximum Network Flow%1
by Daniel D. K. Sleator (Thesis, 81 pages, December 1980)

This thesis presents a new algorithm for the maximum network flow problem.
The problem is this:   Given a directed network  of %2m%1 edges and  %2n%1
vertices with two distinguished vertices, a source and a sink, and with  a
nonnegative capacity associated with each edge, find a way of labeling the
edges with nonnegative real numbers representing flow in such a way that:

(1) The flow into each  vertex equals the flow  out (except at the  source
    and sink).  
(2) The flow at each edge does not exceed the capacity at that edge.
(3) The  flow  out  of  the source  is  a  maximum  over-all  flow
    satisfying (1) and (2).

Our algorithm finds a maximum flow  in O(%2nm%1log%2n%1) time, which is  a
factor of  log %2n%1  faster  than the  previous fastest  algorithm.   The
central innovation of our algorithm is a sophisticated data structure that
is used to represent a  certain subset of edges  that form a forest.   The
edges of this forest are further partitioned into two classes: broken  and
solid.  Long paths  of solid edges  are grouped together  and stored in  a
balanced tree data structure called a  biased 2-3 tree.  Each leaf of  the
biased 2-3 tree corresponds to an edge in the path.

%2Scheduling Wide  Graphs%1 
by Danny  Dolev (43  pages, December 1980)

The problem of scheduling a partially ordered set of unit length tasks  on
%2m%1 identical  processors is  known to  be %2NP%1-complete.   There  are
efficient algorithms for only 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 %2m%1 -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.

%2Graph Separator Theorems and Sparse Gaussian Elimination%1
by John Russell Gilbert (Thesis, 104 pages, December 1980)

Much of  the process  of  making computer  programs consists  of  creating
methods  for  the  manipulation  of  discrete,  finite  objects  such   as
characters,  vectors,  sets,  graphs,  and  permutations.   "Combinatorial
algorithms" is  the  awkward  but  serviceable name  for  this  branch  of
computer science.   Designing efficient  combinatorial algorithms  usually
involves  applying  or  inventing   subtle  data  structures  and   search
techniques, and is often associated with mathematics of significant  depth
and beauty.  This association gives the  subject an appeal beyond that  of
usefulness:  Combinatorial algorithms are fun.

Like most branches of mathematics and science, the study of  combinatorial
algorithms began as a collection of loosely related tricks, constructions,
and special insights.  As the  discipline has matured, unifying ideas  and
principles have begun to  emerge.  One central theme  is the formation  of
complex data structures (together with algorithms for their  manipulation)
out of simpler data structures.  A body of well-known representations  for
basic data  structures  such  as  queues and  graphs  has  grown  up,  and
continues to  expand.  Another  theme is  the use  of such  paradigms  for
algorithm design as divide-and-conquer, search, and dynamic programming.

%2Numerical Solution of the Biharmonic Equation%1
by Petter E. Bjorstad (Thesis, 139 pages, December 1980)

The numerical solution of discrete approximations to the first  biharmonic
boundary value problem in rectangular domains is studied.  Several  finite
difference schemes are compared  and a family of  new fast algorithms  for
the solution  of the  discrete systems  is developed.   These methods  are
optimal, having a theoretical computational complexiy of O(N↑2) arithmetic
operations and  requiring  N↑2+O(N)  storage locations  when  solving  the
problem on an N by N grid.  Several practical computer implementations  of
the algorithm are discussed  and compared.  These implementations  require
aN↑2 + bN↑2logN arithmetic operations with b<<a . The algorithms take full
advantage of vector or parallel computers and can also be used to solve  a
sequence of  problems  efficiently.  A  new  fast direct  method  for  the
biharmonic problem on a disk is also  developed.  It is shown how the  new
method of solution is related  to the associated eigenvalue problem.   The
results  of  extensive  numerical  tests  and  comparisons  are   included
throughout the dissertation.

It is believed that the material presented provides a good foundation  for
practical computer implementations and that the numerical solution of  the
biharmonic equation in rectangular domains from now on, will be considered
no more difficult than Poisson's equation.

%2Approximation and Optimization of Electron Density Maps%1
by Eric H. Grosse (Thesis, 118 pages, December 1980)

The three-dimensional structure  of proteins is  commonly determined  from
x-ray diffraction  data  by  manually  inspecting  the  electron  density,
displayed  as  a  stack  of  two  dimensional  contour  maps.   A  network
connecting peaks and passes of the density function has been suggested  as
a representation  more suitable  for automatic  interpretation.   However,
locating all critical points of such a complicated function is a difficult

The solution  proposed here  is to  partition the  domain into  cubes  and
approximate the density  function on each  cube by a  polynomial of  three
variables, chosen so that all first derivatives are continuous across  the
cube boundaries.  Two algorithms are examined for this approximation:  one
is least squares fitting with smooth tent-shaped basis functions (known as
tensor product  B-splines) by  repeated  univariate least  squares  spline
fits, and the other  scales Fourier coefficients  of the electron  density
function.  Critical points can then be sought independently on each  cube.
One variable is  solved for  immediately in terms  of the  other two;  the
resulting two-dimensional  problems  are  approximated on  a  subgrid  and
finally reduced  to  one-dimensional  quadratic  equations.   This  method
locates critical points more accurately than discrete pattern matching and
more quickly than repeated Newton searches.

%2Temporal Verification of Concurrent Programs, Part I: The Temporal Framework
for Concurrent  Programs%1 
by Zohar Manna and  Amir Pnueli (70 pages, January 1981)

This is the  first in a  series of reports  describing the application  of
Temporal  Logic  to  the  specification  and  verification  of  concurrent

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 about  those
execution states and 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  %2Invariance%1
(Safety),   %2Eventuality%1   (Liveness),   and   %2Precedence%1   (Until)
properties.  Among  the  properties  studied  are:   Partial  Correctness,
Global Invariance,  Clean Behavior,  Mutual Exclusion,  Deadlock  Absence,
Termination, Total  Correctness, Intermittent  Assertions,  Accessibility,
Starvation Freedom, Responsiveness, Safe Liveness, Absence of  Unsolicited
Response, Fair Responsiveness, and Precedence.

In the following reports of this series, we use the temporal formalism  to
develop proof methodologies for proving the properties discussed here.

%2Research on Expert Systems%1 
by Bruce G. Buchanan (38 pages, February 1981)

All Al 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.

%2Dynamic Program Building%1 
by Peter Brown (13  pages, February 1981)

This report argues that  programs are better  regarded as dynamic  running
objects rather  than as  static textual  ones.  The  concept of  %2dynamic
building%1, whereby a  program is  constructed as it  runs, is  described.
The report then describes the %2Build%1 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.

%2Short Waits%1 
by Arthur L. Samuel (37 pages, February 1981)

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.

%2Verification of Link-Level  Protocols%1 
by Donald  E. Knuth (6 pages, January 1981)

Stein Krogdahl [1] has given  an interesting demonstration of the  partial
correctness of  a  "protocol  skeleton",  by which  the  validity  of  the
essential aspects of a large variety  of data transmission schemes can  be
demonstrated.  The purpose  of this note  is to present  a simpler way  to
obtain the same  results, by  first establishing  the validity  of a  less
efficient skeleton  and then  "optimizing"  the algorithms.   The  present
approach, which was introduced for a particular protocol by N. V. Stenning
[2],  also  solves  a  wider  class  of  problems  that  do  not   require
first-in-first-out transmissions.

%2Huffman's Algorithm via Algebra%1 
by Donald E.  Knuth (6 pages, March 1981)

The  well-known  algorithm  of  David  A.  Huffman  for  finding   minimum
redundancy codes has found many diverse applications, and in recent  years
it has been extended in a variety of ways.  The purpose of this note is to
discuss a simple algebraic approach that  seems to fit essentially all  of
the applications of Huffman's method that are presently known.

%2The Role of Plans In Intelligent Teaching Systems%1
by Michael R. Genesereth (19 pages, November 1980)

One of the keys to effective remedial instruction is information about the
student's beliefs  and  misconceptions.   This information  can  often  be
obtained by  analyzing  the student's  efforts  in solving  problems  that
require knowledge of the subject matter.  In some areas, it is possible to
design diagnostic  tests  that  can  pinpoint  a  student's  misconception
directly from  his answers.   For  example, in  their  work on  the  Buggy
system,  Burton  adn  Brown  developed  a  methodology  for  automatically
generting  diagnostic  tests  that   discoffer  the  underlying   problems
responsible for a  student's errors in  subtraction.  However, in  subject
areas where the student chooses his own problem or when there are  several
ways of  solving  a  problem, it  is  helpful  to consider  not  only  the
student's final answer but also his steps in producing it.  This paper  is
concerned with the process of automatically analyzing a student's steps to
infer his rationale for taking those steps and the use of this information
in providing remediation tailored to the student.

%2Temporal Verification of Concurrent Programs, Part II: Proving Invariances%1
by Zohar Manna and Amir Pnueli (30 pages, March 1981)

In this report,  the second  of a series  on the  application of  temporal
logic to concurrent programs, we  concentrate on developing proof  methods
for establishing %2Invariance%1 (Safety) properties.  These are properties
that  remain  true  throughout  a  computation.   Examples  of  invariance
properties are:  Partial Correctness,  Global Invariance, Clean  Behavior,
Mutual Exclusion, and Deadlock Absence.

We formulate  a  single uniform  proof  principle based  on  computational
induction for proving  the invariance of  assertions.  We present  several
sample programs and  the invariant  assertions needed  to establish  their
properties. The assertions are  proved to be  invariant using the  uniform
proof principle.

For a restricted class of concurrent programs we present an algorithm  for
the automatic derivation of invariant assertions.  Finally, we compare our
formulation of the proof principle with other existing methods for proving

%2Temporal Verification of Concurrent Programs, Part III: Proving Eventualities%1
by Zohar Manna and Amir Pnueli (35 pages, March 1981)

In this report, the third of a series on the application of temporal logic
to concurrent programs,  we concentrate  on developing  proof methods  for
establishing %2Eventuality%1 (Liveness) properties.

In order to establish eventuality properties we present several principles
which  translate  the  structure  of  the  program  into  basic   temporal
statements  about  its  behavior.   These  principles  can  be  viewed  as
providing the temporal  semantics of  the program.   The basic  statements
thus derived are then combined into temporal proofs for the  establishment
of eventuality  properties.   All the  methods  are amply  illustrated  by

%2Temporal Verification of Concurrent Programs, Part IV: The Non-Temporal
by Zohar Manna and Amir Pnueli (45 pages, March 1981)

In this paper we consider proofs of properties of concurrent programs.  We
use the temporal formalism to state the properties but not to prove  them.
We present proof principles which  are based on convergence functions  and
well-founded structures.

The main goal is to establish properties (%2fair correctness%1) that  hold
for all  fair  computations. For  this  purpose, we  first  develop  proof
principles for the  related notions  of unrestricted,  impartial and  just
correctness, and then state  a proof principle  for fair correctness.  The
principles are illustrated by examples.


STAN-CS-79-717 (AIM-324), Robert Cartwright and John McCarthy, %2Recursive Programs
as Functions in a First Order Theory%1

STAN-CS-80-817, Jeffrey Scott Vitter (Thesis), %2Analysis of Coalesced Hashing%1

STAN-CS-80-790 (AD-A086 838), Gio Wiederhold, %2Databases in Health Care%1

STAN-CS-80-791, Clark R. Wilcox, Mary L. Dageforde & Gregory A. Jirak,%2MAINSAIL
Language Manual%1