perm filename ELEVEN.PUB[BIB,CSR] blob sn#580987 filedate 1981-04-23 generic text, type C, neo UTF8
```COMMENT ⊗   VALID 00018 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	%3STAN-CS-80-829:
C00010 00003	%3STAN-CS-80-830:
C00012 00004	%3STAN-CS-80-831:
C00015 00005	%3STAN-CS-80-832:
C00017 00006	%3STAN-CS-80-833:
C00020 00007	%3STAN-CS-80-834:
C00023 00008	%3STAN-CS-80-835:
C00026 00009	%3STAN-CS-81-836:
C00029 00010	%3STAN-CS-81-837:
C00030 00011	%3STAN-CS-81-838:
C00032 00012	%3STAN-CS-81-839:
C00034 00013	%3STAN-CS-81-840:
C00036 00014	%3STAN-CS-81-841:
C00037 00015	%3STAN-CS-80-842:
C00039 00016	%3STAN-CS-81-843:
C00044 00017	%3STAN-CS-81-844:
C00046 00018	%3STAN-CS-81-845:
C00049 ENDMK
C⊗;
%3STAN-CS-80-829:
%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.

%3STAN-CS-80-830:
%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.

%3STAN-CS-80-831:
%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.

%3STAN-CS-80-832:
%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.

%3STAN-CS-80-833:
%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.

%3STAN-CS-80-834:
%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.

%3STAN-CS-80-835:
%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
problem.

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.

%3STAN-CS-81-836:
%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
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 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.

%3STAN-CS-81-837:
%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.

%3STAN-CS-81-838:
%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.

%3STAN-CS-81-839:
%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.

%3STAN-CS-81-840:
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.

%3STAN-CS-81-841:
%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.

%3STAN-CS-80-842:
%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.

%3STAN-CS-81-843:
%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,

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
invariance.

%3STAN-CS-81-844:
%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
examples.

%3STAN-CS-81-845:
%2Temporal Verification of Concurrent Programs, Part IV: The Non-Temporal
Alternative%1
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.

ERRATA:

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
```