Arithmetizing uniform \(NC\).

*(English)*Zbl 0741.03019The 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

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.) |

##### Keywords:

polynomially bounded functions; bounded arithmetic; Boolean circuit definable; recursion definable; polynomial complexity; induction schemata; arithmetical definability; uniform NC; BL; complexity analysis in a bounded sequent calculus
PDF
BibTeX
XML
Cite

\textit{B. Allen}, Ann. Pure Appl. Logic 53, No. 1, 1--50 (1991; Zbl 0741.03019)

Full Text:
DOI

##### References:

[1] | 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 |

[2] | Barrington, D.A.M.; Immerman, N.; Straubing, H., On uniformity within NC1, (), 47-59 |

[3] | Bennet, J.H., On spectra, Ph.D. thesis, (1962), Princeton University · Zbl 0057.35903 |

[4] | Buss, S.R., Bounded arithmetic, (1986), Bibliopolis Naples |

[5] | 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 |

[6] | Clote, P., A sequential programming language for parallel complexity classes, Technical report BCCS-88-07, (November 1988), Boston College |

[7] | Clote, P., A first-order theory for the parallel complexity class NC, Technical report BCCS-89-01, (November 1989), Boston College |

[8] | Cobham, A., The intrinsic computational difficulty of functions, (), 24-30, Jerusalem 1964 |

[9] | Cook, S.A., A taxonomy of problems with fast parallel algorithms, Inform. and control, 64, 2-22, (1985) · Zbl 0575.68045 |

[10] | Compton, K.; Laflamme, C., A logic and an algebra for NC1, Inform. and control, 87, 241-263, (1990) · Zbl 0717.68032 |

[11] | Fagin, R., Generalized first-order spectra and polynomial time recognizable sets, (), 43-73 |

[12] | Gentzen, G., Untersuchungen über das logische schliessen, Math. Z., Math. Z., 39, 405-431, (1934) · Zbl 0010.14601 |

[13] | Gurevich, Y., Algebras of feasible functions, (), 210-214 |

[14] | Gurevich, Y.; Lewis, H.R., A logic for constant depth circuits, Inform. and comput., 61, 65-74, (1984) · Zbl 0592.94023 |

[15] | Immerman, N., Relational queries computable in polynomial time, Inform. and control, 68, 86-104, (1986) · Zbl 0612.68086 |

[16] | Immerman, N., Expressibility as a complexity measure: results and directions, (), 127-144 |

[17] | Immerman, N., Languages that capture complexity classes, SIAM J. comput., 16, 761-778, (1987) · Zbl 0634.68034 |

[18] | Jones, N.D.; Laaser, W.T., Complete problems for deterministic polynomial time, Theoret. comput. sci., 3, 105-117, (1977) · Zbl 0352.68068 |

[19] | Kent, C.F.; Hodgson, B.R., An arithmetical characterization of NP, Theoret. comput. sci., 21, 225-267, (1982) · Zbl 0498.03023 |

[20] | Krajíc̆ek, J.; Pudlák, P.; Takeuti, G., Propositional provability and models of weak arithmetic, (1990), (draft) · Zbl 0925.03211 |

[21] | Lind, J.C., Computing in logarithmic space, MAC technical memorandum 52, (1974), Massachusetts Institute of Technology, Project MAC |

[22] | Lynch, J., Complexity classes and theories of finite models, Math. systems theory, 15, 127-144, (1982) · Zbl 0484.03020 |

[23] | Molzan, Expressibility and nonuniform complexity classes, SIAM J. comput., 19, 411-423, (1990) · Zbl 0698.68047 |

[24] | Parikh, R., Existence and feasibility in arithmetic, J. symbolic logic, 36, 494-508, (1971) · Zbl 0243.02037 |

[25] | Ritchie, R., Classes of predicatably computable functions, Trans. amer. math. soc., 106, 139-173, (1963) · Zbl 0107.01001 |

[26] | Ruzzo, W.L., On uniform circuit complexity, J. comput. system sci., 22, 365-383, (1981) · Zbl 0462.68013 |

[27] | Stockmeyer, L.; Vishkin, U., Simulation of parallel random access machines by circuits, SIAM J. comput., 13, 413-422, (1984) · Zbl 0533.68048 |

[28] | Takeuti, G., Proof theory, (1986), North-Holland Amsterdam |

[29] | 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.