A Tutorial on Specifying Data Structures in Maude

This tutorial describes the equational specification of a series of typical data structures in Maude. We start with the well-known stacks, queues, and lists, to continue with binary and search trees. Not only are the simple versions considered but also advanced ones such as AVL and 2-3-4 trees. The operator attributes available in Maude allow the specification of data based on constructors that satisfy some equational properties, like concatenation of lists which is associative and has the empty list as identity, as opposed to the free constructors available in other functional programming languages. Moreover, the expressive version of equational logic in which Maude is based, namely membership equational logic, allows the faithful specification of types whose data are defined not only by means of constructors, but also by the satisfaction of additional properties, like sorted lists or search trees. In the second part of the paper we describe the use of an inductive theorem prover, the ITP, which itself is developed and integrated in Maude by means of the powerful metalevel and metalanguage features offered by the latter, to prove properties of the data structures. This is work in progress because the ITP is still under development and, as soon as the data gets a bit complex, the proof of their properties gets even more complex.     

Optimal Mappings of q-ary and Binomial Trees into Parallel Memory Modules for Fast and Conflict-Free Access to Path and Subtree Templates

The main memory access latency can significantly slow down the overall performance of a computer system due to the fact that average cycle time of the main memory is typically a factor of 5–10 times higher than that of a processor. To cope with this problem, in addition to the use of caches, the main memory of a multiprocessor architecture is usually organized into multiple modules or banks. Although such organization enhances memory bandwidth, the amount of data that the multiprocessor can retrieve in the same memory cycle, conflicts due to simultaneous attempts to access the same memory module may reduce the effective bandwidth. Therefore, efficient mapping schemes are required to distribute data in such a way that regular patterns, called templates, of various structures can be retrieved in parallel without memory conflicts. Prior work on data mappings mostly dealt with conflict-free access to templates such as rows, columns, or diagonals of (multidimensional) arrays, and only limited attention has been paid to access templates of nonnumeric structures such as trees. In this paper, we study optimal and balanced mappings for accessing path and subtree templates of trees, where a mapping will be called optimal if it allows conflict-free access to templates with as few memory banks as possible. An optimal mapping will also be called balanced if it distributes as evenly as possible the nodes of the entire tree among the memory banks available. In particular, based on Latinsquares, we propose an optimal and balanced mapping for leaf-to-root paths of q-ary trees. Another (recursive) mapping for leaf-to-root paths of binary trees raises interesting combinatorial problems. We also derive an optimal and balanced mapping to access complete t-ary subtrees of complete q-ary trees, where 2⩽t⩽q, and an optimal mapping for subtrees of binomial trees.     

Computing on a free tree via complexity-preserving mappings

The relationship between linear lists and free trees is studied. We examine a number of well-known data structures for computing functions on linear lists and show that they can be canonically transformed into data structures for computing the same functions defined over free trees. This is used to establish new upper bounds on the complexity of several query-answering problems.     

A framework to capture dynamic data structures in pointer-based codes

To successfully exploit all the possibilities of current computer/multicomputer architectures, optimization compiling techniques are a must. However, for codes based on pointers and dynamic data structures, these optimization techniques have to be necessarily carried out after identifying the characteristics and properties of the data structure used in the code. We describe the framework and the analyzer we have implemented to capture complex data structures generated, traversed, and modified in codes based on pointers. Our method assigns a reduced set of reference shape graph (RSRSG) to each statement to approximate the shape of the data structure after the execution of such a statement. With the properties and operations that define the behavior of our RSRSG, the method can accurately detect complex recursive data structures such as a doubly linked list of pointers to trees where the leaves point to additional lists. Several experiments are carried out with real codes to validate the capabilities of our analyzer.     

Set theory for verification. II: Induction and recursion

A theory of recursive definitions has been mechanized in Isabelle's Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs, and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski theorem over a suitable set.Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion.Recursive data structures are expressed by applying the Knaster-Tarski theorem to a set, such asV , that is closed under Cartesian product and disjoint sum.Worked examples include the transitive closure of a relation, lists, variable-branching trees, and mutually recursive trees and forests. The Schröder-Bernstein theorem and the soundness of propositional logic are proved in Isabelle sessions.     

Efficiency of hybrid index structures—Theoretical analysis and a practical application

Hybrid index structures support access to heterogeneous data types in multiple columns. Several experiments confirm the improved efficiency of these hybrid access structures. Yet, very little is known about the worst case time and space complexity of them. This paper aims to close this gap by introducing a theoretical framework supporting the analysis of hybrid index structures. This framework then is used to derive the constraints for an access structure which is both time and space efficient. An access structure based on a B+-Tree augmented with bit lists representing sets of terms from texts is the outcome of the analysis which is then validated experimentally together with a hybrid R-Tree variant to show a logarithmic search time complexity.     

Verification of complex dynamic data tree with mu-calculus

The problem of verifying software systems that use dynamic data structures (such as linked lists, queues, or binary trees) has attracted increasing interest over the last decade. Dynamic structures are not easily supported by verification techniques because, among other reasons, it is difficult to efficiently manage the pointer-based internal representation. This is a key aspect when, for instance, the goal is to construct a verification tool based on model checking techniques. In addition, since new nodes can be dynamically inserted or extracted from the structure, the shape of the dynamic data (and other more specific properties) may vary at runtime, with errors such as the non desirable sharing between two nodes being difficult to detect. In this paper, we propose to use mu-calculus to describe and analyze with model checking techniques dynamic data structures such as lists and trees. The expressiveness of mu-calculus makes it possible to naturally describe these structures. In addition, following the ideas of separation logic, the logic has been extended with a new operator capable of describing the non-sharing property, which is essential when analyzing dynamic data structures.     

Supervised neural networks for the classification of structures

Standard neural networks and statistical methods are usually believed to be inadequate when dealing with complex structures because of their feature-based approach. In fact, feature-based approaches usually fail to give satisfactory solutions because of the sensitivity of the approach to the a priori selection of the features, and the incapacity to represent any specific information on the relationships among the components of the structures. However, we show that neural networks can, in fact, represent and classify structured patterns. The key idea underpinning our approach is the use of the so called "generalized recursive neuron", which is essentially a generalization to structures of a recurrent neuron. By using generalized recursive neurons, all the supervised networks developed for the classification of sequences, such as backpropagation through time networks, real-time recurrent networks, simple recurrent networks, recurrent cascade correlation networks, and neural trees can, on the whole, be generalized to structures. The results obtained by some of the above networks (with generalized recursive neurons) on the classification of logic terms are presented.     

Stochastic rearrangement rules for self-organizing data structures

We consider self-organizing data structures when the number of data accesses is unknown. We show that certain general rearrangement rules can be modified to reduce significantly the number of data moves, without affecting the asymptotic cost of a data access. As a special case, explicit formulae are given for the expected cost of a data access and the expected number of data moves for the modified move-to-front rules for linear lists and binary trees. Since a data move usually costs at least as much as a data access, the modified rule eventually leads to a savings in total cost (the sum of data accesses and moves).     

Random access in a list environment

A memory allocation scheme for list structures (ral system) is proposed, which allows random access and search for the elements of the structure. A comparative study of classical list systems and ral systems is given, for the basic operations of search, insertion, deletion and sorting of the structure elements. It is shown that, in general, ral systems exhibit lower order expected time complexities for such operations, possibly at the expense of a reasonable increase in memory occupation. Allocation and processing of linear ordered lists and trees are discussed in particular.     

Multilevel model and structure of representation of ultra-large amounts of graphic information and images

The model and structure of representation of data are considered for the processing and compact storage of ultra-large amounts of various types of information in the form of binary difference trees of essential readings, which provide efficient access to arbitrary fragments of the tree and the solution of various thematic problems using general-to-specific and other methods. The new method, which is the result of development of approaches to the models and structures of data representation on the basis of binary trees of essential readings, ensures better flexibility and helps to overcome many of the difficulties that arise in the processing of ultra-large amounts of data.     

Parallel Data Mining for Association Rules on Shared-Memory Systems

In this paper we present a new parallel algorithm for data mining of association rules on shared-memory multiprocessors. We study the degree of parallelism, synchronization, and data locality issues, and present optimizations for fast frequency computation. Experiments show that a significant improvement of performance is achieved using our proposed optimizations. We also achieved good speed-up for the parallel algorithm. A lot of data-mining tasks (e.g. association rules, sequential patterns) use complex pointer-based data structures (e.g. hash trees) that typically suffer from suboptimal data locality. In the multiprocessor case shared access to these data structures may also result in false sharing. For these tasks it is commonly observed that the recursive data structure is built once and accessed multiple times during each iteration. Furthermore, the access patterns after the build phase are highly ordered. In such cases locality and false sharing sensitive memory placement of these structures can enhance performance significantly. We evaluate a set of placement policies for parallel association discovery, and show that simple placement schemes can improve execution time by more than a factor of two. More complex schemes yield additional gains. Received 24 May 1999 / Revised 20 June 2000 / Accepted in revised form 6 July 2000     

Stochastic rearrangement rules for self-organizing data structures

We consider self-organizing data structures when the number of data accesses is unknown. We show that certain general rearrangement rules can be modified to reduce significantly the number of data moves, without affecting the asymptotic cost of a data access. As a special case, explicit formulae are given for the expected cost of a data access and the expected number of data moves for the modified move-to-front rules for linear lists and binary trees. Since a data move usually costs at least as much as a data access, the modified rule eventually leads to a savings in total cost (the sum of data accesses and moves).This research was supported in part by the National Science Foundation, Grant Number MCS 81-17364     

RTR-trees for space robotics behavior simulation and visualization

New types of trees of structures and linked lists with variable order relations (RTR-trees and RTR-lists) are discussed. Using them enables application of the direct kinematic scheme for simulation of 3D-objects with reorderable structure, making behavior simulation more natural.     

Computing on a free tree via complexity-preserving mappings

The relationship between linear lists and free trees is studied. We examine a number of well-known data structures for computing functions on linear lists and show that they can be canonically transformed into data structures for computing the same functions defined over free trees. This is used to establish new upper bounds on the complexity of several query-answering problems.This work was started when the author was at Brown University, Providence, RI. It was partly supported by NSF Grant MCS 83-03925. A preliminary version of this work has appeared in theProceedings of the 25th Annual IEEE Symposium on Foundations of Computer Science, West Palm Beach, FL, October 1984, pp. 358–368.     

递归程序结构研究

对递归程序的结构进行了较为深入的研究 ,提出了递归树的概念 ,给出了递归程序的一般结构 ,把递归分为简单链结构、树状结构、复杂链结构三种情况 ,据此 ,给出了复杂的递归问题的程序设计方法 ,根据此方法 ,可方便地写出较为复杂的递归问题的递归程序 ,从而提高设计递归程序的效率。     

Efficient parallel algorithms for graph problems

We present an efficient technique for parallel manipulation of data structures that avoids memory access conflicts. That is, this technique works on the Exclusive Read/Exclusive Write (EREW) model of computation, which is the weakest shared memory, MIMD machine model. It is used in a new parallel radix sort algorithm that is optimal for keys whose values are over a small range. Using the radix sort and known results for parallel prefix on linked lists, we develop parallel algorithms that efficiently solve various computations on trees and “unicycular graphs.” Finally, we develop parallel algorithms for connected components, spanning trees, minimum spanning trees, and other graph problems. All of the graph algorithms achieve linear speedup for all but the sparsest graphs.     

Generalized binary split trees

Summary The definition of binary split trees is generalized by removing the condition of decreasing frequency. It is shown that the access time of generalized split trees is less than that of split trees in general. The optimal representation of generalized split trees is studied. A polynomial time algorithm to construct such optimal tree structures is given. The relationship among several classes of binary trees are also discussed.The research of the first author was partially supported by a Research Initiation Grant from the University of Houston     

Circular programs and self-referential structures

A circular program creates a data structure whose computation depends upon itself or refers to itself. The technique is used to implement the classic data structures circular and doubly-linked lists, threaded trees and queues, in a functional programming language. These structures are normally thought to require updateable variables found in imperative languages. For example, a functional program to perform the breadth-first traversal of a tree is given. Some of the examples result in circular data structures when evaluated. Some examples are particularly space-efficient by avoiding the creation of intermediate temporary structures which would otherwise later become garbage. Lastly, the technique can be applied in an imperative language to give an elegant program.