Search

The model of bulk-synchronous parallel (BSP) computation is an emerging paradigm of general-purpose parallel computing. We study the BSP complexity of subcubic algorithms for Boolean matrix multiplication. The communication cost of a standard Strassen-type algorithm is known to be optimal for general matrices. A natural question is whether it remains optimal when the problem is restricted to Boolean matrices. We give a negative answer to this question, by showing how to achieve a lower asymptotic communication cost for Boolean matrix multiplication. The proof uses a deep result from extremal graph theory, known as Szemerédi's Regularity Lemma. Despite its theoretical interest, the algorithm is not practical, because it works only on astronomically large matrices and involves huge constant factors. [ABSTRACT FROM AUTHOR]

In this paper we consider the problem of inverting an n × n circulant matrix with entries over Zm. We show that the algorithm for inverting circulants, based on the reduction to diagonal form by means of FFT, has some drawbacks when working over Zm. We present three different algorithms which do not use this approach. Our algorithms require different degrees of knowledge of m and n, and their costs range - roughly - from n log n log log n to n log2n log log n log m operations over Zm. We also present an algorithm for the inversion of finitely generated bi-infinite Toeplitz matrices. The problems considered in this paper have applications to the theory of linear Cellular Automata. [ABSTRACT FROM AUTHOR]

In the type frame originating from the flat domain of boolean values, we single out elements which are hereditarily total. We show that these elements can be defined, up to total equivalence, by sequential programs. The elements of an equivalence class of the totality equivalence relation (totality class) can be seen as different algorithms for computing a given set-theoretic boolean function. We show that the bottom element of a totality class, which is sequential, corresponds to the most eager algorithm, and the top to the laziest one. Finally we suggest a link between size of totality classes and a well known measure of complexity of boolean functions, namely their sensitivity. [ABSTRACT FROM AUTHOR]

Partial evaluation specializes terms, but traditionally this specialization does not apply to the type of these terms. As a result, specializing, e.g., an interpreter written in a typed language, which requires a “universal” type to encode expressible values, yields residual programs with type tags all over. Neil Jones has stated that getting rid of these type tags was an open problem, despite possible solutions such as Torben Mogensen's “constructor specialization.” To solve this problem, John Hughes has proposed a new paradigm for partial evaluation, “Type Specialization”, based on type inference instead of being based on symbolic interpretation. Type Specialization is very elegant in principle but it also appears non-trivial in practice. Stating the problem in terms of types instead of in terms of type encodings suggests a very simple type-directed solution, namely, to use a projection from the universal type to the specific type of the residual program. Standard partial evaluation then yields a residual program without type tags, simply and efficiently. [ABSTRACT FROM AUTHOR]

We consider systems of finite automata performing together computation on an input string. Each automaton has its own read head that moves independently of the other heads, but the automata cooperate in making state transitions. Computational power of such devices depends on the number of states of automata, the number of automata, and the way they cooperate. We concentrate our attention on the last issue. The first situation that we consider is that each automaton has a full knowledge on the states of all automata (multihead automata). The other extreme is that each automaton (called also a processor) has no knowledge of the states of other automata; merely, there is a central processing unit that may “freeze” any automaton or let it proceed its work (so called multiprocessor automata). The second model seems to be severely restricted, but we show that multihead and multiprocessor automata have similar computational power. Nevertheless, we show a separation result. [ABSTRACT FROM AUTHOR]

The following simulations by machines equipped with a one-way input tape and additional queue storage are shown:Every single-tape Turing machine (no separate input-tape) with time bound t(n) can be simulated by one queue in O(t(n)) time.Every pushdown automaton can be simulated by one queue in time O(n√n).Every deterministic machine with a one-turn pushdown store can be simulated deterministically by one queue in O(n√n) time.Every Turing machine with several multi-dimensional tapes accepting with time bound t(n) can be simulated by two queues in time O(t(n) log2t(n)).Every deterministic Turing machine with several linear tapes accepting with time bound t(n) can be simulated deterministically by a queue and a pushdown store in O(t(n) log t(n)) time. The former results appear to be the first sub-quadratic simulations of other storage devices such as pushdowns or tapes by one queue. The simulations of pushdown machines almost match the corresponding lower bounds. [ABSTRACT FROM AUTHOR]

We discuss abstractions for protection and the correctness of their implementations. Relying on the concept of full abstraction, we consider two examples: (1) the translation of Java classes to an intermediate bytecode language, and (2) in the setting of the pi calculus, the implementation of private channels in terms of cryptographic operations. [ABSTRACT FROM AUTHOR]

We study an asynchronous π-calculus, called Local π (Lπ), where: (a) only the output capability of names may be transmitted; (b) there is no matching or similar constructs. We study the basic operational and algebraic theory of Lπ and show some applications: the derivability of delayed input; the correctness of an optimisation of the encoding of call-by-name λ-calculus; the validity of some laws for the Join-calculus. [ABSTRACT FROM AUTHOR]

We generate a natural hierarchy of equivalences for asynchronous name-passing process calculi from simple variations on Milner and Sangiorgi's definition of weak barbed bisimulation. The π-calculus, used here, and the join-calculus are examples of such calculi. We prove that barbed congruence coincides with Honda and Yoshida's reduction equivalence, and with asynchronous labeled bisimulation when the calculus includes name matching, thus closing those two conjectures. We also show that barbed congruence is coarser when only one barb is tested. For the π-calculus it becomes an odd limit bisimulation, but for the join-calculus it coincides with both fair testing equivalence and with the weak barbed version of Sjödin and Parrow's coupled simulation. [ABSTRACT FROM AUTHOR]

Score functions (potential functions) have been used effectively in many problems in molecular biology. We propose a general method for deriving score functions that are consistent with example data, which yields polynomial time learning algorithms for several important problems in molecular biology (including sequence alignment). On the other hand, we show that deriving a score function for some problems (multiple alignment and protein threading) is computationally hard. However, we show that approximation algorithms for these optimization problems can also be used for deriving score functions. [ABSTRACT FROM AUTHOR]

We study some extensions of Grover's quantum searching algorithm. First, we generalize the Grover iteration in the light of a concept called amplitude amplification. Then, we show that the quadratic speedup obtained by the quantum searching algorithm over classical brute force can still be obtained for a large family of search problems for which good classical heuristics exist. Finally, as our main result, we combine ideas from Grover's and Shor's quantum algorithms to perform approximate counting, which can be seen as an amplitude estimation process. [ABSTRACT FROM AUTHOR]

Martin-Löf defined infinite random sequences over a finite alphabet via randomness tests which describe sets having measure zero in a constructive sense. In this paper this concept is generalized to separable topological spaces with a measure. We show several general results, like the existence of a universal randomness test under weak conditions, and a randomness preservation result for functions between randomness spaces. Applying these ideas to the real numbers yields a direct definition of random real numbers which is shown to be equivalent to the usual one via the representation of real numbers to some base. Furthermore, we show that every nonconstant computable analytic function preserves randomness. As a second example, by considering the power set of the natural numbers with its natural topology as a randomness space, we introduce a new notion of a random set of numbers. We characterize it in terms of random sequences. Surprisingly, it turns out that there are infinite co-r.e. random sets. [ABSTRACT FROM AUTHOR]

We show that the class NISZK of languages that admit non-interactive statistical zero-knowledge proof system has a natural complete promise problem. This characterizes statistical zero-knowledge in the public random string model without reference to the public random string or to zero knowledge. Building on this result we are able to show structural properties of NISZK such as closure under OR composition and closure under complement. [ABSTRACT FROM AUTHOR]

We study interactive arguments, in particular their error probability under sequential iteration. This problem is more complex than for interactive proofs, where the error trivially decreases exponentially in the number of iterations. In particular, we study the typical efficient case where the iterated protocol is based on a single instance of a computational problem. This is not a special case of independent iterations of an entire protocol, and real exponential decrease of the error cannot be expected. Nevertheless, for practical applications, one needs concrete relations between the complexity and error probability of the underlying problem and the iterated protocol. We formalize and solve this problem using the theory of proofs of knowledge. We also seem to present the first definition of arguments in a fully uniform model of complexity. We also prove that in non-uniform complexity, the error probability of independent iterations of an argument does decrease exponentially — to our knowledge this is the first result about a strictly exponentially small error probability in a computational cryptographic security property. To illustrate our first result, we present a very efficient zero-knowledge argument for circuit satisfiability, and thus for any NP problem, based on any collision-intractable hash function. [ABSTRACT FROM AUTHOR]

We propose a general technique, inspired from proof-irrelevance, to prove strong normalisation and consistency for extensions of the Calculus of Constructions. [ABSTRACT FROM AUTHOR]

This paper introduces a λ-calculus with explicit substitutions, corresponding to an S4 modal logic of constructive necessity. As well as being semantically well motivated, the calculus can be used (a) to develop abstract machines, and (b) as a framework for specifying and analysing computation stages in the context of functional languages. We prove several syntactic properties of this calculus, which we call xDIML, and then sketch its use as an interpretation of binding analysis and partial evaluation which respects execution of programs in stages. [ABSTRACT FROM AUTHOR]

One of the most intricate algorithms related to words is Makanin's algorithm solving word equations. The algorithm is very complicated and the complexity of the problem of solving word equations is not well understood. Word equations can be used to define various properties of strings, e.g. general versions of pattern-matching with variables. This paper is devoted to introduce a new approach and to study relations between Lempel-Ziv compressions and word equations. Instead of dealing with very long solutions we propose to deal with their Lempel-Ziv encodings. As our first main result we prove that each minimal solution of a word equation is highly compressible (exponentially compressible for long solutions) in terms of Lempel-Ziv encoding. A simple algorithm for solving word equations is derived. If the length of minimal solution is bounded by a singly exponential function (which is believed to be always true) then LZ encoding of each minimal solution is of a polynomial size (though the solution can be exponentially long) and solvability can be checked in nondeterministic polynomial time. As our second main result we prove that the solvability can be tested in polynomial deterministic time if the lengths of all variables are given in binary. We show also that lexicographically first solution for given lengths of variables is highly compressible in terms of Lempel-Ziv encodings. [ABSTRACT FROM AUTHOR]

With efficiency motivations the notion of symbolic transition graph for the π-calculus is proposed along the lines of [4,7]. The single/double ground/symbolic arrows are given to such graphs. Based on them the strong/weak ground/symbolic bisimulation equivalences and observation congruences are defined and are shown to agree with each other. The notions of symbolic observation graph and symbolic congruence graph are also introduced. Finally algorithms for checking strong/weak bisimulation equivalences and observation congruence are presented together with their correctness proofs. These results lift and refine the techniques and algorithms for bisimulation checking of regular pure-CCS and value-passing process to the finite control π-calculus. [ABSTRACT FROM AUTHOR]

This paper considers how locality restrictions on the use of capabilities can be enforced by a static type system. A distributed π-calculus with a simple reduction semantics is introduced, integrating location and migration primitives from the Distributed Join Calculus with asynchronous π communication. It is given a type system in which the input and output capabilities of channels may be either global, local or absent. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. We show that the most local possible capabilities for internal channels can be inferred automatically. [ABSTRACT FROM AUTHOR]

We present polynomial-time approximation schemes for the problem of finding a minimum-cost k-connected Euclidean graph on a finite point set in Rd. The cost of an edge in such a graph is equal to the Euclidean distance between its endpoints. Our schemes use Steiner points. For every given c > 1 and a set S of n points in ℝd, a randomized version of our scheme finds an Euclidean graph on a superset of S which is k-vertex (or k-edge) connected with respect to S, and whose cost is with probability 1/2 within (1 + 1/c) of the minimum cost of a k-vertex (or k-edge) connected Euclidean graph on S, in time $$n \cdot \left( {logn} \right)^{\left( {\mathcal{O}\left( {c\sqrt d k} \right)} \right)^{d - 1} } \cdot 2^{\left( {\left( {\mathcal{O}\left( {c\sqrt d k} \right)} \right)^{d - 1} } \right)!}$$ . We can derandomize the scheme by increasing the running time by a factor O(n). We also observe that the time cost of the derandomization of the PTA schemes for Euclidean optimization problems in ℝd derived by Arora can be decreased by a multiplicative factor of Ω(nd−1). [ABSTRACT FROM AUTHOR]

This paper considers the problem of selecting a minimum communication spanning tree (MCT) for a given weighted network, namely, a tree that minimizes the total cost of transmitting a given set of communication requirements between n sites over the tree edges [8]. A slightly stronger formulation of the problem [1] is based on the concept of a minimum average stretch spanning tree (MAST) for weighted connected multigraphs. In particular, a ρ-solution for the MAST problem (namely, an algorithm for constructing a spanning tree with average stretch ρ) in the special case of complete weighted graphs implies an approximation algorithm for the MCT problem with approximation ratio ρ. It is conjectured in [1] that for any given weighted multigraph there exists a spanning tree with average stretch O(log n) (which is the best possible, in view of the Ω(log n) lower bound given therein). However, the (deterministic) construction presented (which is the best construction to date) yields only a bound of exp(O(√ log n log log n)) on the average stretch. For the restricted case of complete weighted graphs, there is a better, albeit randomized, construction yielding average stretch O(log2n) [2]. This implies a randomized approximation algorithm for MCT with the same ratio. This paper presents a deterministic algorithm that for every weighted complete multigraph constructs a spanning tree whose average stretch is bounded by O(log2n). This yields a deterministic polynomial-time approximation algorithm for MCT with ratio O(log2n). In addition, our solution approach confirms the conjecture of [1] in the special case of d-dimensional Euclidean complete multigraphs for fixed d, where our construction yields spanning trees with O(log n) average stretch. [ABSTRACT FROM AUTHOR]

The Μ-calculus can be viewed as essentially the “ultimate” program logic, as it expressively subsumes all propositional program logics, including dynamic logics, process logics, and temporal logics. It is known that the satisfiability problem for the Μ-calculus is EXPTIME-complete. This upper bound, however, is known for a version of the logic that has only forward modalities, which express weakest preconditions, but not backward modalities, which express strongest postconditions. Our main result in this paper is an exponential time upper bound for the satisfiability problem of the Μ-calculus with both forward and backward modalities. To get this result we develop a theory of two-way alternating automata on infinite trees. [ABSTRACT FROM AUTHOR]

An architecture is described for designing systems that acquire and manipulate large amounts of unsystematized, or so-called commonsense, knowledge. Its aim is to exploit to the full those aspects of computational learning that are known to offer powerful solutions in the acquisition and maintenance of robust knowledge bases. The architecture makes explicit the requirements on the basic computational tasks that are to be performed and is designed to make these computationally tractable even for very large databases. The main claims are that (i) the basic learning tasks are tractable and (ii) tractable learning offers viable approaches to a range of issues that have been previously identified as problematic for artificial intelligence systems that are entirely programmed. In particular, attribute efficiency holds a central place in the definition of the learning tasks, as does also the capability to handle relational information efficiently. Among the issues that learning offers to resolve are robustness to inconsistencies, robustness to incomplete information and resolving among alternatives. [ABSTRACT FROM AUTHOR]

Given a graph G and a (multi-)set of pairs of vertices in it, the classical NP-hard maximum edge-disjoint-paths problem (MDP) is to connect as many of the given pairs as possible using pairwise edge-disjoint paths in G. We study a relative of this problem: we have a network with fixed link capacities that may have to service large demands when necessary. In particular, individual demands are allowed to exceed capacities, and thus flows for some request pairs necessarily have to be split into different flow-paths. This is the framework for computational problems arising from: (i) electrical power networks due to the proposed deregulation of the electric utility industry in the USA, and (ii) applications such as real-time Internet services (e.g., telephone, fax, video). We show that these problems come in a few variants, some efficiently solvable and many NP-hard; we also present approximation algorithms for many of the NP-hard variants presented. Some of our approximation algorithms benefit from certain improved tail estimates that we derive; the latter also yield improved approximations for a family of packing integer programs. [ABSTRACT FROM AUTHOR]

We study entailment of structural and nonstructural recursive subtyping constraints. Constraints are formal inequalities between type expressions, interpreted over an ordered set of possibly infinite labeled trees. The nonstructural ordering on trees is the one introduced by Amadio and Cardelli for subtyping with recursive types. The structural ordering compares only trees with common shape. A constraint set entails an inequality if every assignment of meanings (trees) to type expressions that satisfies all the constraints also satisfies the inequality. In this paper we prove that nonstructural subtype entailment is PSPACE-hard, both for finite trees (simple types) and infinite trees (recursive types). For the structural ordering we prove that subtype entailment over infinite trees is PSPACE-complete, when the order on trees is generated from a lattice of type constants. Since structural subtype entailment over finite trees has been shown to be coNP-complete these are the first complexity-theoretic separation results that show that, informally, nonstructural subtype entailment is harder than structural entailment, and recursive entailment is harder than nonrecursive entailment. [ABSTRACT FROM AUTHOR]

In this paper we consider Interval Routing Schemes (IRS) that are optimal with respect to the congestion of the induced path system. We provide a general framework able to deal with the various congestion issues in IRS. In fact, it is possible to distinguish between static cases, in which the source-destination configurations are fixed, and dynamic cases, where they vary over time. All these situations can be handled in a unified setting, thanks to the notion of competitiveness introduced in this paper. We first give some general results not related to specific traffic demands. Then, in the one-to-all communication pattern, we show that constructing competitive IRS for a given network is an intractable problem, both for the static and the dynamic case, that is respectively when the root vertex is fixed and when it can change along the time. Finally, both for one-to-all and all-to-all communication patterns, we provide nicely competitive k-IRS for relevant topologies. Networks considered are chains, trees, rings, chordal rings and multi-dimensional grids and tori. We consider both the directed congestion case, in which there are pairwise opposite unidirectional links connecting two neighbor processors, and the undirected congestion case, in which two neighbors are connected by a single bi-directional link. [ABSTRACT FROM AUTHOR]

A specification formalism for reactive systems defines a class of Ω-languages. We call a specification formalism fully decidable if it is constructively closed under boolean operations and has a decidable satisfiability (nonemptiness) problem. There are two important, robust classes of Ω-languages that are definable by fully decidable formalisms. The Ω -reqular languages are definable by finite automata, or equivalcntly, by the Sequential Calculus. The counter-free Ω-regular languages are definable by temporal logic, or equivalcntly, by the first-order fragment of the Sequential Calculus. The gap between both classes can be closed by finite counting (using automata connectives), or equivalently, by projection (existential second-order quantification over letters). A specification formalism for real-time systems defines a class of timed Ω-langnages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed Ω-languages are robust, and we explain their relationship. First, we show that temporal logic with event clocks defines the same class of timed Ω-languages as temporal logic with nonsingular time bounds, and we identify a first-order monadic theory that also defines this class. Second, we show that if the ability of finite counting is added to these formalisms, we obtain the class of timed Ω-languages that are definable by finite automata with event clocks, or equivalently, by a restricted second-order extension of the monadic theory. Third, we show that if projection is added, we obtain the class of timed Ω-languages that are definable by timed automata, or equivalently, by a richer second-order extension of the monadic theory. These results identify three robust classes of timed Ω-languages, of which the third, while popular, is not definable by a, fully decidable formalism. By contrast, the first two classes are definable by fully decidable formalisms from temporal logic, from automata theory, and from monadic logic. Since the gap between these two classes can be closed by finite counting, we dub them the timed Ω-regular languages and the timed counter-free Ω-rcgular languages, respectively. [ABSTRACT FROM AUTHOR]

This paper investigates the use of a complete metric space framework for providing denotational semantics to a real-time process algebra. The study is carried out in a non-interleaving setting and is based on a timed extension of Langerak's bundle event structures, a variant of Winskel's event structures. The distance function is based on the amount of time to which event structures do ‘agree’. We show that this intuitive notion of distance is a pseudo metric (but not a metric) on the set of timed event structures. A generalisation to equivalence classes of timed event structures in which we abstract from event names and non-executable events (events that can never appear) is shown to be a complete ultra-metric space. We show that the resulting metric semantics is an abstraction of an existing cpo-based denotational and a related operational semantics for the considered language. [ABSTRACT FROM AUTHOR]

A mimicking network for a k-terminal network, N, is one whose realizable external flows are the same as those of N. Let S(k) denote the minimum size of a mimicking network for a k-terminal network. In this paper we give new constructions of mimicking networks and prove the following results (the values in brackets are the previously best known results): S(4) = 5 [216], S(5) = 6 [232]. For bounded treewidth networks we show S(k) = O(k) [22k], and for outerplanar networks we show S(k) ≤ 10k − 6 [k22k+2]. [ABSTRACT FROM AUTHOR]

Let T be a symmetric directed tree, i.e., a tree with each edge viewed as two opposite directed links. We consider the problem of routing arbitrary sets of connection requests in T. In all-optical communication tree networks with WDM (wavelength-division multiplexing) this is equivalent to color a given set of directed paths so that no two directed paths of the same color use the same link of T. Let W be the number of available wavelengths. The load, that is, the maximum number of directed paths passing through a link of T cannot exceed W. If there is no wavelength conversion available then each request (directed path) is restricted to a single wavelength and it is known that the minimum number of colors needed to color any set of directed paths in a tree is lower bounded away from the load L of the paths on the tree; moreover, no algorithm is known that uses a number of colors less than 5L/3. The presence of wavelength converters allows to overcome this limits. The complexity of converters is measured by the maximum degree, which represents the maximum number of possible conversions of any given wavelength. We show that it is possible to route any set of requests of load L ≤ W(1 − e), where ε depends only on the degree of the converters. Moreover, we show that in any tree it is possible to route any set of requests of load L <- W with converters of degree O(√W). In case of trees containing at most one node of degree ≥ 4 we show that converters of degree 3 already allow to route any set of requests of load L≤W. [ABSTRACT FROM AUTHOR]

The higher-order rewriting in presence of associative and commutative (AC) symbols is considered. A higher-order reduction ordering which allows to state the termination of a given rewriting system is presented. This ordering is an AC-extensiou of λ-RPO and is defined on simply-typed λ-terms in Β-normal η-long form. It is total on ground terms. [ABSTRACT FROM AUTHOR]

The article is mainly concerned with the Kruskal tree theorem and the following observation: there is a duality at the level of binary relations between well and noetherian orders. The first step here is to extend Kruskal theorem from orders to binary relations so that the duality applies. Then, we describe the theorem obtained by duality and show that it corresponds to a theorem by Ferreira and Zantema which subsumes Dershowitz's seminal results on recursive path orderings. [ABSTRACT FROM AUTHOR]

In the seventies, several classification schemes for the rational languages were proposed, based on the alternate use of certain operators (union, complementation, product and star). Some thirty years later, al-though much progress has been done, several of the original problems are still open. Furthermore, their significance has grown considerably over the years, on account of the successive discoveries of surprising links with other fields, like non commutative algebra, finite model theory, structural complexity and topology. In this article, we solve positively a question raised in 1985 about concatenation hierarchies of rational languages, which are constructed by alternating boolean operations and concate-nation products. We establish a simple algebraic connection between the Straubing-Thérien hierarchy, whose basis is the trivial variety, and the group hierarchy, whose basis is the variety of group languages. Thanks to a recent result of Almeida and Steinberg, this reduces the decidability problem for the group hierarchy to a property stronger than decidability for the Straubing-Thérien hierarchy. [ABSTRACT FROM AUTHOR]

For a string rewriting system, it is known that termination by a simplification ordering implies multiple recursive complexity. This theoretical upper bound is, however, far from having been reached by known examples of rewrite systems. All known methods used to establish termination by simplification yield a primitive recursive bound. Furthermore, the study of the order types of simplification orderings suggests that the recursive path ordering is, in a broad sense, a maximal simplification ordering. This would imply that simplifying string rewrite systems cannot go beyond primitive recursion. Contradicting this intuition, we construct here a simplifying string rewriting system whose complexity is not primitive recursive. This leads to a new lower bound for the complexity of simplifying string rewriting systems. [ABSTRACT FROM AUTHOR]

We show how to compute the entropy of two important classes of cellular automata namely, linear and positively expansive cellular automata. In particular, we prove a closed formula for the topological entropy of D-dimensional (D ≥ 1) linear cellular automata over the ring Zm (m ≥ 2) and we provide an algorithm for computing the topological entropy of positively expansive cellular automata. [ABSTRACT FROM AUTHOR]

We study determinization of weighted finite-state automata (WFAs), which has important applications in automatic speech recognition (ASR). We provide the first polynomial-time algorithm to test for the twins property, which determines if a WFA admits a deterministic equivalent. We also provide a rigorous analysis of a determinization algorithm of Mohri, with tight bounds for acyclic WFAs. Given that WFAs can expand exponentially when determinized, we explore why those used in ASR tend to shrink. The folklore explanation is that ASR WFAs have an acyclic, multi-partite structure. We show, however, that there exist such WFAs that always incur exponential expansion when determinized. We then introduce a class of WFAs, also with this structure, whose expansion depends on the weights: some weightings cause them to shrink, while others, including random weightings, cause them to expand exponentially. We provide experimental evidence that ASR WFAs exhibit this weight dependence. That they shrink when determinized, therefore, is a result of favorable weightings in addition to special topology. [ABSTRACT FROM AUTHOR]

We use the fusion calculus, a generalization and simplification of the π-calculus, to model concurrent constraint programming. In particular we encode three basic variants of the ρ-calculus, which is a foundational calculus for the concurrent constraint programming language Oz. Using a new reduction-based semantics and weak barbed congruences for the fusion calculus we formally establish an operational correspondence between the ρ-calculi and their encodings. These barbed congruences are shown to coincide with the hyper-equivalences previously adopted for the fusion calculus. [ABSTRACT FROM AUTHOR]

Proof systems for weak bisimulation congruences in the finite-control π-calculus are presented and their completeness proved. This study consists of two major steps: first complete proof systems for guarded recursions arc obtained; then sound laws sufficient to remove any unguarded recursions are formulated. These results lift Milner's axiomatisation for observation congruence in regular pure-CCS to the π-calculus. The completeness proof relies on the symbolic bisimulation technique. [ABSTRACT FROM AUTHOR]

We give an account of part of modularity in denotational semantics. We define a computational effect to consist of a category with algebraic structure together with a construction using that algebraic structure of a new denotational category together with an identity on objects functor to it from the original category. We make precise what we mean by algebraic structure and what constructions are allowable. Further, given two computational effects, we give a mathematical foundation for extending one along the other. We prove a theorem to show when such a extension is possible. [ABSTRACT FROM AUTHOR]

We call a one-way infinite word w over a finite alphabet (ρ,ρ)-repetitive if all long enough prefixes of w contain as a suffix a repetition of order ρ of a word of length at most p. We show that each (2,4)-repetitive word is ultimately periodic, as well as that there exist nondenumerably many, and hence also nonultimately periodic, (2,5)-repetitive words. Further we characterize nonultimately periodic (2, 5)-repetitive words both structurally and algebraically. [ABSTRACT FROM AUTHOR]

We have presented a new class of tree automata which can deal with several interpreted domains and which extends previous works on constrained tree automata and automata dealing with AC axioms. The proof used for the decision of emptiness in the multiset case is new and may have other applications. This approach is complementary of the approach in [BJ97] which deals with specifications involving equations between constructors but doesn't handle the domains that we consider. Future work will be to embed the previous approach of [LM94] in our class and to look for efficient implementation of tree automata algorithms with AC symbols similar to [Mon97]. [ABSTRACT FROM AUTHOR]

We introduce an extension of the Calculus of Construction with inductive and co-inductive types that preserves normalisation, while keeping a relatively simple collection of typing rules. This extension considerably enlarges the expressiveness of the language, enabling a direct representation of recursive programs in type theory. [ABSTRACT FROM AUTHOR]

We investigate the problem of finding two nonempty disjoint subsets of a set of n positive integers, with the objective that the sums of the numbers in the two subsets be as close as possible. In two versions of this problem, the quality of a solution is measured by the ratio and the difference of the two partial sums, respectively. Answering a problem of Woeginger and Yu (1992) in the affirmative, we give a fully polynomial-time approximation scheme for the case where the value to be optimized is the ratio between the sums of the numbers in the two sets. On the other hand, we show that in the case where the value of a solution is the positive difference between the two partial sums, the problem is not 2nk -approximable in polynomial time unless P=NP, for any constant k. In the positive direction, we give a polynomial-time algorithm that finds two subsets for which the difference of the two sums does not exceed K/nΩ(log n) where K is the greatest number in the instance. [ABSTRACT FROM AUTHOR]

Given a multiset X={x1,... xn} of real numbers, the floating-point set summation (FPS) problem asks for Sn = x1+...+ xn, and the floating point prefix set summation problem (FPPS) asks for Sk=x1+...+xk for all k = 1, ... n. Let Ek* denote the minimum worst-case error over all possible orderings of evaluating Sk. We prove that if X has both positive and negative numbers, it is NP-hard to compute Sn with the worst-case error equal to En*. We then give the first known polynomial-time approximation algorithm for computing Sn that has a provably small error for arbitrary X. Our algorithm incurs a worstcase error at most 2([log(n−1)]+1) En*. After X is sorted, it runs in O(n) time, yielding an O(n2)-time approximation algorithm for computing Sk for all k = 1, ..., n such that the worst-case error for each Sk is less than 2(⌈ log(k−1)⌋+ 1)Ek*. For the case where X is either all positive or all negative, we give another approximation algorithm for computing Sn with a worst-case error at most ⌈ log log n⌋En*. Even for unsorted X, this algorithm runs in O(n) time. Previously, the best linear-time approximation algorithm had a worst-case error at most ⌈ log n⌋En*, while En* was known to be attainable in O(n log n) time using Huffman coding. Consequently, FPPS is solvable in O(n2) time such that the worst-case error for each Sk is the minimum. To improve this quadratic time bound in practice, we design two on-line algorithms that calculate the next Sk by taking advantage of the current Sk and thus reduce redundant computation. [ABSTRACT FROM AUTHOR]

We introduce a generalization of the classical notion of flowchart for languages with higher order and object-oriented features. These general flowcharts are obtained by an abstraction of the game semantics for Idealized Algol and as such rely on a solid mathematical basis. We demonstrate how charts may be used as the basis for data flow analysis. [ABSTRACT FROM AUTHOR]

In this paper a Markov chain for contingency tallies with two lows is defined. The chain is shown to be rapidly mixing using the path coupling method. The mixing time of the chain is quadratic in the number of columns and linear in the logarithm of the table sum. Two extensions of the new chain are discussed: one for three-rowed contingency tables and one for m-rowed contingency tables. We show that, unfortunately, it is not possible to prove rapid mixing for these chains by simply extending the path coupling approach used in the two-rowed case. [ABSTRACT FROM AUTHOR]

It is well known that the performance of quicksort can be substantially improved by selecting the median of a sample of three elements as the pivot of each partitioning stage. This variant is easily generalized to samples of size s = 2k+1. For large samples the partitions are better as the median of the sample makes a more accurate estimate of the median of the array to be sorted, but the amount of additional comparisons and exchanges to find the median of the sample also increases. We show that the optimal sample size to minimize the average total cost of quicksort (which includes both comparisons and exchanges) is s = a · √n+o(√n). We also give a closed expression for the constant factor a, which depends on the median-finding algorithm and the costs of elementary comparisons and exchanges. The result above holds in most situations, unless the cost of an exchange exceeds by far the cost of a comparison. In that particular case, it is better to select not the median of the samples, but the (p}+1)th element. The value of p can be precisely determined as a function of the ratio between the cost of an exchange and the cost of a comparison. [ABSTRACT FROM AUTHOR]

Existential types have proved useful for classifying various kinds of information hiding in programming languages, such as occurs in abstract datatypes and objects. In this paper we address the question of when two elements of an existential type are semantically equivalent. Of course, it depends what one means by ‘semantic equivalence’. Here we take a syntactic approach—so semantic equivalence will mean some kind of operational equivalence. The paper begins by surveying some of the literature on this topic involving ‘logical relations’. Matters become quite complicated if the programming language mixes existential types with function types and features involving non-termination (such as recursive definitions). We give an example (suggested by Ian Stark) to show that in this case the existence of suitable relations is sufficient, but not necessary for proving operational equivalences at existential types. Properties of this and other examples are proved using a new form of operationally-based logical relation which does in fact provide a useful characterisation of operational equivalence for existential types. [ABSTRACT FROM AUTHOR]

In the classical theory of Petri nets, a process is an operational description of the behaviour of a net, which takes into account the causal links between transitions in a sequence of firing steps. In the categorical framework developed in [19,11], processes of a P/T net are modeled as arrows of a suitable monoidal category: In this paper we lay the basis of a similar characterization for contextual P/T nets, that is, P/T nets extended with read arcs, which allows a transition to check for the presence of a token in a place, without consuming it. [ABSTRACT FROM AUTHOR]

Several formal concurrent semantics have been proposed for graph rewriting, a powerful formalism for the specification of concurrent and distributed systems which generalizes P/T Petri nets. In this paper we relate two such semantics recently proposed for the algebraic double-pushout approach to graph rewriting, namely the derivation trace and the graph process semantics. The notion of concatenable graph process is introduced and then the category of concatenable derivation traces is shown to be isomorphic to the category of concatenable graph processes. As an outcome we obtain a quite intuitive characterization of events and configurations of the event structure associated to a graph grammar. [ABSTRACT FROM AUTHOR]