Arrow Research search

Author name cluster

Stephen A. Cook

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

32 papers
2 author rows

Possible papers

32

FOCS Conference 2016 Conference Paper

Exponential Lower Bounds for Monotone Span Programs

  • Robert Robere
  • Toniann Pitassi
  • Benjamin Rossman
  • Stephen A. Cook

Monotone span programs are a linear-algebraic model of computation which were introduced by Karchmer and Wigderson in 1993 [1]. They are known to be equivalent to linear secret sharing schemes, and have various applications in complexity theory and cryptography. Lower bounds for monotone span programs have been difficult to obtain because they use non-monotone operations to compute monotone functions, in fact, the best known lower bounds are quasipolynomial for a function in (nonmonotone) P [2]. A fundamental open problem is to prove exponential lower bounds on monotone span program size for any explicit function. We resolve this open problem by giving exponential lower bounds on monotone span program size for a function in monotone P. This also implies the first exponential lower bounds for linear secret sharing schemes. Our result is obtained by proving exponential lower bounds using Razborov's rank method [3], a measure that is strong enough to prove lower bounds for many monotone models. As corollaries we obtain new proofs of exponential lower bounds for monotone formula size, monotone switching network size, and the first lower bounds for monotone comparator circuit size for a function in monotone P. We also obtain new polynomial degree lower bounds for Nullstellensatz refutations using an interpolation theorem of Pudlak and Sgall [4]. Finally, we obtain quasipolynomial lower bounds on the rank measure for the st-connectivity function, implying tight bounds for st-connectivity in all of the computational models mentioned above.

Details

FOCS Conference 2013 Conference Paper

Average Case Lower Bounds for Monotone Switching Networks

  • Yuval Filmus
  • Toniann Pitassi
  • Robert Robere
  • Stephen A. Cook

An approximate computation of a Boolean function by a circuit or switching network is a computation in which the function is computed correctly on the majority of the inputs (rather than on all inputs). Besides being interesting in their own right, lower bounds for approximate computation have proved useful in many sub areas of complexity theory, such as cryptography and derandomization. Lower bounds for approximate computation are also known as correlation bounds or average case hardness. In this paper, we obtain the first average case monotone depth lower bounds for a function in monotone P. We tolerate errors that are asymptotically the best possible for monotone circuits. Specifically, we prove average case exponential lower bounds on the size of monotone switching networks for the GEN function. As a corollary, we separate the monotone NC hierarchy in the case of errors -- a result which was previously only known for exact computations. Our proof extends and simplifies the Fourier analytic technique due to Potechin, and further developed by Chan and Potechin. As a corollary of our main lower bound, we prove that the communication complexity approach for monotone depth lower bounds does not naturally generalize to the average case setting.

Details

CSL Conference 2013 Conference Paper

Theories for Subexponential-size Bounded-depth Frege Proofs

  • Kaveh Ghasemloo
  • Stephen A. Cook

This paper is a contribution to our understanding of the relationship between uniform and nonuniform proof complexity. The latter studies the lengths of proofs in various propositional proof systems such as Frege and bounded-depth Frege systems, and the former studies the strength of the corresponding logical theories such as VNC1 and V0 in [Cook/Nguyen, 2010]. A superpolynomial lower bound on the length of proofs in a propositional proof system for a family of tautologies expressing a result like the pigeonhole principle implies that the result is not provable in the theory associated with the propositional proof system. We define a new class of bounded arithmetic theories n^epsilon-ioV^\infinity for epsilon < 1 and show that they correspond to complexity classes AltTime(O(1), O(n^epsilon)), uniform classes of subexponential-size bounded-depth circuits DepthSize(O(1), 2^O(n^epsilon)). To accomplish this we introduce the novel idea of using types to control the amount of composition in our bounded arithmetic theories. This allows our theories to capture complexity classes that have weaker closure properties and are not closed under composition. We show that the proofs of Sigma^B_0-theorems in our theories translate to subexponential-size bounded-depth Frege proofs. We use these theories to formalize the complexity theory result that problems in uniform NC1 circuits can be computed by uniform subexponential bounded-depth circuits in [Allender/Koucky, 2010]. We prove that our theories contain a variation of the theory VNC1 for the complexity class NC1. We formalize Buss's proof in [Buss, 1993] that the (unbalanced) Boolean Formula Evaluation problem is in NC1 and use it to prove the soundness of Frege systems. As a corollary, we obtain an alternative proof of [Filmus et al, ICALP, 2011] that polynomial-size Frege proofs can be simulated by subexponential-size bounded-depth Frege proofs. Our results can be extended to theories corresponding to other nice complexity classes inside NTimeSpace(n^O(1), n^o(1)) such as NL. This is achieved by essentially formalizing the containment NTimeSpace(n^O(1), n^o(1)) \subseteq AltTime(O(1), O(n^epsilon)) for all epsilon > 0.

Details

CSL Conference 2011 Conference Paper

A Formal Theory for the Complexity Class Associated with the Stable Marriage Problem

  • Dai Tri Man Le
  • Stephen A. Cook
  • Yuli Ye

Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and formalize them in VCC*.

Details

STOC Conference 2010 Conference Paper

Complexity theory for operators in analysis

  • Akitoshi Kawamura
  • Stephen A. Cook

We propose a new framework for discussing computational complexity of problems involving uncountably many objects, such as real numbers, sets and functions, that can be represented only through approximation. The key idea is to use a certain class of string functions, which we call regular functions, as names representing these objects. These are more expressive than infinite sequences, which served as names in prior work that formulated complexity in more restricted settings. An important advantage of using regular functions is that we can define their size in the way inspired by higher-type complexity theory. This enables us to talk about computation on regular functions whose time or space is bounded polynomially in the input size, giving rise to more general analogues of the classes P, NP, and PSPACE. We also define NP- and PSPACE-completeness under suitable many-one reductions.

Details

CSL Conference 2010 Conference Paper

Formal Theories for Linear Algebra

  • Stephen A. Cook
  • Lila Fontes

Abstract We introduce two-sorted theories in the style of [CN10] for the complexity classes ⊕ L and DET, whose complete problems include determinants over ℤ 2 and ℤ, respectively. We then describe interpretations of Soltys’ linear algebra theory LA P over arbitrary integral domains, into each of our new theories. The result shows equivalences of standard theorems of linear algebra over ℤ 2 and ℤ can be proved in the corresponding theory, but leaves open the interesting question of whether the theorems themselves can be proved.

Details

MFCS Conference 2009 Conference Paper

Branching Programs for Tree Evaluation

  • Mark Braverman
  • Stephen A. Cook
  • Pierre McKenzie
  • Rahul Santhanam
  • Dustin Wehr

Abstract The problem \(FT^{h}_{d}(k)\) consists in computing the value in [ k ] = {1, .. ., k } taken by the root of a balanced d -ary tree of height h whose internal nodes are labelled with d -ary functions on [ k ] and whose leaves are labelled with elements of [ k ]. We propose \({FT^{h}_{d}(k)}\) as a good candidate for witnessing \({\mathbf{L}} \subsetneq{\mathbf{LogDCFL}}\). We observe that the latter would follow from a proof that k -way branching programs solving \({FT^{h}_{d}(k)}\) require \(\Omega(k^{\mbox{\scriptsize unbounded function}(h)})\) size. We introduce a “state sequence” method that can match the size lower bounds on \(FT^{h}_{d}(k)\) obtained by the Nec̆iporuk method and can yield slightly better (yet still subquadratic) bounds for some nonboolean functions. Both methods yield the tight bounds Θ( k 3 ) and Θ( k 5/2 ) for deterministic and nondeterministic branching programs solving \(FT^{3}_{2}(k)\) respectively. We propose as a challenge to break the quadratic barrier inherent in the Nec̆iporuk method by adapting the state sequence method to handle \(FT^{4}_{d}(k)\).

Details

CSL Conference 2007 Conference Paper

Relativizing Small Complexity Classes and Their Theories

  • Klaus Aehlig
  • Stephen A. Cook
  • Phuong Nguyen 0001

Abstract Existing definitions of the relativizations of NC 1, L and NL do not preserve the inclusions NC 1 ⊆ L, NL ⊆ AC 1. We start by giving the first definitions that preserve them. Here for L and NL we define their relativizations using Wilson’s stack oracle model, but limit the height of the stack to a constant (instead of log( n )). We show that the collapse of any two classes in { AC 0 ( m ), TC 0, NC 1, L, NL } implies the collapse of their relativizations. Next we develop theories that characterize the relativizations of subclasses of P by modifying theories previously defined by the second two authors. A function is provably total in a theory iff it is in the corresponding relativized class. Finally we exhibit an oracle α that makes AC k ( α ) a proper hierarchy. This strengthens and clarifies the separations of the relativized theories in [Takeuti, 1995]. The idea is that a circuit whose nested depth of oracle gates is bounded by k cannot compute correctly the ( k + 1) compositions of every oracle function.

Details

FOCS Conference 1991 Conference Paper

A New Characterization of Mehlhorn's Polynomial Time Functionals (Extended Abstract)

  • Bruce M. Kapron
  • Stephen A. Cook

A. Cobham (1964) presented a machine-independent characterization of computational feasibility, via inductive definition. R. Constable (1973) was apparently the first to consider the notion of feasibility for type 2 functionals. K. Mehlhorn's (1976) study of feasible reducibilities proceeds from Constable's work. Here, a class of polytime operators is defined, using a generalization of Cobham's definition. The authors provide an affirmative answer to the question of whether there is a natural machine based definition of Mehlhorn's class. >

Details

FOCS Conference 1989 Conference Paper

Characterizations of the Basic Feasible Functionals of Finite Type (Extended Abstract)

  • Stephen A. Cook
  • Bruce M. Kapron

The authors define a simple typed while-programming language that generalizes the sort of simple language used in computability texts to define the familiar numerical computable functions and corresponds roughly to the mu -recursion of R. O. Gandy (1967). This language does not fully capture the notion of higher type computability. The authors define run times for their programs and prove that the feasible functionals of S. Cook and A. Urquhart (1988) are precisely those functionals computable by typed while-programs with run times feasibly length-bounded. The authors introduce the notion of a bounded typed loop program and prove that a finite type functional is feasible if it is computable by a bounded typed loop program. >

Details

I&C Journal 1989 Journal Article

Complexity theory of parallel time and hardware

  • Patrick W. Dymond
  • Stephen A. Cook

The parallel resources time and hardware and the complexity classes defined by them are studied using the aggregate model. The equivalence of complexity classes defined by sequential space and uniform aggregate hardware is established. Aggregate time is related to (bounded fanin) circuit depth and, similarly, aggregate hardware is related to circuit width. Interelationships between aggregate time and hardware follow as corollaries. Aggregate time is related to the sequential resource reversal. Simultaneous relationships from aggregate hardware and time to sequential space and reversal are shown (and conversely), and these are used as evidence for an “extended parallel computation thesis. ” These simultaneous relationships provide new characterizations for the simultaneous parallel complexity class NC and for the complementary class SC. The evaluation of monotone planar circuits is shown to be in NC, in fact in LOGCFL.

Details DOI

FOCS Conference 1984 Conference Paper

Log Depth Circuits for Division and Related Problems

  • Paul Beame
  • Stephen A. Cook
  • H. James Hoover

We present optimal depth Boolean circuits (depth O(log n)) for integer division, powering, and multiple products. We also show that these three problems are of equivalent uniform depth and space complexity. In addition, we describe an algorithm for testing divisibility that is optimal for both depth and space.

Details

STOC Conference 1982 Conference Paper

Bounds on the Time for Parallel RAM's to Compute Simple Functions

  • Stephen A. Cook
  • Cynthia Dwork

We prove that a parallel RAM with no write conflicts allowed requires Ω(log n) steps to compute the Boolean or of n bits stored in the first n global memory cells. We first argue that this result is subtler than it appears, and in fact the “obvious” lower bound of log 2 n steps can be beaten.

Details

STOC Conference 1975 Conference Paper

Feasibly Constructive Proofs and the Propositional Calculus (Preliminary Version)

  • Stephen A. Cook

The motivation for this work comes from two general sources. The first source is the basic open question in complexity theory of whether P equals NP (see [1] and [2]). Our approach is to try to show they are not equal, by trying to show that the set of tautologies is not in NP (of course its complement is in NP ). This is equivalent to showing that no proof system (in the general sense defined in [3]) for the tautologies is “super” in the sense that there is a short proof for every tautology. Extended resolution is an example of a powerful proof system for tautologies that can simulate most standard proof systems (see [3]). The Main Theorem (5.5) in this paper describes the power of extended resolution in a way that may provide a handle for showing it is not super. The second motivation comes from constructive mathematics. A constructive proof of, say, a statement @@@@×A must provide an effective means of finding a proof of A for each value of x, but nothing is said about how long this proof is as a function of x. If the function is exponential or super exponential, then for short values of x the length of the proof of the instance of A may exceed the number of electrons in the universe. In section 2, I introduce the system PV for number theory, and it is this system which I suggest properly formalizes the notion of a feasibly constructive proof.

Details

STOC Conference 1975 Conference Paper

Proving Assertions about Programs that Manipulate Data Structures

  • Derek C. Oppen
  • Stephen A. Cook

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.

Details

STOC Conference 1974 Conference Paper

On the Lengths of Proofs in the Propositional Calculus (Preliminary Version)

  • Stephen A. Cook
  • Robert A. Reckhow

One of the most important open questions in the field of computational complexity is the question of whether there is a polynomial time decision procedure for the classical propositional calculus. The purpose of the present paper is to study a question related to the complexity of decision procedures for the propositional calculus; namely, the complexity of proof systems for the propositional calculus. The fundamental issue here is whether there exists any proof system, and a polynomial p(n) such that every valid formula has a proof of length not exceeding p(n), where n is the length of the formula. Theorem 1 below helps establish the importance of this question. For the purposes of this theorem, we give the following definitions.

Details

STOC Conference 1972 Conference Paper

Time-Bounded Random Access Machines

  • Stephen A. Cook
  • Robert A. Reckhow

In this paper we introduce a formal model for random access computers and argue that the model is a good one to use in the theory of computational complexity. Results are proved which compare run times for recognizing sets using this model (which has a fixed program) with a stored program model and with Turing machines. The main result, theorem 3, shows the existence of a time complexity hierarchy which is finer than that of any standard abstract computer model. An Algol-like programming language is introduced which facilitates proofs of the theorems.

Details

STOC Conference 1971 Conference Paper

The Complexity of Theorem-Proving Procedures

  • Stephen A. Cook

It is shown that any recognition problem solved by a polynomial time-bounded nondeterministic Turing machine can be “reduced” to the problem of determining whether a given propositional formula is a tautology. Here “reduced” means, roughly speaking, that the first problem can be solved deterministically in polynomial time provided an oracle is available for solving the second. From this notion of reducible, polynomial degrees of difficulty are defined, and it is shown that the problem of determining tautologyhood has the same polynomial degree as the problem of determining whether the first of two given graphs is isomorphic to a subgraph of the second. Other examples are discussed. A method of measuring the complexity of proof procedures for the predicate calculus is introduced and discussed.

Details
v2026.09.13