Matrices, machines and behaviors

Sabadini, Walters and others have developed a categorical, machine based theory of concurrency in which there are four essential aspects: a distributive category of data-types; a bicategory Mach whose objects are data types, and whose arrows are input-output machines built from data types; a semantic category (or categories) Sem, suitable to contain the behaviors of machines, and a functor, behavior: MachSem. Suitable operations on machines and semantics are found so that the behavior functor preserves these operations. Then, if each machine is decomposable into primitive machines using these operations, the behavior of a general machine is deducible from the behavior of its parts. The theory of non-deterministic finite state automata provides an example of the paradigm and also throws some light on the classical theory of finite state automata.We describe a bicategory whose objects are natural numbers, in which an arrow M: np is a finite state automaton with n input states, p output states, and some additional internal states; we require that no transitions begin at output states or end at input states. A machine is represented by an q+n by q+p matrix. The bicategory supports additional operations: non-deterministic choice, parallel interleaving, and feedback. Enough operations are imposed on machines to show that each machine may be obtained from some atomic ones by means of the operations.The semantic category is the (Bloom-Ésik) iteration theory Mat _(X whose objects are natural numbers and whose arrows from n to p are n×p matrices with entries in the semiring of languages. The behavior functor associates to a machine M: np a matrix |M| of languages, one language to each pair of input and output states. Behavior preserves composition, feedback, takes non-deterministic choice to union, and parallel-interleaving to shuffle. Thus, behavior gives a compositional semantics to a primitive notion of concurrent processes.This work has been supported by the Australian Research Council, by CEC under grant number 6317, ASMICS II, by Italian MURST, and by the Italian CNR.Visit to Sydney supported by a grant from the Australian Research Council.Presented at the European Colloquium of Category Theory, Tours, France, 25–31 July 1994.     

A game semantics for disjunctive logic programming

Denotational semantics of logic programming and its extensions (by allowing negation, disjunctions, or both) have been studied thoroughly for many years. In 1998, a game semantics was given to definite logic programs by Di Cosmo, Loddo, and Nicolet, and a few years later it was extended to deal with negation by Rondogiannis and Wadge. Both approaches were proven equivalent to the traditional semantics. In this paper we define a game semantics for disjunctive logic programs and prove soundness and completeness with respect to the minimal model semantics of Minker. The overall development has been influenced by the games studied for PCF and functional programming in general, in the styles of Abramsky–Jagadeesan–Malacaria and Hyland–Ong–Nickau.     

Equilibrium semantics of languages of imperfect information

In this paper, we introduce a new approach to independent quantifiers, as originally introduced in Informational independence as a semantic phenomenon by Hintikka and Sandu (1989) [9] under the header of independence-friendly (IF) languages. Unlike other approaches, which rely heavily on compositional methods, we shall analyze independent quantifiers via equilibriums in strategic games. In this approach, coined equilibrium semantics, the value of an IF sentence on a particular structure is determined by the expected utility of the existential player in any of the game’s equilibriums. This approach was suggested in Henkin quantifiers and complete problems by Blass and Gurevich (1986) [2] but has not been taken up before. We prove that each rational number can be realized by an IF sentence. We also give a lower and upper bound on the expressive power of IF logic under equilibrium semantics.     

Full abstraction for Reduced ML

We present the first effectively presentable fully abstract model for Stark?s Reduced ML, a call-by-value higher-order programming language featuring integer-valued references. The model is constructed using techniques of nominal game semantics. Its distinctive feature is the presence of carefully restricted information about the store in plays, combined with conditions concerning the participants? ability to distinguish reference names. We show how it leads to an explicit characterization of program equivalence.     

Qualitative versus quantitative fixed point techniques in computer science

In 1970, a qualitative fixed point technique useful to model the recursive specifications in denotational semantics was developed by means of the celebrated Kleene‘s fixed point theorem. Later on, in 1994 and 1995, quantitative counterparts of the aforesaid technique, but now based on generalized versions of Banach fixed point theorem, were obtained in such a way that the spirit of Kleene‘s technique was preserved. These new techniques are able to provide a measure of the information content degree and this fact has constituted an advantage with respect to the qualitative techniques. The main purpose of this paper is to discern the relationship between the aforementioned qualitative and quantitative fixed point techniques. In particular, we clarify what is the additional real contribution of the quantitative fixed point techniques with respect to the qualitative ones.     

Lower Bounds For Concurrent Zero Knowledge*

We consider zero knowledge interactive proofs in a richer, more realistic communication environment. In this setting, one may simultaneously engage in many interactive proofs, and these proofs may take place in an asynchronous fashion. It is known that zero-knowledge is not necessarily preserved in such an environment; we show that for a large class of protocols, it cannot be preserved. Any 4 round (computational) zero-knowledge interactive proof (or argument) for a non-trivial language L is not black-box simulatable in the asynchronous setting.* An abridge version of this work has appeared in [24].     

Dichotomy Results for Fixed-Point Existence Problems for Boolean Dynamical Systems

A complete classification of the computational complexity of the fixed-point existence problem for Boolean dynamical systems, i.e., finite discrete dynamical systems over the domain {0, 1}, is presented. For function classes and graph classes , an ()-system is a Boolean dynamical system such that all local transition functions lie in and the underlying graph lies in . Let be a class of Boolean functions which is closed under composition and let be a class of graphs which is closed under taking minors. The following dichotomy theorems are shown: (1) If contains the self-dual functions and contains the planar graphs, then the fixed-point existence problem for ()-systems with local transition function given by truth-tables is NP-complete; otherwise, it is decidable in polynomial time. (2) If contains the self-dual functions and contains the graphs having vertex covers of size one, then the fixed-point existence problem for ()-systems with local transition function given by formulas or circuits is NP-complete; otherwise, it is decidable in polynomial time.      

Independence and port oracles for matroids,with an application to computational learning theory

Given a matroidM with distinguished elemente, aport oracie with respect toe reports whether or not a given subset contains a circuit that containse. The first main result of this paper is an algorithm for computing ane-based ear decomposition (that is, an ear decomposition every circuit of which contains elemente) of a matroid using only a polynomial number of elementary operations and port oracle calls. In the case thatM is binary, the incidence vectors of the circuits in the ear decomposition form a matrix representation forM. Thus, this algorithm solves a problem in computational learning theory; it learns the class ofbinary matroid port (BMP) functions with membership queries in polynomial time. In this context, the algorithm generalizes results of Angluin, Hellerstein, and Karpinski [1], and Raghavan and Schach [17], who showed that certain subclasses of the BMP functions are learnable in polynomial time using membership queries. The second main result of this paper is an algorithm for testing independence of a given input set of the matroidM. This algorithm, which uses the ear decomposition algorithm as a subroutine, uses only a polynomial number of elementary operations and port oracle calls. The algorithm proves a constructive version of an early theorem of Lehman [13], which states that the port of a connected matroid uniquely determines the matroid.Research partially funded by NSF PYI Grant No. DDM-91-96083.Research partially funded by NSF Grant No CCR-92-10957.     

Parallel computing in combinatorial optimization

This is a review of the literature on parallel computers and algorithms that is relevant for combinatorial optimization. We start by describing theoretical as well as realistic machine models for parallel computations. Next, we deal with the complexity theory for parallel computations and illustrate the resulting concepts by presenting a number of polylog parallel algorithms andP-completeness results. Finally, we discuss the use of parallelism in enumerative methods.     

A Computationally Motivated Definition Of Parametric Estimation And Its Applications To The Gaussian Distribution

We introduce a treatment of parametric estimation in which optimality of an estimator is measured in probability rather than in variance (the measure for which the strongest general results are known in statistics). Our motivation is that the quality of an approximation algorithm is measured by the probability that it fails to approximate the desired quantity within a set tolerance. We concentrate on the Gaussian distribution and show that the sample mean is the unique “best” estimator, in probability, for the mean of a Gaussian distribution. We also extend this method to general penalty functions and to multidimensional spherically symmetric Gaussians. The algorithmic significance of studying the Gaussian distribution is established by showing that determining the average matching size in a graph is #P-hard, and moreover approximating it reduces to estimating the mean of a random variable that (under some mild conditions) has a distribution closely approximating a Gaussian. This random variable is (essentially) polynomial time samplable, thereby yielding an FPRAS for the problem.     

Tropological systems are points of quantales

We address two areas in which quantales have been used. One is of a topological nature, whereby quantales or involutive quantales are seen as generalized noncommutative spaces, and its main purpose so far has been to investigate the spectrum of noncommutative C∗-algebras. The other sees quantales as algebras of abstract experiments on physical or computational systems, and has been applied to the study of the semantics of concurrent systems. We investigate connections between the two areas, in particular showing that concurrent systems, in the form of either set-theoretic or localic tropological systems, can be identified with points of quantales by means of a suitable adjunction, which indeed holds for a much larger class of so-called “tropological models”. We show that in the case of tropological models in factor quantales, which still generalize tropological systems, the identification of models and (generalized) points preserves all the information needed for describing the observable behaviour of systems. We also define a notion of morphism of models that generalizes previous definitions of morphism of systems, and show that morphisms, too, can be defined in terms of either side of the adjunction, in fact giving us isomorphisms of categories. The relation between completeness notions for tropological systems and spatiality for quantales is also addressed, and a preliminary partial preservation result is obtained.     

Characterizing Valiant's algebraic complexity classes

Valiant introduced 20 years ago an algebraic complexity theory to study the complexity of polynomial families. The basic computation model used is the arithmetic circuit, which makes these classes very easy to define and open to combinatorial techniques. In this paper we gather known results and new techniques under a unifying theme, namely the restrictions imposed upon the gates of the circuit, building a hierarchy from formulas to circuits. As a consequence we get simpler proofs for known results such as the equality of the classes VNP and _VNPe${\mathrm{VNP}}_{\mathrm{e}}$ or the completeness of the Determinant for VQP, and new results such as a characterization of the classes VQP and VP (which we can also apply to the Boolean class LOGCFL) or a full answer to a conjecture in Bürgisser's book [Completeness and reduction in algebraic complexity theory, Algorithms and Computation in Mathematics, vol. 7, Springer, Berlin, 2000]. We also show that for circuits of polynomial depth and unbounded size these models all have the same expressive power and can be used to characterize a uniform version of VNP.     

Pseudorandom generators for space-bounded computation

Pseudorandom generators are constructed which convertO(SlogR) truly random bits toR bits that appear random to any algorithm that runs inSPACE(S). In particular, any randomized polynomial time algorithm that runs in spaceS can be simulated using onlyO(Slogn) random bits. An application of these generators is an explicit construction of universal traversal sequences (for arbitrary graphs) of lengthn ^O(logn).The generators constructed are technically stronger than just appearing random to spacebounded machines, and have several other applications. In particular, applications are given for deterministic amplification (i.e. reducing the probability of error of randomized algorithms), as well as generalizations of it.This work was done in the Laboratory for Computer Science, MIT, supported by NSF 865727-CCR and ARO DALL03-86-K-017     

A simulation tool for the performance evaluation of parallel branch and bound algorithms

Parallel computation offers a challenging opportunity to speed up the time consuming enumerative procedures that are necessary to solve hard combinatorial problems. Theoretical analysis of such a parallel branch and bound algorithm is very hard and empirical analysis is not straightforward because the performance of a parallel algorithm cannot be evaluated simply by executing the algorithm on a few parallel systems. Among the difficulties encountered are the noise produced by other users on the system, the limited variation in parallelism (the number of processors in the system is strictly bounded) and the waste of resources involved: most of the time, the outcomes of all computations are already known and the only issue of interest is when these outcomes are produced.We will describe a way to simulate the execution of parallel branch and bound algorithms on arbitrary parallel systems in such a way that the memory and cpu requirements are very reasonable. The use of simulation has only minor consequences for the formulation of the algorithm.     

Factoring polynomials modulo special primes

We consider the problem of factoring polynomials overGF(p) for those prime numbersp for which all prime factors ofp– 1 are small. We show that if we have a primitivet-th root of unity for every primet dividingp– 1 then factoring polynomials overGF(p) can be done in deterministic polynomial time.Research partially supported by Hungarian National Foundation for Scientific Research, Grant 1812.     

Strategies and simulations in a semantic framework

By means of several examples of structural operational semantics for a variety of languages, we justify the importance and interest of using the notions of strategies and simulations in the semantic framework provided by rewriting logic and implemented in the Maude metalanguage. On the one hand, we describe a basic strategy language for Maude and show its application to CCS, the ambient calculus, and the parallel functional language Eden. On the other hand, we show how the concept of stuttering simulation can be used inside Maude to show that a stack machine correctly implements the operational semantics of a simple functional language.     

Integrating Lucid’s Declarative Dataflow Paradigm into Object-Orientation

The dataflow language Lucid applies concepts from intensional logic to declarative ISWIM expressions which are intensionalised relative to the dimension of time, thus introducing the notion of an expression’s history. Lucian, a language derived from Lucid, embeds dataflow into object-orientation allowing the intensionalisation of objects. Lucian introduces the notion of a declarative intensional object as the history of an object’s transformations. This paper discusses the embedding relationships and semantics of conjoining the dataflow and object-oriented paradigms to provide the language Lucian for defining intensional objects.      

On the power of interaction

LetIP[f(n)] be the class of languages recognized by interactive proofs withf(¦x¦) interactions. Babai [2] showed that all languages recognized by interactive proofs with a bounded number of interactions can be recognized by interactive proofs with only two interactions; i.e., for every constantk, IP[k] collapses toIP[2].In this paper, we give evidence that interactive proofs with an unbounded number of interactions may be more powerful than interactive proofs with a bounded number of interactions. We show that for any polynomially bounded polynomial time computable functionf(n) and anyg(n)=o(f(n)) there exists an oracleB such thatIP ^B [f(n)] ₌ IP ^B [g(n)].The techniques employed are extensions of the techniques for proving lower bounds on small depth circuits used in [6], [14] and [10].Research done while in the Department of Mathematics at M. I. T. and supported by an ONR graduate fellowship.Supported in part by NSF Grant DCR MCS8509905.Research done while at the Laboratory for Computer Science at M. I. T. and Supported by an IBM fellowship.