International Journal of Foundations of Computer Science

Realizability of monotone inductive definitions is studied to construct a logical system in which recursive data structures and recursive control structures of programs are naturally formalized by using inductive definitions and programs can be produced from constructive proofs by using realizability. Two q-realizability interpretations of monotone inductive definitions are presented. One interpretation is defined so that a realizer of an inductively defined predicate is the same as a realizer of its expansion. It is proved that the interpretation of restricted monotone inductive definitions is sound and that the interpretation of full monotone inductive definitions is not sound, though the interpretation seems very natural. Another interpretation is presented by using the higher order coding and q-realizability for the second order logic. The soundness of this interpretation of full monotone inductive definitions is also proved. To prove this result, greatest-lower-bound inductive definitions are introduced.

This paper analyses how the symmetry of a processor network influences the existence of a solution for the network orientation problem. The orientation of hypercubes and tori is the problem of assigning labels to each link of each processor, in such a way that a sense of direction is given to the network. In this paper the problem of network orientation for these two topologies is studied under the assumption that the network contains a single leader, under the assumption that the processors possess unique identities, and under the assumption that the network is anonymous. The distinction between these three models is considered fundamental in distributed computing.

It is shown that orientations can be computed by deterministic algorithms only when either a leader or unique identities are available. Orientations can be computed for anonymous networks by randomized algorithms, but only when the number of processors is known. When the number of processors is not known, even randomized algorithms cannot compute orientations for anonymous processor networks.

Lower bounds on the message complexity of orientation and algorithms achieving these bounds are given.

It is shown, that for each constant k≥1, the following problems can be solved in time: given a graph G, determine whether G has k vertex disjoint cycles, determine whether G has k edge disjoint cycles, determine whether G has a feedback vertex set of size ≤k. Also, every class , that is closed under minor taking, taking, and that does not contain the graph consisting of k disjoint copies of K₃, has an membership test algorithm.

We consider various TAG-like devices that generate one-way infinite words in real time. The simplest types of these devices are equivalent to iterative morphisms (also called substitutions), automatic sequences and iterative DGSM’s. We consider also a few new types. Mainly we study the comparative power of these mechanisms and develop some techniques for proving that certain devices cannot produce a particular infinite word.

We consider heap-ordered trees in this paper. The main theorems in this paper show that the average and the variance of the altitude (or level) of the nodes in a random n-node heap-ordered tree are and , respectively where γ=0.5772156649… is the Euler’s constant.