Coinduction for Exact Real Number Computation

This paper studies coinductive representations of real numbers by signed digit streams and fast Cauchy sequences. It is shown how the associated coinductive principle can be used to give straightforward and easily implementable proofs of the equivalence of the two representations as well as the correctness of various corecursive exact real number algorithms. The basic framework is the classical theory of coinductive sets as greatest fixed points of monotone operators and hence is different from (though related to) the type theoretic approach by Ciaffaglione and Gianantonio.     

Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts

Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non-well-founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called a bisimulation). We present an automation of coinductive theorem proving. This automation is based on the idea of proof planning [7]. Proof planning constructs the higher level steps in a proof, using knowledge of the general structure of a family of proofs and exploiting this knowledge to control the proof search. Part of proof planning involves the use of failure information to modify the plan by the use of a proof critic [23] which exploits the information gained from the failed proof attempt. Our approach to the problem was to develop a strategy that makes an initial simple guess at a bisimulation and then uses generalisation techniques, motivated by a critic, to refine this guess, so that a larger class of coinductive problems can be automatically verified. The implementation of this strategy has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell [22]. We have developed a proof plan for coinduction and a critic associated with this proof plan. These have been implemented in CoCLAM, an extended version of CLAM [9], with encouraging results. The planner has been successfully tested on a number of theorems. This revised version was published online in June 2006 with corrections to the Cover Date.     

A certified,corecursive implementation of exact real numbers

We implement exact real numbers in the logical framework Coq using streams, i.e., infinite sequences, of digits, and characterize constructive real numbers through a minimal axiomatization. We prove that our construction inhabits the axiomatization, working formally with coinductive types and corecursive proofs. Thus we obtain reliable, corecursive algorithms for computing on real numbers.     

Productivity of Edalat-Potts Exact Arithmetic in Constructive Type Theory

In this work we focus on a formalisation of the algorithms of lazy exact arithmetic a la Edalat-Potts in type theory. We choose the constructive type theory extended with coinductive types as our formal verification tool. We show examples of how infinite objects such as streams and expression trees can be formalised as coinductive types. We study the type theoretic notion of productivity which ensures the infiniteness of the outcome of the algorithms on infinite objects. Syntactical methods are not always strong enough to ensure the productivity. However, if some information about the complexity of a function is provided, one may be able to show the productivity of that function. In the case of the normalisation algorithm we show that such information can be obtained from the choice of real number representation that is used to represent the input and the output. Furthermore, we show how to employ this semantic information to formalise a restricted case of normalisation algorithm in our type theory.     

Complete sets of cooperations

The structure map turning a set into the carrier of a final coalgebra is not unique. This fact is well known, but commonly elided. In this paper, we argue that any such concrete representation of a set as a final coalgebra is potentially interesting on its own. We discuss several examples, in particular, we consider different coalgebra structures that turn the set of infinite streams into the carrier of a final coalgebra. After that we focus on coalgebra structures that are made up using so-called cooperations. We say that a collection of cooperations is complete for a given set X if it gives rise to a coalgebra structure that turns X into the carrier set of a subcoalgebra of a final coalgebra. Any complete set of cooperations yields a coalgebraic proof and definition principle. We exploit this fact and devise a general definition scheme for constants and functions on a set X that is parametrical in the choice of the complete set of cooperations for X.     

I/O scheduling for digital continuous media

A growing set of applications require access to digital video and audio. In order to provide playback of such continuous media (CM), scheduling strategies for CM data servers (CMS) are necessary. In some domains, particularly defense and industrial process control, the timing requirements of these applications are strict and essential to their correct operation. In this paper we develop a scheduling strategy for multiple access to a CMS such that the timing guarantees are maintained at all times. First, we develop a scheduling strategy for the steady state, i.e., when there are no changes in playback rate or operation. We derive an optimal Batched SCAN (BSCAN) algorithm that requires minimum buffer space to schedule concurrent accesses. The scheduling strategy incorporates two key constraints: (1) data fetches from the storage system are assumed to be in integral multiples of the block size, and (2) playback guarantees are ensured for frame-oriented streams when each frame can span multiple blocks. We discuss modifications to the scheduling strategy to handle compressed data like motion-JPEG and MPEG. Second, we develop techniques to handle dynamic changes brought about by VCR-like operations executed by applications. We define a suite of primitive VCR-like operations that can be executed. We show that an unregulated change in the BSCAN schedule, in response to VCR-like operations, will affect playback guarantees. We develop two general techniques to ensure playback guarantees while responding to VCR-like operations: passive and active accumulation. Using user response time as a metric we show that active accumulation algorithms outperform passive accumulation algorithms. An optimal response-time algorithm in a class of active accumulation strategies is derived. The results presented here are validated by extensive simulation studies.     

Fast computation of the Smith form of a sparse integer matrix

We present a new probabilistic algorithm to compute the Smith normal form of a sparse integer matrix . The algorithm treats A as a “black box”—A is only used to compute matrix-vector products and we do not access individual entries in A directly. The algorithm requires about black box evaluations for word-sized primes p and , plus additional bit operations. For sparse matrices this represents a substantial improvement over previously known algorithms. The new algorithm suffers from no “fill-in” or intermediate value explosion, and uses very little additional space. We also present an asymptotically fast algorithm for dense matrices which requires about bit operations, where O(MM(m)) operations are sufficient to multiply two matrices over a field. Both algorithms are probabilistic of the Monte Carlo type — on any input they return the correct answer with a controllable, exponentially small probability of error. Received: March 9, 2000.     

Efficient Modular Squaring Algorithms for Hardware Implementation in GF(p)

ABSTRACT

Some of the most popular public key encryption algorithms use exponentiation as their core operation, which can be mostly broken into several modular squaring operations. In this paper, we present GF(p) modular squaring algorithms and efficiently implement them on hardware. We present different algorithms, two for squaring and one for reduction combined with the squaring, to provide a general modular squaring algorithm. The algorithms are implemented through datapaths that uses redundant Carry-Save Adders, making the computation time independent form the operands precision. The proposed algorithms are compared with each other as well as with the existing modular squaring algorithms. The experimental results are obtained by synthesizing the hardware designs for FPGA Virtex5 chip (xc5vlx50 – ff1153 technology), which showed interesting results and made our ideas very attractive.     

Efficient and Scalable Routing Algorithms for Collective Communication Operations on 2D All-Port Torus Networks

Collective Communication Algorithms for 2D torus networks have been investigated quite extensively in the literature and two broad approaches, namely direct methods and indirect (message combining) methods are recognized in the field. While direct methods minimize the volume of data, the indirect methods reduce the number of message start-ups. Consequently, either a suite of algorithms must be employed for efficiency over a wide range of message lengths and communication operations or algorithms should be able to adapt themselves to the current case, possibly by switching between direct and indirect routing modes as appropriate. In this paper, we propose adaptive routing algorithms for all-port, wormhole routed, synchronous, 2D torus networks optimized for one-to-all broadcast,  gossiping and complete exchange collective communication operations. The proposed algorithms employ completely-connected subnetworks where complete exchange amongst the nodes in the subnetwork can be accomplished in one step only. Combined with suitable 2D plane tiling techniques, the proposed algorithms share the same set of primitive operations and yield superior performance compared to previously proposed methods, either pure or hybridized.     

A survey on algorithms for mining frequent itemsets over data streams

The increasing prominence of data streams arising in a wide range of advanced applications such as fraud detection and trend learning has led to the study of online mining of frequent itemsets (FIs). Unlike mining static databases, mining data streams poses many new challenges. In addition to the one-scan nature, the unbounded memory requirement and the high data arrival rate of data streams, the combinatorial explosion of itemsets exacerbates the mining task. The high complexity of the FI mining problem hinders the application of the stream mining techniques. We recognize that a critical review of existing techniques is needed in order to design and develop efficient mining algorithms and data structures that are able to match the processing rate of the mining with the high arrival rate of data streams. Within a unifying set of notations and terminologies, we describe in this paper the efforts and main techniques for mining data streams and present a comprehensive survey of a number of the state-of-the-art algorithms on mining frequent itemsets over data streams. We classify the stream-mining techniques into two categories based on the window model that they adopt in order to provide insights into how and why the techniques are useful. Then, we further analyze the algorithms according to whether they are exact or approximate and, for approximate approaches, whether they are false-positive or false-negative. We also discuss various interesting issues, including the merits and limitations in existing research and substantive areas for future research.