# zbMATH — the first resource for mathematics

Arithmetizing uniform $$NC$$. (English) Zbl 0741.03019
The characterization of classes of polynomially bounded functions by means of bounded arithmetic is the central theme of this paper. The three concepts: 1) Boolean circuit definable, 2) (mathematically) recursion definable and 3) representable in bounded arithmetic are analyzed and compared. The paper contains many interesting results about polynomial complexity and induction in bounded arithmetic. Of particular interest is the comparison of different induction schemata for bounded arithmetic, where special emphasis is laid on a recursion schema modelling the divide and conquer technique. We shall describe some of the concepts and results in more detail:
NC describes the functions computable in polylogarithmic depth and polynomial size by families of Boolean circuits (the family has to be log-space uniform).
BL denotes a class of functions containing some basic functions (among them are lading functions) which are closed under the map operator, under composition and under polynomially bounded branching recursion; polynomially bounded branching recursion is an abstraction of the divide and conquer technique.
The first main result is that BL is equal to (logspace uniform) NC.
The second part starts with a presentation of bounded arithmetic (quantifiers are term-bounded), where different kinds of induction schemata are analyzed:\smallskip
(1)
the “usual” schema: $$\Phi(0)\land(\forall x)(\Phi(x)\to\Phi(x+1))\to(\forall x)\Phi(x)\qquad(\Phi\hbox{-IND})$$;\smallskip
(2)
$$\Phi(0)\land(\forall x)(\Phi([{1\over 2}x])\to\Phi(x))\to(\forall x)\Phi(x)\qquad(\Phi\hbox{-PIND})$$;\smallskip
(3)
$$\Phi(0)\land(\forall x)(\Phi(x)\to\Phi(x+1))\to(\forall x)\Phi(| x|)\qquad(\Phi\hbox{-LIND})$$ $$(| x|$$ is the length of the binary representation of $$x$$);\smallskip
(4)
$$\Phi(0)\land\Phi(1)\land(\forall x)(\Phi(Fh(x))\land\Phi(Bh(x))\to\Phi(x))\to(\forall x)\Phi(x)\qquad(\Phi\hbox{-DCI}$$ “divide and conquer induction”, here $$Fh$$ is a function describing a front half, $$Bh$$ a function describing a back half via the binary coding);\smallskip
(5)
$$\Phi(0)\land(\forall x)(\Phi([{1\over 2}x])\to\Phi(x))\to(\forall x)\Phi(| x|)\quad(\Phi\hbox{-LPIND})$$ (combining features of 2 and 3);\smallskip
(6)
$$\Phi(0)\land(\forall x)(\Phi(x)\to\Phi(x+1))\to(\forall x)\Phi(\| x\|)\qquad(\Phi\hbox{- LLIND})$$.\smallskip In their further application the induction schemata are restricted to instances of the form $$\Sigma^ b_ i$$ (bounded $$\Sigma_ i$$-forms). A key role play the systems $$D^ i_ 2$$, where the induction axioms are of the form DCI with instances of the form $$\Sigma^ b_ i$$. It is shown that the $$\Sigma^ b_ i$$- LPIND and $$\Sigma$$-LLIND induction axioms are derivable in $$D^ i_ 2$$. If the $$\Sigma^ b_ i$$-DCI schema is available, then $$\Sigma^ b_ i$$-LP induction, $$\Sigma^ b_ i$$-LL induction and $$\Sigma^ b_ i$$- DC induction systems are all equivalent. It is shown how arithmetical definability corresponds to the class NC (and thus to BL): Uniform NC can be defined via $$\Sigma^ b_ 1$$-DCI induction. On the other hand, $$\Sigma^ b_ 1$$-DCI induction definable functions in $$\Sigma^ b_ 1$$-form are contained in uniform NC and thus in BL. Technically the last results were obtained by complexity analysis in a bounded sequent calculus (i.e. a sequent calculus containing rules for DCI induction and bounded quantifier introduction).
Reviewer: A.Leitsch (Wien)

##### MSC:
 03D15 Complexity of computation (including implicit computational complexity) 03F30 First-order arithmetic and fragments 68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
Full Text:
##### References:
  Barrington, D.A.M.; Compton, K.; Thérien, D.; Straubing, H., Regular languages and NC1, Technical report BCCS-88-02, (1988), Boston College, Computer Science Department Chestnut Hill, MA  Barrington, D.A.M.; Immerman, N.; Straubing, H., On uniformity within NC1, (), 47-59  Bennet, J.H., On spectra, Ph.D. thesis, (1962), Princeton University · Zbl 0057.35903  Buss, S.R., Bounded arithmetic, (1986), Bibliopolis Naples  S.R. Buss, Axiomatization and conservation results for fragments of bounded arithmetic, Workshop in Logic and Computation, AMS, Contemporary Math., to appear. · Zbl 0699.03032  Clote, P., A sequential programming language for parallel complexity classes, Technical report BCCS-88-07, (November 1988), Boston College  Clote, P., A first-order theory for the parallel complexity class NC, Technical report BCCS-89-01, (November 1989), Boston College  Cobham, A., The intrinsic computational difficulty of functions, (), 24-30, Jerusalem 1964  Cook, S.A., A taxonomy of problems with fast parallel algorithms, Inform. and control, 64, 2-22, (1985) · Zbl 0575.68045  Compton, K.; Laflamme, C., A logic and an algebra for NC1, Inform. and control, 87, 241-263, (1990) · Zbl 0717.68032  Fagin, R., Generalized first-order spectra and polynomial time recognizable sets, (), 43-73  Gentzen, G., Untersuchungen über das logische schliessen, Math. Z., Math. Z., 39, 405-431, (1934) · Zbl 0010.14601  Gurevich, Y., Algebras of feasible functions, (), 210-214  Gurevich, Y.; Lewis, H.R., A logic for constant depth circuits, Inform. and comput., 61, 65-74, (1984) · Zbl 0592.94023  Immerman, N., Relational queries computable in polynomial time, Inform. and control, 68, 86-104, (1986) · Zbl 0612.68086  Immerman, N., Expressibility as a complexity measure: results and directions, (), 127-144  Immerman, N., Languages that capture complexity classes, SIAM J. comput., 16, 761-778, (1987) · Zbl 0634.68034  Jones, N.D.; Laaser, W.T., Complete problems for deterministic polynomial time, Theoret. comput. sci., 3, 105-117, (1977) · Zbl 0352.68068  Kent, C.F.; Hodgson, B.R., An arithmetical characterization of NP, Theoret. comput. sci., 21, 225-267, (1982) · Zbl 0498.03023  Krajíc̆ek, J.; Pudlák, P.; Takeuti, G., Propositional provability and models of weak arithmetic, (1990), (draft) · Zbl 0925.03211  Lind, J.C., Computing in logarithmic space, MAC technical memorandum 52, (1974), Massachusetts Institute of Technology, Project MAC  Lynch, J., Complexity classes and theories of finite models, Math. systems theory, 15, 127-144, (1982) · Zbl 0484.03020  Molzan, Expressibility and nonuniform complexity classes, SIAM J. comput., 19, 411-423, (1990) · Zbl 0698.68047  Parikh, R., Existence and feasibility in arithmetic, J. symbolic logic, 36, 494-508, (1971) · Zbl 0243.02037  Ritchie, R., Classes of predicatably computable functions, Trans. amer. math. soc., 106, 139-173, (1963) · Zbl 0107.01001  Ruzzo, W.L., On uniform circuit complexity, J. comput. system sci., 22, 365-383, (1981) · Zbl 0462.68013  Stockmeyer, L.; Vishkin, U., Simulation of parallel random access machines by circuits, SIAM J. comput., 13, 413-422, (1984) · Zbl 0533.68048  Takeuti, G., Proof theory, (1986), North-Holland Amsterdam  Vardi, M., Complexity of relational query languages, (), 137-146
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.