Calibrating computational feasibility by abstraction rank
Proceedings - Symposium on Logic in Computer Science - Trang 345-354
Tóm tắt
We characterize computationally the functions provable in second order logic with set existence restricted to natural classes of first order formulas. A classification of first-order set-existence by implicational rank yields a natural hierarchy of complexity classes within the class of Kalmar-elementary functions: The functions over {0, 1}* constructively provable using set existence for formulas of implicational rank /spl les/k are precisely the functions computable in deterministic time O(exp/sub k/(n)), where exp/sub 0/=U/sub k/(/spl lambda/n.n/sup k/), and exp/sub k+1/=2(exp/sub k/)./sup 1/ In particular, set-existence for positive formulas yields exactly PTime. We thus obtain lean and natural formalisms for codifying feasible mathematics, which are expressive both in allowing second order definitions and reasoning, and in incorporating equational programming and reasoning about program convergence in a direct and uncoded style. Through a formula-as-type morphism, we also obtain a link with lambda definability, which we exhibit in the full paper: The functions over {0, 1}* definable in the polymorphic lambda calculus F/sub 2/ over a base of type of words, using first-order type-arguments of rank /spl les/k, are precisely the functions computable in deterministic time O(exp/sub k/(n))./sup 2/ The poly-time case was proved (directly) in [15].
Từ khóa
#Equations #Arithmetic #Logic #Computational complexity #Mathematics #Mathematical programming #Reasoning about programs #Calculus #Calibration #Size controlTài liệu tham khảo
10.1007/978-94-011-0820-1
troelstra, 1996, Basic proof theory
meinke, 1992, Universal algebra, Handbook of Logic in Computer Science, 189
10.1007/978-3-642-76771-5
10.1016/S0049-237X(08)70771-7
10.1007/BFb0037112
marion, 2001, Actual arithmetic and feasibility, LNCS, 2142, 115
10.1007/3-540-45500-0_9
10.1016/S0168-0072(01)00078-1
10.1007/3-540-45653-8_23
10.1007/978-94-010-0526-5_14
schwichtenberg, 2002, Feasible programs from proofs
buss, 1986, Bounded Arithmetic
prawitz, 1965, Natural Deduction
10.1017/S0305004100013463
10.2178/jsl/1190150032
10.1007/3-540-60178-3_84
10.1007/978-1-4612-2822-6_12
10.1111/j.1746-8361.1958.tb01464.x
girard, 1971, Une extension de l'interpre?tation de Go?del a? l'analyse, et son application a l'e?limination des coupures dans l'analyse et la the?orie des types, Proceedings of the Second Scandinavian Logic Symposium, 63, 10.1016/S0049-237X(08)70843-7
cobham, 1962, The intrinsic computational difficulty of functions, Proceedings of the International Conference on Logic Methodology and Philosophy of Science, 24
leivant, 1994, Higher-order logic, Handbook of Logic in Artificial Intelligence and Logic Programming Volume 2 Deduction Methodologies, 2, 230
10.1006/inco.1994.1038