关于图的导出森林独立系统

本文研究图的导出森林独立系统.在这个独立系统中,独立集是指导出子图不含圈的点子集.文中证明了图G的导出森林独立系统是拟阵当且仅当G是块森林.文中同时给出了在强弦图上求最大导出森林的多项式算法.     

An algebraic certificate for Budan’s theorem

The existing algorithms to construct the real closure of an ordered field involve very high complexities. These algorithms are based on Sturm’s theorem which we suspect to be one reason for the complexities since all known proofs of Sturm’s theorem use Rolle’s theorem which is problematic in a constructive context.Therefore we propose to replace the use of Sturm’s theorem by Budan’s theorem. In this paper we present as a first step in this direction an algebraic certificate for Budan’s theorem. An algebraic certificate is a certain kind of proof of a statement. In particular, it is an algorithm which produces, from an arbitrary data in the premise of the statement, explicit (in)equalities which express the conclusion.     

Performance bounds on multiprocessor scheduling strategies for statically allocated programs

In multiprocessors with static allocation of processes to processors, scheduling can be done locally for each processor. The scheduling strategy may have dramatic effect on the execution time of a parallel program. It is an NP-hard problem to find an optimal schedule, and very little is known of how close the heuristic solutions get.The major result here is a theorem stating that if certain program parameters, which can be obtained from an execution of the program on a single-processor, are known, the execution time of the optimal schedule can be calculated within a factor equal to the largest number of border processes on one processor. Border processes are processes which communicate with other processors. The program parameters are obtained using a previously developed tool.Due to the generality of this theorem, the proof is rather complex because it has to cover a large range of situations. The theorem itself, however, is easy to apply, making it possible to compare the performance of different scheduling strategies with the optimal case. The proof also gives important hints on how to design efficient scheduling algorithms for statically allocated programs.     

Thinking and Turing's test

The questions raised by A. M. Turing in his paper on thought and machines are discussed. Human thought is considered in turn as a concept of normal language usage, as a basic concept of psychology, and as the basis of intellectual activity. It is concluded that neither of these notions of thought identifies something specific that a human being can or cannot do. The imitation game proposed by Turing for deciding whether a machine can think is found to result from an arbitrary empoverishment of the channel of communication between the interrogator and the item under investigation. Turing's notions of thinking are shown to lead to logical difficulties. An alternative view of consciousness, that would place it beyond the reach of any finite test, is finally discussed.     

Disk allocation methods for binary Cartesian product files

Since a file is usually stored on a disk, the response time to a query is dominated by the disk access time. In order to reduce the disk access time, a file can be stored on several independently accessible disks. In this paper, we discuss the problem of allocating buckets in a file among disks such that the maximum disk accessing concurrency can be achieved. We are particularly concerned with the disk allocation problem for binary Cartesian product files. A new allocation method is first proposed for the cases when the number (m) of available disks is a power of 2. Then it is extended to fit the cases wherem is not a power of 2. The proposed algorithm has a near strict optimal performance for a partial match query in which the number of unspecified attributes is greater than a small number (5 or 6).This work was supported in part by NSF Grant DCR-8405498.     

WEAK CONVERGENCE OF HENSTOCK INTEGRABLE SEQUENCES

Some relationships between pointwise and weak convergence of a sequence of Henstock integrable functions are studied, In particular it is provided an example of a sequence of Henstock integrable functions whose pointwise limit is different from the weak one. By introducing an asymptotic version of the Henstock equiintegrability notion it is given a necessary and sufficient condition in order that a pointwisely convergent sequence of Henstock integrable functions is weakly convergent to its pointwise limit.     

On specifications,subset types and interpretation of proposition in type theory

In this paper we discuss some practical aspects of using type theory as a programming and specification language, where the viewpoint is to use it not only as a basis for program synthesis but also as a programming language with a programming logic allowing us to do ordinary verification.The subset type has been added to type theory in order to avoid irrelevant information in programs. We give an example of a proof which illustrates the problems that may occur if the subset type is used in specifications when we have the standard interpretation of propositions as types. Harrop-formulas and Squash are then discussed as solutions to these problems. It is argued that they are not acceptable from a practical point of view.An extension of the theory to include the two new judgment forms:A is a proposition, andA is true, is then given and explained in terms of the old theory. The logical constants are no longer identified with the corresponding type theoretical constants, but propositions are interpreted as Gödel formulas, which allow us to introduce and justify logical rules similar to rules for classical logic. The interpretation is extended to include predicates defined by using reflections of the ordinary definition of Gödel formulas in a type of small propositions.The programming example is then revisited and stronger elimination rules are discussed.     

On the design of reactive systems

The notion of joint actions provides a framework in which the granularity of atomic actions can be refined in the design of concurrent systems. An example of a telephone exchange is elaborated to demonstrate the feasibility of this approach for reactive systems and to illustrate transformations that are justifiable in such a process. Particular problems arise when a refinement would allow new interleavings of semantically relevant events. The meaning of a reactive computation is specified in a way that makes this possible.Dedicated to Peter Naur on the occasion of his 60th birthday     

Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation

We prove the correctness of an algorithm for normalizing untyped combinator terms by evaluation. The algorithm is written in the functional programming language Haskell, and we prove that it lazily computes the combinatory Böhm tree of the term. The notion of combinatory Böhm tree is analogous to the usual notion of Böhm tree for the untyped lambda calculus. It is defined operationally by repeated head reduction of terms to head normal forms. We use formal neighbourhoods to characterize finite, partial information about data, and define a Böhm tree as a filter of such formal neighbourhoods. We also define formal topology style denotational semantics of a fragment of Haskell following Martin-Löf, and let each closed program denote a filter of formal neighbourhoods. We prove that the denotation of the output of our algorithm is the Böhm tree of the input term. The key construction in the proof is a “glueing” relation between terms and semantic neighbourhoods which is defined by induction on the latter. This relation is related to the glueing relation which was earlier used for proving the correctness of normalization by evaluation algorithm for typed combinatory logic.     

二阶Melnikov函数及其应用

在Ｍｅｌｎｉｋｏｖ函数的种种应用中，目前常见到的仅是一阶形式。本文具体推导了二阶Ｍｅｌｎｉｋｏｖ函数的分析表达，提出了临界情况下考察双曲鞍点的稳定流形与不稳定流形相对位置的二阶判据，并成功地用于环面ｖａｎｄｅｒＰｏｌ方程的研究中。     

Terminating general recursion

In Martin-Löf's type theory, general recursion is not available. The only iterating constructs are primitive recursion over natural numbers and other inductive sets. The paper describes a way to allow a general recursion operator in type theory (extended with propositions). A proof rule for the new operator is presented. The addition of the new operator will not destroy the property that all well-typed programs terminate. An advantage of the new program construct is that it is possible to separate the termination proof of the program from the proof of other properties.Dedicated to Peter Naur on the occasion of his 60:th birthday.     

Page usage in a quadtree index

This paper provides a characterization of the storage needs of a quadtree when used as an index to access large volumes of 2-dimensional data. It is shown that the page occupancy for data in random order approaches 33%. A precise mathematical analysis that involves a modicum of hypergeometric functions and dilogarithms, together with some computer algebra is presented.A brief survey of the analysis of storage usage in tree structures is included. The 33% ratio for quadtrees is to be compared to the figures for binary search trees (50%), tries (69%), and quadtries (46%).The research of this author was done while visiting INRIA, Rocquencourt, France under support from the Ministry of Education of Japanese Government.Work of this author was supported in part by the Basic Research Action of the E.C. under contract No. 3075 (Project ALCOM).     

Uncle-attributed grammars

Evaluation of inherited attributes is a problem in conjunction with LR parsing, because the derivation tree is incomplete during parsing. An evaluation scheme for inherited attributes is presented based on a restricted grammar class, uncle-attributed grammars. A transformation to the uncle-attributed form is described for L-attributed grammars.     

An axiomatic semantics for nested concurrency

We give transformation rules for the concurrent parts of Hoare's language CSP, transforming concurrent CSP programs into nondeterministic, sequential programs.On the basis of these transformations we define an axiomatic semantics for CSP with nested concurrency.This axiomatic system includes a rule for binary, associative process composition, enabling modular verification dealing with parts of concurrent systems as well as full programs.The proof system is fully abstract, in the sense that the internal structure of processes is irrelevant in the specification inasmuch it is not externally observable.An outline of a verification of a recursive, concurrent sorter is given as an example.     

求解大型线性方程组的一类非定常内外迭代法

1 引 言 求解大型线性方程组 Ax=b, A∈R~(?),det(A)≠0. x,b∈R~n (1.1)的内外迭代法,首先由Nichols于1973年提出。由于这类算法在求解大型问题。特别对由边值问题离散化得到的大型稀疏方程组求解,显示了优越性,而受到众多的关注。1991年,Lanzkron.Rose.Szvld等人进一步降其发展成为成套迭代法,为预条件组的近似及同步和     

Verification of a class of self-timed computational networks

A mathematical model for systolic networks is generalized and applied to a class of VLSI cellular networks which is defined to include both systolic and self-timed networks. The general model is kept simple by assuming that a computation does not deadlock, that is by separating the verification of liveness from the the verification of the results. The main contribution of this paper concerns the study of deadlock in self-timed computational networks. More specifically, an algebra of events is developed and used to prove that the liveness of any self-timed network is determined uniquely by its initial state. Moreover, a method is presented for the verification of liveness in networks preset to given initial states.This work was supported in part under ONR contract N00014-80-C-0455.     

A constant-time channel-assignment algorithm on reconfigurable meshes

The channel-assignment problem is central to the integrated circuit fabrication process. Given a two-sided printed circuit board, we wish to maken pairs of components electrically equivalent. The connections are made using two vertical runs along with a horizontal one. Each horizontal run lies in a channel. The channel-assignment problem involves minimizing the total number of channels used.Recent advances in VLSI have made it possible to build massively parallel machines. To overcome the inefficiency of long distance communications among processors, some parallel architectures have been augmented by bus systems. If such a bus system can be dynamically changed to suit communication needs among processors, it is referred to asreconfigurable. The reconfigurable mesh is one of the practical models featuring a reconfigurable bus system. In this paper, we propose a constant-time algorithm to solve the channel-assignment problem of sizen on a reconfigurable mesh of sizen×n.This work was supported by NASA under grant NCC1-99.Additional support by the National Science Foundation under grant CCR-8909996 is gratefully acknowledged.     

一类非拟Newton算法及其收敛性

本文对求解无约束最优化问题提出一类非拟Ｎｅｗｔｏｎ算法，此方法同样具有二次终止性，产生的矩阵序列保持正定对称传递性，并证明了新类中的任何一种算法的全局收敛和超线性收敛性。     

A heuristic file reorganization algorithm based on record clustering

The problem of file organization which we consider involves altering the placement of records on pages of a secondary storage device. In addition, we want this reorganization to be done in-place, i.e., using the file's original storage space for the newly reorganized file. The motivation for such a physical change is to improve the database system's performance. For example, by placing frequently and jointly accessed records on the same page or pages, we can try to minimize the number of page accesses made in answering a set of queeries. The optimal assignment (or reassignment) of records to clusters is exactly what record clustering algorithms attempt to do. However, record clustering algorithms usually do not solve the entire problem, i.e., they do not specify how to efficiently reorganize the file to reflect the clustering assignment which they determine. Our algorithm is a companion to general record clustering algorithms since it actually transforms the file. The problem of optimal file reorganization isNP-hard. Consequently, our reorganization algorithm is based on heuristics. The algorithm's time and space requirements are reasonable and its solution is near optimal. In addition, the reorganization problem which we consider in this paper is similar to the problem of join processing when indexes are used.The research of this author was partially supported by the National Science Foundation under grant IST-8696157.     

A reciprocal confluence tree unit and its applications

A theorem by Jaeschke is generalized in this paper and a fast and efficient implementation called Reciprocal Confluence Tree unit for implementing the new theorem is sketched. We shall show that it can be used to solve two problems: a hashing algorithm design problem and an access control mechanism design problem.