Handbook of Formal Languages

The theory of tree automata and tree languages emerged in the middle of the 1960s quite naturally from the view of finite automata as unary algebras advocated by J. R. Büchi and J. B. Wright. From this perspective the generalization from strings to trees means simply that any finite algebra of finite type can be regarded as an automaton which as inputs accepts terms over the ranked alphabet formed by the operation symbols of the algebra, and these terms again can be seen as (formal representations of) labeled trees with a left-to-right ordering of the branches. Strings over a finite alphabet can then be regarded as terms over a unary ranked alphabet, and hence finite automata become special tree automata and string languages unary tree languages. The theory of tree automata and tree languages can thus be seen as an outgrowth of Büchi’s and Wright’s program which had as its goal a general theory that would encompass automata, universal algebra, equational logic, and formal languages. Some interesting vistas of this program and its development are opened by Büchi’s posthumous book [Büc89] in which many of the ideas are traced back to people like Thue, Skolem, Post, and even Leibniz.

In this paper, we will describe a tree generating system called tree-adjoining grammar (TAG) and state some of the recent results about TAGs. The work on TAGs is motivated by linguistic considerations. However, a number of formal results have been established for TAGs, which we believe, would be of interest to researchers in formal languages and automata, including those interested in tree grammars and tree automata.

Graph languages are sets of labeled graphs. They can be generated by graph grammars, and in particular by context-free graph grammars. There are several types of context-free graph grammars, depending, e.g., on whether (hyper)edges or nodes are rewritten by graphs. Basic properties of the main types of context-free graph grammars are discussed. Other, equivalent, ways of defining context-free graph languages are: generating graph expressions by regular tree grammars, and translating trees into graphs by formulas of monadic second-order logic. Context-free graph grammars can be used to generate string languages and tree languages.

The aim of this chapter is to generalize concepts and techniques of formal language theory to two dimensions. Informally, a two-dimensional string is called a picture and is defined as a rectangular array of symbols taken from a finite alphabet. A two-dimensional language (or picture language) is a set of pictures.

Terms and trees are important structured objects that can be found almost everywhere in Computer Science, not only in connection with their mathematical foundations. In any axiomatic definition of structures and equationally defined calculi one will find the combination of axioms, i.e., equations, and a method of deriving new theorems from those by using deduction rules. This situation traditionally can be found in logic and became important in applications such as symbolic algebraic computation, program specification and verification using abstract data types, and automated theorem proving. Term rewriting can be seen as a generalization of string rewriting as studied early in this century by Axel Thue. Terms are structured strings that can well be visualized by rooted, node-labelled, and ordered trees. This was already recognized by Axel Thue in 1910, [Thue10]. In his paper he investigated the formulation of new concepts from already given ones and designed a theory of terms or trees and how to create and use them. He posed what we now call the word problem for equational theories and thereby introduced the idea of a universal algebra and the free algebra over sets of equations. The theorems deduced syntactically from a set of axioms within a calculus are useful only in the context of a semantic interpretation in an algebraic structure that models the theory specified by the axioms and the deduction rules. The semantic equality means that a theorem a = b is true in each model of a given theory whereas syntactic equality a = _E b is its deducibility (provability) from the axioms E. From Birkhoff 1935, [Birk35], we know that semantic and syntactic equality coincides and thus the deduction rules specified in the calculus could in general be used for deciding semantic equality.

The purpose of this chapter is to give an introduction into languages of infinite strings (of order type ω), so-called ω-languages. The set of all infinite strings over a finite alphabet may be considered, as we shall see below, in a natural way as a metric space.

The subject of this chapter is the study of formal languages (mostly languages recognizable by finite automata) in the framework of mathematical logic.

Parallelism and concurrency are fundamental concepts in computer science. Specification and verification of concurrent programs are of first importance. It concerns our daily life whether software written for distributed systems behaves correctly.

In these notes we survey applications of L-systems to the modeling of plants, with an emphasis on the results obtained since the comprehensive presentation of this area in The Algorithmic Beauty of Plants [99]. The new developments include:

We discuss the application of (weighted) finite automata to image specification and image-data compression and applications of (weighted) finite transducers to image manipulation.