International Journal of Foundations of Computer Science

This brief survey will discuss the early years of the theory of formal languages through about 1970, treating only the most fundamental of the concepts. The paper will conclude with a brief discussion of a small number of topics, the choice reflecting only the personal interest of the author.

Term graphs are a natural generalization of terms in which structure sharing is allowed. Structure sharing makes term graph rewriting a time- and space-efficient method for implementing term rewrite systems. Certain structure sharing schemes can lead to a situation in which a term graph component is rewritten to another component that contains the original. This phenomenon, called redex capturing, introduces cycles into the term graph which is being rewritten—even when the graph and the rule themselves do not contain cycles. In some applications, redex capturing is undesirable, such as in contexts where garbage collectors require that graphs be acyclic. In other applications, for example in the use of the fixed-point combinator Y, redex capturing acts as a rewriting optimization. We show, using results about infinite rewritings of trees, that term graph rewriting with arbitrary structure sharing (including redex capturing) is sound for left-linear term rewrite systems.

We show how to solve boolean combinations of inequations s>t in the Herbrand Universe, assuming that ≥ is interpreted as a lexicographic path ordering extending a total precedence. In other words, we prove that the existential fragment of the theory of a lexicographic path ordering which extends a total precedence is decidable.

In the theory of denotational semantics of programming languages, several authors proved the existence of particular kinds of universal domains. D. Scott constructed universal information systems, which are, however, not unique up to isomorphism. Here, we use a model-theoretic technique to establish the existence and uniqueness of a universal homogeneous information system. Similar results are also obtained for canonical and for stable information systems, respectively.

Different methods for compressing trees are surveyed and developed. Tree compression can be seen as a trade-off problem between time and space in which we can choose different strategies depending on whether we prefer better compression results or more efficient operations in the compressed structure. Of special interest is the case where space can be saved while preserving the functionality of the operations; this is called data optimization. The general compression scheme employed here consists of separate linearization of the tree structure and the data stored in the tree. Also some applications of the tree compression methods are explored. These include the syntax-directed compression of program files, the compression of pixel trees, trie compaction and dictionaries maintained as implicit data structures.

In this paper we present a strategy to maintain a dynamic optimal binary search tree. The algorithms for insertion and deletion use swapping as the basic operation. Since in average situations the tree reorganization is limited to local changes, it can be favourably compared with the local balancing algorithms. The present algorithms dynamically maintain the optimal tree with an amortized time of O(log₂ n), where n is the total number of nodes in the tree. In the worst case situations, the algorithms take only O(n) time. This is significant when they are compared to the algorithms producing static optimal binary search trees.