waashk/dblp huggingface dataset:
narrow proofs may be spacious: separating space and width in resolution. the width of a resolution proof is the maximal number of literals in any clause of the proof. the space of a proof is the maximal number of clauses kept in memory simultaneously if the proof is only allowed to infer new clauses from clauses currently in memory. both of these measures have previously been studied and related to the resolution refutation size of unsatisfiable conjunctive normal form (cnf) formulas. also, the minimum refutation space of a formula has been proven to be at least as large as the minimum refutation width, but it has been open whether space can be separated from width or the two measures coincide asymptotically. we prove that there is a family of $k$-cnf formulas for which the refutation width in resolution is constant but the refutation space is nonconstant, thus solving a problem mentioned in several previous papers.
subtree replacement systems: a unifying theory for recursive equations, lisp, lucid and combinatory logic recent work on computation of functions defined by sets of recursive equations by cadiou [ca72], vuillemin [vu74] and downey and sethi [ds76] depends on semantic interpretations of such equations. a purely syntactic, combinatory approach yields similar results for a much wider class of sets of equations, including sets of defining equations for lisp, lucid and the combinator calculus. the application to lisp proves several conjectures of henderson and morris [hm76].
a programming language theorem which is independent of peano arithmetic strongly typed programming languages contain a natural subrecursive part consisting of programs with no loops and no explicitly recursive (circular) function definitions. for languages with polymorphic type structure, such as model, the termination of all loop-free nonrecursive programs is independent of peano arithmetic. an attempt to apply the same techniques to prove independence of the p@@@@np problem can succeed only if np complete problems have almost polynomial complexity.
new degree bounds for polynomial threshold functions. we give new upper and lower bounds on the degree of real multivariate polynomials which sign-represent boolean functions. our upper bounds for boolean formulas yield the first known subexponential time learning algorithms for formulas of superconstant depth. our lower bounds for constant-depth circuits and intersections of halfspaces are the first new degree lower bounds since 1968, improving results of minsky and papert. the lower bounds are proved constructively; we give explicit dual solutions to the necessary linear programs.
approximate max-integral-flow/min-multicut theorems. we establish several approximate max-integral-flow / min-multicut theorems. while in general this ratio can be very large, we prove strong approximation ratios in the case where the min-multicut is a constant fraction ε of the total capacity of the graph. this setting is motivated by several combinatorial and algorithmic applications. prior to this work, a general max-integral-flow / min-multicut bound was known only for the special case where the graph is a tree. we prove that, for arbitrary graphs, the max-integral-flow / min-multicut ratio is o(ε-1 log k), where k is the number of commodites; for graphs excluding a fixed subgraph as a minor (for instance, planar graphs), o(1 / ε); and, for dense graphs, o(1√ε). our proofs are constructive in the sense that we give efficient algorithms which compute either an integral flow achieving the claimed approximation ratios, or a witness that the precondition is violated.
intercalation theorems for stack languages this paper develops necessary conditions for languages to be stack generable, stack decidable, and non-erasing stack generable. the result for stack generable languages shows that the languages {an3&brvbar;n&ge; 0} and {an bn2 cn &brvbar;n&ge;0) are not stack generable. it also shows that the language {am bm2 cn &brvbar;m, n&ge1} &ugr;{am bn2 cn &brvbar;m, n&ge;1} is inherently ambiguous as a stack language. in addition, it shows that the infiniteness problem for stack generable languages is solvable. the necessary conditions for stack decidable and non-erasing stack generable languages show that {an bn2 &brvbar;n&ge;1} &ugr;{an b2n2 c&brvbar;n&ge;1} is not stack decidable and that {an bn2 &brvbar;n&ge;0}is not non-erasing stack generable. these examples show that these two families of languages are not closed under reversal. two unsolvability results are also obtained. the question of whether a stack generable language is inherently ambiguous as a stack language is undecidable. the question of whether the reversal of a non-erasing stack generable language is also non-erasing stack generable is undecidable.
compositions of n tree transducers top-down tree transductions, introduced as models of syntax-directed translations and transformational grammars in [12] and [11], are not closed under relational composition. however, closure under relational composition is not always needed; for example, in establishing closure properties of surface sets.(surface sets are tree-languages obtained as ranges of transductions.) one such closure property, whether the image of a surface set under a transduction is a surface set, remained open. in this paper, we show that transductions need not preserve surface sets. in fact, we exhibit a hierarchy of tree languages obtained by successive transductions. we do not have a good proof that the hierarchy inclusions are proper, but there are strong reasons for so suspecting. as is customary in tree automata papers, we spend some effort on notation. this time, we present a list of first-order axioms for plane (ordered) trees. the gorn-brainerd-doner representation of trees as prefix-closed sets of sequences ([5],[2],[3]) really is a representation in the sense that any (well-founded) abstract tree satisfying our axioms is isomorphic to a prefix-closed set. we then adopt rosen's notation [10] for trees in subsequent definitions. in our opinion, however, a universally acceptable notation remains to be discovered.
the pl hierarchy collapses. it is shown that the pl hierarchy plh = pl ,\bigcup\limits\, plpl ,\bigcup\limits\, plplpl ,\bigcup\limits\, \cdots$, defined in terms of the ruzzo--simon--tompa relativization, collapses to pl.
a characterization of hoare's logic for programs with pascal-like procedures this paper presents a new characterization of applicability and limitations of hoare's logic. we consider a programming language lpas consisting of nondeterministic programs with a pascal-like procedure concept and prove as our main theorem: admissible sublanguages l of lpas have a sound and relatively complete hoare logic if and only if all programs in l have regular formal call trees. moreover, we present an explicit hoare calculus for l whenever such a hoare logic exists. our theorem generalizes clarke's results on completeness and incompleteness for languages with procedures [cl 79] and improves lipton's characterization of hoare's logic which cannot deal with nondeterminism and does not provide explicit calculi [li 77].
an efficient signature scheme based on quadratic equations electronic messages, documents and checks must be authenticated by digital signatures which are not forgeable even by their recipients. the rsa system can generate and verify such signatures, but each message requires hundreds of high precision modular multiplications which can be implemented efficiently only on special purpose hardware. in this paper we propose a new signature scheme which can be easily implemented in software on microprocessors: signature generation requires one modular multiplication and one modular division, signature verification requires three modular multiplications, and the key size is comparable to that of the rsa system. the new scheme is based on the quadratic equation m &equil; s21 + ks22 (mod n), where m is the message, s1 and s2 are the signature, and k and n are the publicly known key. while we cannot prove that the security of the scheme is equivalent to factoring, all the known methods for solving this quadratic equation for arbitrary k require the extraction of square roots modulo n or the solution of similar problems which are at least as hard as factoring. a novel property of the new scheme is that legitimate users can choose k in such a way that they can sign messages even without knowing the factorization of n, and thus everyone can use the same modulus if no one knows its factorization.
elementary bounds for presburger arithmetic we consider the first-order theory whose language has as nonlogical symbols the constant symbols 0 and 1, the binary relation symbols &equil; and <, the unary function symbol &minus; and the binary function symbol + this theory of integers under addition is commonly called the 'presburger arithmetic' and is known to be decidable for truth [presburger (1929), hilbert and bernays (1968)]. we prove here that there exists a decision procedure for this theory, involving quantifier elimination, for which there is a superexponential upper bound on the size of formula produced when all variables have been eliminated.
proving assertions about programs that manipulate data structures in this paper we wish to consider the problem of proving assertions about programs that construct and alter data structures. our method will be to define a suitable assertion language l for data structures, to define a simple programming language l' for constructing and altering data structures, to give axioms and rules of inference (in the style of [hoare 1969]) which specify the effect of program segments on data structures (described by formulas in l) and finally to prove that these axioms are correct (relative to a formal definition of the semantics of l') and, in a reasonable sense, complete. thus our intention is to provide a complete theoretical framework for describing arbitrary data structures and proving assertions about programs that manipulate them.
the complexity of dynamic languages and dynamic optimization problems in this paper we offer a unifying framework for dynamic problems in terms of &ldquo;dynamic languages&rdquo;, and we discuss the complexity of these languages. in particular, many dynamic languages derived from np-complete languages can be shown to be polynomial space (p-space) complete. among these are the following: the dynamic 3-satisfiability problem, and dynamic 3-dimensional matching problem, the dynamic partition problem, the dynamic hamiltonian circuit problem, and the dynamic independent set problem. we provide a general technique for showing how to prove the p-space completeness of dynamic problems derived from np-complete problems.
a faster strongly polynominal minimum cost flow algorithm we present a new strongly polynomial algorithm for the minimum cost flow problem, based on a refinement of the edmonds-karp scaling technique. our algorithm solves the uncapacitated minimum cost flow problem as a sequence of &ogr;(n log n) shortest path problems on networks with n nodes and m arcs and runs in &ogr;(n log n(m + n log n)) steps. using a standard transformation, this approach yields an &ogr;(m log n (m + n log n)) algorithm for the capacitated minimum cost flow problem. this algorithm improves the best previous strongly polynomial algorithm due to galil and tardos, by a factor of m/n. our algorithm is even more efficient if the number of arcs with finite upper bounds, say m', is much less than m. in this case, the number of shortest path problems solved is &ogr;((m + n) log n).
communication with secrecy constraints let x, y, z be finite sets, x,y random variables uniformly distributed over x&times;y, f a function from x&times;y to z and 0&le;&egr;&le1. a person px knows x and a person py knows y and they want to exchange x and y. an eavesdropper who knows their protocol listens to their communication in order to obtain information about f(x, y). px and py want to ensure that for every value (x,y) of (x,y) the eavesdropper's a priori and a posteriori probabilities of {f(x,y)&equil;j} are &egr;-close for all j. therefore, they encrypt some of the transmitted bits. the problem is to find a protocol that minimizes the number of bits encrypted in the worst case. two kinds of protocols are considered: deterministic and randomized. for deterministic protocols it is shown that for all x,y, boolean f (|z|&equil;2) and &egr;>0, there exists a protocol that requires no more than 2&bull; log(1/&egr;) + 16 bits. an example where log(1/&egr;) &minus; 1 bits must be encrypted is given. for k valued functions (|z|&equil;k) it is shown that at most ck(&egr;) bits must be encrypted (independent of x, y and f ). the results are extended to n persons communicating over a broadcast channel. the proofs rely on results concerning partitions of k valued matrices. for randomized protocols it is shown that for all x,y boolean f, and all possible joint distributions of x,y (not only uniform), total secrecy (&egr;&equil;0) can be achieved using only two secret bits.
uniform hashing in constant time and linear space. many algorithms and data structures employing hashing have been analyzed under the uniform hashing assumption, i.e., the assumption that hash functions behave like truly random functions. starting with the discovery of universal hash functions, many researchers have studied to what extent this theoretical ideal can be realized by hash functions that do not take up too much space and can be evaluated quickly. in this paper we present an almost ideal solution to this problem: a hash function that, on any set of n inputs, behaves like a truly random function with high probability, can be evaluated in constant time on a ram, and can be stored in o(n) words, which is optimal. for many hashing schemes this is the first hash function that makes their uniform hashing analysis come true, with high probability, without incurring overhead in time or space.
low distortion embeddings for edit distance. we show that 0,1d endowed with edit distance embeds into l1 with distortion 2o(√log dlog log d). we further show efficient implementations of the embedding that yield solutions to various computational problems involving edit distance. these include sketching, communication complexity, nearest neighbor search. for all these problems, we improve upon previous bounds.
simple and efficient leader election in the full information model. in this paper, we study the leader election problem in the full information model. we show two results in this context. first, we exhibit a constructive $o(\log n)$ round protocol that is resilient against linear size coalitions. that is, our protocol is resilient against any coalition of size less then $\beta n$ for some constant (but small) value of $\beta$. second, we provide an easy, non-constructive probabilistic argument that shows the existence of $o(\log n)$ round protocol in which $\beta$ can be made as large as $\half - \epsilon$ for any positive $\epsilon$. our protocols are extremely simple.
dynamically maintaining configurations in the plane (detailed abstract) for a number of common configurations of points (lines) in the plane, we develop datastructures in which insertions and deletions of points (or lines, respectively) can be processed rapidly without sacrificing much of the efficiency of query answering of known static structures for these configurations. as a main result we establish a fully dynamic maintenance algorithm for convex hulls that can process insertions and deletions of single points in only o(log3n) steps or less per transaction, where n is the number of points currently in the set. the algorithm has several intriguing applications, including that one can &ldquo;peel&rdquo; a set of n points in only o(log3n) steps and that one can maintain two sets at a costs of only o(log3n) or less per insertion and deletion such that it never takes more than o(log2n) steps to determine whether the two sets are separable by a straight line. also efficient algorithms are obtained for dynamically maintaining the common intersection of a set of half-spaces and for dynamically maintaining the maximal elements of a set of plane points. the results are all derived by means of one master technique, which is applied repeatedly and which seems to capture an appropriate notion of &ldquo;decomposability&rdquo; for configurations.
a consistent and complete deductive system for the verification of parallel programs the semantics of a simple parallel programming language is presented in two ways: deductively, by a set of hoare-like axioms and inference rules, and operationally, by means of an interpreter. it is shown that the deductive system is consistent with the interpreter. it would be desirable to show that the deductive system is also complete with respect to the interpreter, but this is impossible since the programming language contains the natural numbers. instead it is proved that the deductive system is complete relative to a complete proof system for the natural numbers; this result is similar to cook's relative completeness for sequential programs. the deductive semantics given here is an extension of an incomplete deductive system proposed by hoare. the key difference is an additional inference rule which provides for the introduction of auxiliary variables in a program to be verified.
the lane tracing algorithm for constructing lr(k) parsers the paper presents, as far as the author is aware, the first practical general method for constructing lr(k) parsers. it has been used, without computational difficulty, to produce lr(1), lr(2) and lr(3) parsers for grammars of the size of algol.
on the cell probe complexity of membership and perfect hashing. we study two fundamental static data structure problems, membership and perfect hashing, in yao's cell probe model. the first space and bit probe optimal worst case upper bound is given for the membership problem. we also give a new efficient membership scheme where the query algorithm makes just one adaptive choice, and probes a total of three words. a lower bound shows that two word probes generally do not suffice. for minimal perfect hashing we show a tight bit probe lower bound, and give a simple scheme achieving this performance, making just one adaptive choice. linear range perfect hashing is shown to be implementable with the same number of bit probes, of which just one is adaptive. in contrast, we establish that for sufficiently sparse sets, non-adaptive perfect hashing needs exponentially more bit probes. this is the first such separation of adaptivity and non-adaptivity.
new and improved constructions of non-malleable cryptographic protocols. we present a new constant round protocol for non-malleable zero-knowledge. using this protocol as a subroutine, we obtain a new constant-round protocol for non-malleable commitments. our constructions rely on the existence of (standard) collision resistant hash functions. previous constructions either relied on the existence of trapdoor permutations and hash functions that are collision resistant against sub-exponential sized circuits, or required a super-constant number of rounds.additional results are the first construction of a non-malleable commitment scheme that is statistically hiding (with respect to opening), and the first non-malleable protocols that satisfy a strict polynomial-time simulation requirement. the latter are constructed by additionally assuming the existence of trapdoor permutations.our approach differs from the approaches taken in previous works in that we view non-malleable zero-knowledge as a building-block rather than an end goal. this gives rise to a modular construction of non-malleable commitments and results in a somewhat simpler analysis.the techniques that we use to construct our zero-knowl-edge protocol are non black-box, but are different than the non black-box techniques previously used in the context of non-malleable coin-tossing.
efficient parallel solution of linear systems the most efficient known parallel algorithms for inversion of a nonsingular n &times; n matrix a or solving a linear system ax = b over the rationals require &ogr;(log n)2 time and m(n)n0.5 processors (where m(n) is the number of processors required in order to multiply two n &times; n rational matrices in time &ogr;(log n).) furthermore, all known polylog time algorithms for those problems are unstable: they require the calculation to be done with perfect precision; otherwise they give no results at all. this paper describes parallel algorithms that have good numerical stability and remain efficient as n grows large. in particular, we describe a quadratically convergent iterative method that gives the inverse (within the relative precision 2-no(1)) of an n &times; n rational matrix a with condition &le; n0(1) in &ogr;(log n)2 time using m(n) processors. this is the optimum processor bound and the factor n0.5 improvement of known processor bounds for polylog time matrix inversion. it is the first known polylog time algorithm that is numerically stable. the algorithm relies on our method of computing an approximate inverse of a that involves &ogr;(log n) parallel steps and n2 processors. also, we give a parallel algorithm for solution of a linear system ax = b with a sparse n &times; n symmetric positive definite matrix a. if the graph g(a) (which has n vertices and has an edge for each nonzero entry of a) is s(n)-separable, then our algorithm requires only &ogr;((log n)(log s(n))2) time and |e| + m(s(n)) processors. the algorithm computes a recursive factorization of a so that the solution of any other linear system ax = b&prime; with the same matrix a requires only &ogr;(log n log s(n)) time and |e| + s(n)2 processors.
on adequate performance measures for paging. memory management is a fundamental problem in computer architecture and operating systems. we consider a two-level memory system with fast, but small cache and slow, but large main memory. the underlying theoretical problem is known as the paging problem. a sequence of requests to pages has to be served by making each requested page available in the cache. a paging strategy replaces pages in the cache with requested ones. the aim is to minimize the number of page faults that occur whenever a requested page is not in the cache.experience shows that the paging strategy least-recently-used (lru) usually achieves a factor around 2 to 3 compared to the optimum number of faults. this contrasts the theoretical worst case, in which this factor can be as large as the cache size k.one difficulty in analyzing the paging problem was the lack of an appropriate lower bound for the minimum number of page faults. we address this issue and propose a general lower bound which provides insight into the global structure of a given request sequence. in addition, we derive a characterization for the number of faults incurred by lru.we give a theoretical explanation why lru performs well in practice. we classify the set of all request sequences according to certain parameters and prove a bound on the competitive ratio of lru, which depends on them. this bound varies between 2 and k, i.e., it includes the worst-case, but explains for which sequences lru achieves constant competitive ratio. the classification is motivated from the structure of request sequences of practical applications: locality of reference and characteristic data access patterns. we argue that this structure yields values around 2 for our bound. indeed, it is between 2 and 5 in extensive practical experiments.furthermore, we study the paging problem with variable cache size, which was already considered previously. we show that this approach is not appropriate to explain the usual good performance of lru. we measure the performance of lru with the expected competitive ratio e[alg]/e[opt] and the expected performance ratio e[alg]/e[opt] in a diffuse adversary model and compare both measures. our analysis yields that the expected competitive ratio gives a misleading answer.
linear unification a unification algorithm is described which tests a set of expressions for unifiability and which requires time and space which are only linear in the size of the input.