International Journal of Foundations of Computer Science

Please refer to full tex.

Recently some attention has been paid to the properties enjoyed by combinations of term rewriting and λ-calculus based systems. In this paper strong normalization and confluence are proved for λ-terms obtained by merging pure λ-terms and first order canonical term rewriting systems, in the framework of a system which extends the Coppo-Dezani intersection type assignment system. On terms of the resulting calculus we can perform ordinary β and η reductions, as well as the reductions induced in a natural way by the term rewriting systems. In some parts of our analysis we follow rather closely the development contained in a recent paper by Val Breazu-Tannen and Jean Gallier. There, the same properties of strong normalization and confluence are proved for systems obtained by combining the second order polymorphic λ-calculus with first order canonical term rewriting systems. The strong normalization result of Breazu-Tannen and Gallier is proved to be implied by the corresponding property of our system.

One of the main issues in flow control problems is deadlock of messages caused by a limited amount of resources. In this paper, the problem of predicting whether a deadlock will necessarily occur in a Store-and-Forward Network is analyzed. We show that, in the case of dynamic routing, the deadlock prediction problem can be decided in polynomial time if tokens are allowed to transit more than once through the same vertex, in contrast with an NP-completeness result in the case where they are allowed to transit at most once.

Recently, boolean hierarchies over NP and over RP (denoted BH and RBH respectively) have been introduced in complexity theory. They have proved particularly useful in carefully classifying natural problems which are not finely classified using more standard time and space complexity classes. In this paper we are particularly interested in the structural properties of these hierarchies and in relationships among various boolean hierarchies.

Establishing the most significant relationships between BH, RBH, and other complexity classes would imply solving some of the major open problems in complexity theory. To date the only significant relations known are: , and RBH⊆BH. Essentially nothing is known about the fine structure of BH or of RBH.

In [5] an oracle X is constructed for which both BH^x and RBH^x have an infinite number of proper levels. Further each level of RBH is properly contained in the corresponding level of BH, and RBH is properly contained in PP. In this paper we further explore these constructions. We prove that some of these separations are “strong” separations. That is, they can be witnessed by sets that cannot be “approximated” by sets in the smaller class: the separating sets are immune to sets from the smaller class.

Specifically, we prove that the separations between RBH, BPP, PP and each level of BH, can be witnessed by immune sets.

We introduce BD (Breadth-Depth) grammars which extend context-free grammars by allowing breadth-first derivations. Their languages are recognized by Deque (double ended queue) automata having a single state. BD languages also include languages recognized by monostatic queue automata.

It is shown that the commutative image of BD languages is semilinear, that they have a periodicity (pumping) property, and can be homomorphically characterized as h(DAD∩R), where DAD is the Dyck-AntiDyck language, and R a regular set.

Non-autoinclusive BD grammars coincide in power with breadth-first grammars with regular right parts.

This paper presents the declarative and procedural semantics of Reflective Prolog, a new logic language able to represent metaknowledge and use it in the proof process via an extended resolution procedure including forms of implicit reflection. The declarative semantics of a Reflective Prolog definite program is provided in terms of the Least Reflective Herbrand Model of the program, characterized by means of a suitable mapping. The extended resolution is then shown to be sound and complete with respect to the Least Reflective Herband Model.

This paper defines a new concurrent logic language, Nested Guarded Horn Clauses (NGHC). The main new feature of the language is its concept of guard. In fact, an NGHC clause has several layers of (standard) guards. This syntactic innovation allows the definition of a complete (i.e. always applicable) set of unfolding rules and therefore of an unfolding semantics which is equivalent, with respect to the success set, to the operational semantics. A fixpoint semantics is also defined in the classic logic programming style and is proved equivalent to the unfolding one. Since it is possible to embed Flat GHC into NGHC, our method can be used to give a fixpoint semantics to FGHC as well.

We study the limit distribution of the sequence of random variables where, for each n, is the number of prefixes of a trace of length n chosen in a given free partially commutative monoid under the assumption that all representative strings of length n are equiprobable. We determine such a limit distribution for every free partially commutative monoid defined on a concurrent alphabet <Σ,C> such that the complementary relation C^c is transitive. We prove that if the complementary alphabet <Σ,C^c> has k connected components of equal size, then (suitably normalized) converges in distribution to a chi-square with k-1 degrees of freedom. On the other hand, if at least two connected components of <Σ,C^c> have a different number of vertices, then converges in distribution to a normal random variable. These probabilistic results yield the limit distribution of the time complexity of several algorithms for problems on trace languages, including algorithms for the Membership Problem of regular and context-free trace languages.

The problem of relating system descriptions at different levels of abstraction is addressed in the context of process description languages. As a case study, we introduce two nondeterministic languages. The latter is a simple extension of the former and is obtained by adding to its signature an operator of strong prefixing for making atomic the execution of a sequence of actions. The two languages are intended to be a specification and an implementation language, respectively. To directly relate them, we introduce a mapping, called atomic action refinement, from actions of the former to atomic sequences (i.e. sequences of actions built with strong prefixing) of the latter, which can be homomorphically extended to become a mapping among process terms of the two languages. A notion of implementation, based on a sort of bisimulation (parametric with respect to an atomic action refinement), relates processes of the two languages. Given a specification process P and an atomic action refinement ρ, the refined process ρ(P) is proved to be an implementation of P. Moreover, two complete proof systems for the two languages (and thus also for the operator of strong prefixing) are presented and proved consistent with respect to refinement: if P and Q are congruent processes of the specification language, then ρ(P) and ρ(Q) are congruent, too.

To capture the informal concept of linear time computability, we propose and discuss the class TIME(n¹⁺), consisting of all functions which are computable by a Successor RAM with exponent at most one; the exponent of a function is the infimum of all rational numbers r such that the function is computable in time O(n^r). This class properly contains the class NLT (“Nearly Linear Time”)—proposed by Gurevich and Shelah—which contains all functions computable by a Successor RAM in time O(n(log n)^k) for some k∈N. Both classes are very robust under changes of the underlying machine model: using the same time bounds they can be defined by Random Access Computers, Storage Modification Machines, Kolmogorov algorithms, Random Access Turing machines etc.; this distinguishes them from similar classes defined by ordinary Turing machines. However, we show that TIME(n¹⁺) can be defined e.g. by multi-dimensional Turing machines or by Turing machines which can jump; this is probably not true for NLT. Furthermore we consider two notions of completeness for TIME(n¹⁺) and construct complete problems. These problems are based on restrictions of Gurevich’s function logic for P.

If x is a rational number, 0<x≤1, then A(x)^c is a context-free language, where A(x) is the set of factors of the infinite Sturmian words with asymptotic density of 1’s smaller than or equal to x. We also prove a “gap” theorem i.e. A(x) can never be an unambiguous co-context-free language. The “gap” theorem is established by proving that the counting generating function of A(x) is transcendental. We show some links between Sturmian words, combinatorics and number theory.

Many problems arising in equational theories like Lambda-calculus and Combinatory Logic can be expressed by combinatory equations or systems of equations. However, the solvability problem for an arbitrarily given class of systems is in general undecidable. In this paper we shall focus our attention on a decidable class of systems, which will be called regular systems, and we shall analyse some classical problems and well-known properties of Lambda-calculus that can be described and solved by means of regular systems. The significance of such class will be emphasized showing that for slight extensions of it the solvability problem turns out to be undecidable.

We present a new proof of the existence of a small full subcategory of the effective topos which is closed under very many limits, sufficient to give an intuitive and direct interpretation of polymorphism. We describe also how to construct many new categories with enough limits to give direct interpretation of polymorphisms and other strong programming languages.