waashk/acm huggingface dataset:
sparse sets in np-p  this paper investigates the structural properties of sets in np-p and shows that the computational difficulty of lower density sets in np depends explicitly on the relations between higher deterministic and nondeterministic time-bounded complexity classes. the paper exploits the recently discovered upward separation method, which shows for example that there exist sparse sets in np-pif and only if exptime @@@@ nexptime. in addition, the paper uses relativization techniques to determine logical possibilities, limitations of these proof techniques, and, for the first time, to exhibit structural differences between relativized np and conp.  j. hartmanis v. sewelson n. immerman
the -sequence equivalence problem for dol systems is decidable  the following problem is shown to be decidable. given are homomorphisms h1 and h2 from * to * and strings 1 and 2 over such that hni( i) is a proper prefix of hn+1i ( i) for i 1, 2 and all n ≥ 0, i.e. for i 1, 2, hi generates from i an infinite string αi with prefixes hni( i) for all n ≥ 0\. test whether α1 α2. from this result easily follows the decidability of limit language equivalence (ω-equivalence) for dol systems.  karel culik tero harju
a lower bound for integer greatest common divisor computations  it is proved that no finite computation tree with operations { +, -, *, /, mod, < } can decide whether the greatest common divisor (gcd) of a and b is one, for all pairs of integers a and b. this settles a problem posed by gro"tschel et al. moreover, if the constants explicitly involved in any operation performed in the tree are restricted to be "0" and "1" (and any other constant must be computed), then we prove an (log log n) lower bound on the depth of any computation tree with operations { +, -, *, /, mod, < } that decides whether the gcd of a and b is one, for all pairs of n-bit integers a and b.  a novel technique for handling the truncation operation is implicit in the proof of this lower bound. in a companion paper, other lower bounds for a large class of problems are proved using a similar technique.  yishay mansour baruch schieber prasoon tiwari
algorithmic aspects of type inference with subtypes  we study the complexity of type inference for programming languages with subtypes. there are three language variations that effect the problem: (i) basic functions may have polymorphic or more limited types, (ii) the subtype hierarchy may be fixed or vary as a result of subtype declarations within a program, and (iii) the subtype hierarchy may be an arbitrary partial order or may have a more restricted form, such as a tree or lattice. the naive algorithm for infering a most general polymorphic type, undervariable subtype hypotheses, requires deterministic exponential time. if we fix the subtype ordering, this upper bound grows to nondeterministic exponential time. we show that it is np-hard to decide whether a lambda term has a type with respect to a fixed subtype hierarchy (involving only atomic type names). this lower bound applies to monomorphic or polymorphic languages. we give pspace upper bounds for deciding polymorphic typability if the subtype hierarchy has a lattice structure or the subtype hierarchy varies arbitrarily. we also give a polynomial time algorithm for the limited case where there are of no function constants and the type hierarchy is either variable or any fixed lattice.  patrick lincoln john c. mitchell
generalized fair termination  we present a generalization of the known fairness and equifairness notions, called @@@@-fairness, in three versions: unconditional, weak and strong. for each such version, we introduce a proof rule for the @@@@-fair termination induced by it, using well-foundedness and countable ordinals. each such rule is proved to be sound and semantically complete. we suggest directions for further research.  nissim francez dexter kozen
complete axiomatization of algorithmic properties of program schemes with bounded nondeterministic interpretations  propositional algorithmic logic pal is a propositional counterpart of algorithmic logics. it investigates properties of program connectives: begin...end, while...do, if..then..else, or .... pal supplies tools for reasoning about programs constructed from program variables by means of program connectives and about their algorithmic properties. sound rules of inference and tautologies of pal are as important in analysis of programs (e.g. verification) as tautologies of classical propositional calculus. on the other hand propositional algorithmic theories are of highest interest, since they can capture properties of data structures and also algorithmic properties of behaviours of concurrent systems.  we proved that the semantical and the syntactical consequence operations coincide (completeness property) and that the model existence theorem holds.  grazyna mirkowska
combinations of abstract domains for logic programming  abstract interpretation [7] is a systematic methodology to designstatic program analysis which has been studied extensively in the logicprogramming community, because of the potential for optimizations inlogic programming compilers and the sophistication of the analyses whichrequire conceptual support. with the emergence of efficient genericabstract interpretation algorithms for logic programming, the mainburden in building an analysis is the abstract domain which gives a safeapproximation of the concrete domain of computation. however, accurateabstract domains for logic programming are often complex because of thevariety of analyses to perform their interdependence, and the need tomaintain structural information. the purpose of this paper is to proposeconceptual and software support for the design of abstract domains. itcontains two main contributions: the notion of open product and ageneric pattern domain. the openproduct is a new way of combining abstract domainsallowing each combined domain to benefit from information from the othercomponents through the notions of queries and open operations. the openproduct is general-purpose and can be used for other programmingparadigms as well. the generic patterndomain pat (r )automatically upgrades a domain d with structuralinformation yielding a more accurate domain pat (d) without additionaldesign or implementation cost. the two contributions are orthogonal andcan be combined in various ways to obtain sophisticated domains whileimposing minimal requirements on the designer. both contributions arecharacterized theoretically and experimentally and were used to designvery complex abstract domains such as pat(oprop⊗omode⊗ops) which would be very difficult todesign otherwise. on this last domain, designers need only contributeabout 20% (about 3,400 lines) of the complete system (about 17,700lines).  agostino cortesi baudouin le charlier pascal van hentenryck
unbounded fan-in circuits and associative functions  we consider the computation of finite semigroups using unbounded fan-in circuits. there are constant-depth, polynomial size circuits for semigroup product iff the semigroup does not contain a nontrivial group as a subset. in the case that the semigroup in fact does not contain a group, then for any primitive recursive function f, circuits of size o(nf 1(n)) and constant depth exist for the semigroup product of n elements. the depth depends upon the choice of the primitive recursive function f. the circuits not only compute the semigroup product, but every prefix of the semigroup product. a consequence is that the same bounds apply for circuits computing the sum of two n-bit numbers.  ashok k. chandra steven fortune richard lipton
effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness  elementary translations between various kinds of recursive trees are presented. it is shown that trees of either finite or countably infinite branching can be effectively put into one-one correspondence with infinitely branching trees in such a way that the infinite paths of the latter correspond to the "p-abiding" infinite paths of the former. here p can be any member of a very wide class of properties of infinite paths. for many properties ??, the converse holds too. two of the applications involve (a) the formulation of large classes of highly undecidable variants of classical computational problems, and in particular, easily describable domino problems that are iii&amp;l; t;supscrpt>11-complete, and (b) the existence of a general method for proving termination of nondeterministic or concurrent programs under any reasonable notion of fairness.  david harel
finding k farthest pairs and k closest/farthest bichromatic pairs for points in the plane  we study the problem of enumerating k farthest pairs for n points in the plane and the problems of enumerating k closest/farthest bichromatic pairs of n red and n blue points in the plane. we propose a new technique for geometric enumeration problems which iteratively reduces the search space by a half and provides efficient algorithms. as applications of this technique, we develop algorithms, using higher order voronoi diagrams, for the above problems, which run in o(min{n2, n log n \\+ k4/3 log n/log1/3 k}) time and o(_n+k4/3< ;/supscrpt>/(log k)1/3+k log n) space. since, to the authors' knowledge, no nontrivial algorithms have been known for these problems, our algorithms are currently fastest when k=o(n3/2).  naoki katoh kazuo iwano
improved projection for cad's of  r 3  this paper presents an improved projection operator for the construction of cad's of r3. it is shown that, typically, it suffices to include in projection only leading coefficients (along with discriminants and resultants) rather than all coefficients. cases in which the leading coefficient alone does not suffice can be dealt with, in a sense, even more efficiently. generalizing the improved projection operator to dimension greater than three is a topic of ongoing research.  christopher w. brown
on the power of bounded concurrency i: finite automata  we investigate the descriptive succinctness of three fundamental notions for modeling concurrency: nondeterminism and pure parallelism, the two facets of alternation, and bounded cooperative concurrency, whereby a system configuration consists of a bounded number of cooperating states. our results are couched in the general framework of finite-state automata, but hold for appropriate versions of most concurrent models of computation, such as petri nets, statecharts or finite-state versions of concurrent programming languages. we exhibit exhaustive sets of upper and lower bounds on the relative succinctness of these features over * and ω, establishing that:  (1) each of the three features represents an exponential saving in succinctness of the representation, in a manner that is independent of the other two and additive with respect to them.  (2) of the three, bounded concurrency is the strongest, representing a similar exponential saving even when substituted for each of the others.  for example, we prove exponential upper and lower bounds on the simulation of deterministic concurrent automata by afas, and triple-exponential bounds on the simulation of alternating concurrent automata by dfas.  doron drusinsky david harel
lalr(k) testing is pspace-complete  the problem of testing whether or not an arbitrary context-free grammar is lalr(k) for a fixed integer k ≥ 1 (i.e. only the subject grammar is a problem parameter) is shown to be pspace-complete. the result is in contrast with testing the membership in several other easily parsed classes of grammars, such as lr(k), slr(k), lc(k) and ll(k) grammars, for which deterministic polynomial time membership tests are known. the pspace-hardness of the problem is proved using a transformation from the finite state automaton non- universality problem. a nondeterministic algorithm for constructing sets of lr(k) items leads to a polynomially space bounded algorithm for lalr(k) testing.  esko ukkonen eljas soisalon-soininen
matrix structure, polynomial arithmetic, and erasure-resilient encoding/decoding  we exploit various matrix structures to decrease the running time and memory space of the known practical deterministic schemes for erasure-resilient encoding/decoding. polynomial interpolation and multipoint evaluation enable both encoding and decoding in nearly linear time but the overhead constants are large (particularly, for interpolation), and more straightforward quadratic time algorithms prevail in practice. we propose faster algorithms. at the encoding stage, we decrease the running time per information packet from c log2 r, for a large constant c, or from r (for practical encoding) to log r. for decoding, our improvement is by the factors c and n/log n, respectively, for the input of size n. our computations do not involve polynomial interpolation. multipoint polynomial evaluation is either also avoided or is confined to decoding.  victor y. pan
metric invariants of tetrahedra via polynomial elimination  we use grobner bases and the pedersen-roy-szpirglas real solution counting method to analyze systems of algebraic equations satisfied by metric invariants of the tetrahedron. the transformation from the geometric to the algebraic setting is effected using the cayley-menger determinant formula for the volume of a simplex. we prove that, in general, the four face areas, circumradius and volume together do not uniquely determine a tetrahedron, and that there exist non-regular tetrahedra that are uniquely determined just by the four face areas and circumradius. this settles two open problems posed by the american mathematical monthly in 1999.  petr lisonek robert b. israel
probabilistic checking of proofs: a new characterization of np  we give a new characterization of np: the class np contains exactly those languages l for which membership proofs (a proof that an input x is in l) can be verified probabilistically in polynomial time using logarithmic number of random bits and by reading sublogarithmic number of bits from the proof.  we discuss implications of this characterization; specifically, we show that approximating clique and independent set, even in a very weak sense, is np- hard.  sanjeev arora shmuel safra
on finding the exact solution of a zero-one knapsack problem  given a 0-1 knapsack problem with input drawn from a certain probability distribution, we show that for every ε > 0, there is a self-checking polynomial- time algorithm that finds an optimal solution with probability at least 1 -ε. we also prove some upper and lower bounds on random variables related to the problem.  a. v. goldberg a. marchetti-spaccamela
strong normalizability for the combined system of the typed lmbda calculus and an arbitrary convergent term rewrite system  we give a proof of strong normalizability of the typed λ-calculus extended by an arbitrary convergent term rewriting system, which provides the affirmative answer to the open problem proposed in breazu-tannen [1]. klop [6] showed that a combined system of the untyped λ-calculus and convergent term rewriting system is not church-rosser in general, though both are church-rosser. it is well- known that the typed λ-calculus is convergent (church-rosser and terminating). breazu-tannen [1] showed that a combined system of the typed λ-calculus and an arbitrary church-rosser term rewriting system is again church-rosser. our strong normalization result in this paper shows that the combined system of the typed λ-calculus and an arbitrary convergent term rewriting system is again convergent. our strong normalizability proof is easily extended to the case of the second order (polymorphically) typed lambda calculus and the case in which μ-reduction rule is added.  m. okada
asymptomatic conditional probabilities for first-order logic  motivated by problems that arise in computing degrees of belief, we consider the problem of computing asymptotic conditional probabilities for first-order formulas. that is, given first-order formulas and , we consider the number of structures with domain {1,…,n} that satisfy , and compute the fraction of them in which is true. we then consider what happens to this probability of first- order formulas, except that now we are considering asymptotic conditional probabilities. although work has been done on special cases of asymptotic conditional probabilities, no general theory has been developed. this is probably due in part to the fact that it has been known that, if there is a binary predicate symbol in the vocabulary, asymptotic conditional probabilities do not always exist. we show that in this general case, almost all the questions one might want to ask (such as deciding whether the asymptotic probability exists) are highly undecidable. on the other hand, we show that the situation with unary predicates only is much better. if the vocabulary consists only of unary predicate and constant symbols, it is decidable whether the limit exists, and if it does, there is an effective algorithm for computing it. the complexity depends on two parameters: whether there is a fixed finite vocabulary or an infinite one, and whether there is a bound on the depth of quantifier nesting.  adam j. grove joseph y. halpern daphne koller
a trivial knot whose spanning disks have exponential size  if a closed curve in space is a trivial knot (intuitively, one can untie it without cutting) then it is the boundary of some disk with no self- intersections. in this paper we investigate the minimum number of faces of a polyhedral spanning disk of a polygonal knot with n segments. we exhibit a knot whose minimal spanning disk has exp(cn) faces, for some positive constant c.  jack snoeyink
abstract continuations: a mathematical semantics for handling full jumps  continuation semantics is the traditional mathematical formalism for specifying the semantics of non-local control operations. modern lisp-style languages, however, contain advanced control structures like full functional jumps and control delimiters for which continuation semantics is insufficient. we solve this problem by introducing an abstract domain of rests of computations with appropriate operations. beyond being useful for the problem at hand, these abstract continuations turn out to have applications in a much broader context, e.g., the explication of parallelism, the modeling of control facilities in parallel languages, and the design of new control structures.  matthias felleisen mitch wand daniel friedman bruce duba
completeness and incompleteness of trace-based network proof systems  most trace-based proof systems for networks of processes are known to be incomplete. extensions to achieve completeness are generally complicated and cumbersome. in this paper, a simple trace logic is defined and two examples are presented to show its inherent incompleteness. surprisingly, both examples consist of only one process, indicating that network composition is not a cause of incompleteness. axioms necessary and sufficient for the relative completeness of a trace logic are then presented.  j. widom d. gries f. b. schneider
factorization in  zx : the searching phase  in this paper we describe ideas used to accelerate the searching phase of the berlekamp---zassenhaus algorithm, the algorithm most widely used for computing factorizations in z[x]. our ideas do not alter the theoretical worst-case complexity, but they do have a significant effect in practice: especially in those cases where the cost of the searching phase completely dominates the rest of the algorithm. a complete implementation of the ideas in this paper is publicly available in the library ntl [16]. we give timings of this implementation on some difficult factorization problems.  john abbott victor shoup paul zimmermann
time-space tradeoffs for some algebraic problems  we study the time- space relationship of several algebraic problems such as matrix multiplication and matrix inversion. several results relating the algebraic properties of a set of functions to the structure of the graph of any straight-line program, that computes this set, are shown. some of our results are the following. multiplying m × n by n × p matrices with space s requires at least time t ≥ Ω(mnp/s). inverting an n × n matrix with space s requires at least time t ≥ Ω(n4/s).  joseph ja'ja'
maps and descendant husband trees (abstract only)  map is an acronym for matching and permutation. a map is a finite set in which each member, x, has a spouse and a successor. the spouse function is a matching and the successor function is a permutation. the only tabulation required to describe a map is the successor function. the only primitive structure change is a successor swap. maps are efficient hosts to many data structures, including linked lists, trees, forests and digraphs. in each guest, each member, relation or operation is represented by a few members, relations or successor swaps in the host. a descendant husband tree, an example of a map, implements a binary tree, using only one pointer per mode. left-child, right-child and mother are computable in a few steps. insertion or deletion of a subtree is accomplished with a few successor swaps. preorder traversal of a tree requires only two steps per node visited and no auxiliary storage.  don morrison
iterated pushdown automata and complexity classes  an iterated pushdown is a pushdown of pushdowns of ... of pushdowns. an iterated exponential function is 2 to the 2 to the ... to the 2 to some polynomial. the main result is that nondeterministic 2-way and multi-head iterated pushdown automata characterize deterministic iterated exponential time complexity classes. this is proved by investigating both nondeterministic and alternating auxiliary iterated pushdown automata, for which similar characterization results are given. in particular it is shown that alternation corresponds to one more iteration of pushdowns. these results are applied to the 1-way iterated pushdown automata: (1) they form a proper hierarchy with respect to the number of iterations, (2) their emptiness problem is complete in deterministic iterated exponential time.  joost engelfriet
a unified approach to approximating resource allocation and scheduling we present a general framework for solving resource allocation and scheduling problems. given a resource of fixed size, we present algorithms that approximate the maximum throughput or the minimum loss by a constant factor. our approximation factors apply to many problems, among which are: (i) real- time scheduling of jobs on parallel machines, (ii) bandwidth allocation for sessions between two endpoints, (iii) general caching, (iv) dynamic storage allocation, and (v) bandwidth allocation on optical line and ring topologies. for some of these problems we provide the first constant factor approximation algorithm. our algorithms are simple and efficient and are based on the local- ratio technique. we note that they can equivalently be interpreted within the primal-dual schema. amotz bar-noy reuven bar-yehuda ari freund joseph (seffi) naor baruch schieber