Partial inductive definitions as type-systems for λ-terms

To every partial inductive definitionD, a natural deduction calculusND(D) is associated. Not every such system will have the normalization property; specifically, there are definitionsD for whichND(D) permits non-normalizable deductions. A lambda calculus is formulated where the terms are used as objects realizing deductions inND(D), and is shown to have the Church-Rosser property. SinceND(D) permits non-normalizable deductions, there will be typed terms which are non-normalizable. It will, for example, be possible to obtain a typed fixed-point operator.     

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.     

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.     

Complexity of subclasses of the intuitionistic propositional calculus

We investigate the complexity of the decision problem for subclasses of the intuitionistic propositional calculus and present upper bounds for decision procedures locating these subclasses into lower complexity classes like co-NP or polynomial time.     

An efficient implicit data structure for relation testing and searching in partially ordered sets

In this paper, we introduce an implicit data structure which represents a forest-structured partial order to efficiently perform, with respect to time and space, the following operations: 1) testing the relation among two elements (checking whether the two elements are related) and 2) given an elementu, searching for its father. The first operation can be performed in constant time, while the second one requires polylog time (logarithmic in the case of bounded degree). The data structure represents the order relation by referring only to internal nodes of the forest, thus achieving in many cases a significant saving in space occupation. Finally, the algorithm is shown to be optimal in a restricted computation model by deriving a lower bound on the space complexity within such a model.Work partially performed in the framework of Esprit BRA project 3075 Algorithms and Complexity and of Italian MURST 40% project Algoritmi e Strutture di Calcolo and partially supported by the National Research Council (CNR) Project Sistemi Informatici e Calcolo Parallelo.     

Remarks on Martin-Löf's partial type theory

In this paper we discuss Martin-Löf's partial type theory, that is type theory with general recursion, and in particular the consequences of the presence of a fixed point operator. We model Martin-Löf's logical framework domain-theoretically in the category of conditional upper semi lattices and parametrizations thereof. An interpretation of a type of sets in the logical framework, which defines partial type theory with one universe, is finally described.During the preparation of this paper, the first author was supported by the Swedish Natural Science Research Council as a PhD-student in mathematical logic.     

A general performance analysis method for uniform memory architectures

The performance of a multiprocessor system greatly depends on the bandwidth of its memory architecture. In this paper, uniform memory architectures with various interconnection networks including crossbar, multiple-buses and generalized shuffle networks are studied. We propose a general method based on the Markov chain model by assuming that the blocked memory requests will be redistributed to the memory modules in the next memory cycle. This assumption results in an analysis with lower complexity where the number of states is linearly proportional to the number of processors. Moreover, it can provide excellent estimation on the system power and memory bandwidth for all three types of interconnection networks as compared with the simulation results in which the blocked memory requests are resubmitted to the same memory module. Comparisons also show that our method is more general and precise than most existing analysis methods. The method is further extended to estimate the performance of multiprocessor system with caches. The approximation results are also shown to be remarkably good.     

Optimal assignment of task modules with precedence for distributed processing by graph matching and state-space search

A graph matching approach to optimal assignment of task modules with varying lengths and precedence relationship in a distributed computing system is proposed. Inclusion of module precedence into the optimal solution is made possible by the use of topological module orderings. Two graphs are defined to represent the processor structure and the module precedence relationship, respectively. Assignment of the task modules to the system processors is transformed into a type of graph matching. The search of optimal graph matching corresponding to optimal task assignment is formulated as a state-space search problem which is then solved by theA* algorithm in artificial intelligence. Illustrative examples and experimental results are included to show the effectiveness of the proposed approach.     

On the eigenvalue distribution of a class of preconditioning methods

Summary A class of preconditioning methods depending on a relaxation parameter is presented for the solution of large linear systems of equationAx=b, whereA is a symmetric positive definite matrix. The methods are based on an incomplete factorization of the matrixA and include both pointwise and blockwise factorization. We study the dependence of the rate of convergence of the preconditioned conjugate gradient method on the distribution of eigenvalues ofC ^–1 A, whereC is the preconditioning matrix. We also show graphic representations of the eigenvalues and present numerical tests of the methods.     

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.     

A measure-theoretic proof of Turing incomparability

We prove that if S is an ω-model of weak weak König’s lemma and , is incomputable, then there exists , such that A and B are Turing incomparable. This extends a recent result of Ku?era and Slaman who proved that if S₀ is a Scott set (i.e. an ω-model of weak König’s lemma) and A∈S₀, A⊆ω, is incomputable, then there exists B∈S₀, B⊆ω, such that A and B are Turing incomparable.     

An axiomatic treatment ofSIMD assignment

The aims of this article are to provide (i) an abstract characterisation of SIMD computation and (ii) a simple proof theory for SIMD programs. A soundness result is stated and the consequences of the result are analysed. The use of the axiomatic theory is illustrated by a proof of a parallel implementation of Euclid's GCD algorithm.     

An application of proof mining to nonlinear iterations

In this paper we apply methods of proof mining to obtain a highly uniform effective rate of asymptotic regularity for the Ishikawa iteration associated with nonexpansive self-mappings of convex subsets of a class of uniformly convex geodesic spaces. Moreover, we show that these results are guaranteed by a combination of logical metatheorems for classical and semi-intuitionistic systems.     

An adaptation of a root finding method to searching ordered disk files revisited

In the present report, Interpolation search, Fast search and Pegasus method are compared with respect to their performance in searching ordered disk files for several key distributions. The aim is to study the effect of the page capacity on searching performance. Cost metric is the number of page accesses and not key comparisons. Numerical results are illustrated and a new approximate formula is derived giving an estimate of the number of page accesses for the case of the Interpolation algorithm under uniform distributions.     

An efficient method for calculating smoothing splines using orthogonal transformations

Summary A procedure for calculating the mean squared residual and the trace of the influence matrix associated with a polynomial smoothing spline of degree 2m–1 using an orthogonal factorization is presented. The procedure substantially overcomes the problem of ill-conditioning encountered by a recently developed method which employs a Cholesky factorization, but still requires only orderm ² n operations and ordermn storage.     

An analysis of Ralston's quadrature

Summary Ralston's quadrature achieves higher accuracy in composite rules than analogous Newton-Cotes or Gaussian formulas. His rules are analyzed, computable expressions for the weights and knots are given, and a more suitable form of the remainder is derived.     

An optimal algorithm for generating equivalence relations on a linear array of processors

We describe a cost-optimal parallel algorithm for enumerating all partitions (equivalence relations) of the set {1, ...,n}, in lexicographic order. The algorithm is designed to be executed on a linear array of processors. It usesn processors, each having constant size memory and each being responsible for producing one element of a given set partition. Set partitions are generated with constant delay leading to anO(B _n) time solution, whereB _n is the total number of set partitions. The same method can be generalized to enumerate some other combinatorial objects such as variations. The algorithm can be made adaptive, i.e. to run on any prespecified number of processors. To illustrate the model of parallel computation, a simple case of enumerating subsets of the set {1, ...,n}, having at mostm (n) elements is also described.The research is partialy supported by NSERC operating grant OGPIN 007.     

A fast ‘Monte-Carlo cross-validation’ procedure for large least squares problems with noisy data

Summary We propose a fast Monte-Carlo algorithm for calculating reliable estimates of the trace of the influence matrixA involved in regularization of linear equations or data smoothing problems, where is the regularization or smoothing parameter. This general algorithm is simply as follows: i) generaten pseudo-random valuesw ₁, ...,w _n , from the standard normal distribution (wheren is the number of data points) and letw=(w ₁, ...,w _n ) ^T , ii) compute the residual vectorw–A w, iii) take the normalized inner-product (w ^T (w–A w))/(w ^T w) as an approximation to (1/n)tr(I–A ). We show, both by theoretical bounds and by numerical simulations on some typical problems, that the expected relative precision of these estimates is very good whenn is large enough, and that they can be used in practice for the minimization with respect to of the well known Generalized Cross-Validation (GCV) function. This permits the use of the GCV method for choosing in any particular large-scale application, with only a similar amount of work as the standard residual method. Numerical applications of this procedure to optimal spline smoothing in one or two dimensions show its efficiency.     

Signature files: An integrated access method for text and attributes,suitable for optical disk storage

We design and analyze integrated ways of applying the signature file approach for text and attributes simultaneously. In traditional signature file methods, the records are stored sequentially in the main file; for every record, a hash-coded abstraction of it (record signature) is created and stored in the signature file (usually, sequentially). To resolve a query, the signature file is scanned; the signatures retrieved correspond to all the qualifying records, plus some false drops.Here, we extend some signature file methods, namely superimposed coding and disjoint coding, to handle text and attributes. We develop a mathematical model and derive formulas for the optimal choice of parameters. The proposed methods achieve significant performance improvements, because they can take advantage of the skewed distribution of the queries. Depending on the query frequencies, the false drop probability can be reduced 40–45 times ( 97% savings), for the same overhead.Also with the University of Maryland Institute for Advanced Computer Studies (U.M.I.A.C.S.). This research was sponsored partially by the National Science Foundation under the grant DCR-86-16833.