A key problem in implicitcomplexity is to analyse the impact on program run times of nesting control structures, such as recursion in all finite types in functional languages or for-do statements in imperative langua...
详细信息
A key problem in implicitcomplexity is to analyse the impact on program run times of nesting control structures, such as recursion in all finite types in functional languages or for-do statements in imperative languages. Three types of programs are studied. One type of program can only use ground type recursion. Another is concerned with imperative programs: ordinary loop programs and stack programs. Programs of the third type can use higher type recursion on notation as in functional programming languages. The present approach to analysing run time yields various characterisations of FPTIME and all Grzegorczyk classes at and above the FLINSPACE level. Central to this approach is the distinction between "top recursion" and "side recursion". Top recursions are the only form of recursion which can cause an increase in complexity. Counting the depth of nested top recursions leads to several versions of "the mu-measure". In this way, various recent solutions of key problems in implicitcomplexity are integrated into a uniform approach. (c) 2004 Elsevier B.V. All rights reserved.
Light Affine Lambda Calculus is a term calculus for polynomial time computation ([12]). Some of the terms of Light Affine Lambda Calculus must however be regarded as errors. Intuitionistic Light Affine Logic (ILAL) ty...
详细信息
Light Affine Lambda Calculus is a term calculus for polynomial time computation ([12]). Some of the terms of Light Affine Lambda Calculus must however be regarded as errors. Intuitionistic Light Affine Logic (ILAL) types only terms without errors, but not all of them. We introduce two type assignment systems with intersection types : in the first one, typable pseudo-terms are exactly the terms without errors;in the second one, they are exactly those that reduce to normal terms without errors.
Two restricted imperative programming languages are considered: One is a slight modification of a loop language studied intensively in the literature, the other is a stack programming language over an arbitrary but fi...
详细信息
Two restricted imperative programming languages are considered: One is a slight modification of a loop language studied intensively in the literature, the other is a stack programming language over an arbitrary but fixed alphabet, supporting a suitable loop concept over stacks. The paper presents a purely syntactical method for analysing the impact of nesting loops on the running time. This gives rise to a uniform measure mu on both loop and stack programs, that is, a function that assigns to each such program P a natural number mu(P) computable from the syntax of P. It is shown that stack programs of mu-measure n compute exactly those functions computed by a Turing machine whose running time lies in Grzegorczyk class epsilon(ndivided by2). In particular, stack programs of mu-measure 0 compute precisely the polynomial-time computable functions. Furthermore, it is shown that loop programs of mu-measure n compute exactly the functions in epsilon(ndivided by2). In particular, loop programs of mu-measure 0 compute precisely the linear-space computable functions. (C) 2003 Elsevier B.V. All rights reserved.
作者：
Baillot, PUniv Paris 13
CNRS Lab Informat Paris Nord UMR 7030Inst Galilee F-93430 Villetaneuse France
Light Affine Logic (LAL) is a system due to Girard and Asperti capturing the complexity class P in a proof-theoretical approach based on Linear Logic. LAL provides a typing for lambda-calculus which guarantees that a ...
详细信息
Light Affine Logic (LAL) is a system due to Girard and Asperti capturing the complexity class P in a proof-theoretical approach based on Linear Logic. LAL provides a typing for lambda-calculus which guarantees that a well-typed program is executable in polynomial time on any input. We prove that the LAL type inference problem for lambda-calculus is decidable (for propositional LAL). To establish this result we reformulate the type-assignment system into an equivalent one which makes use of subtyping and is more flexible. We then use a reduction to a satisfiability problem for a system of inequations on words over a binary alphabet, for which we provide a decision procedure. (C) 2004 Elsevier B.V. All rights reserved.
An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Godel's T and therefore defines a non-siz...
详细信息
An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Godel's T and therefore defines a non-size-increasing polynomial time computable function. (C) 2003 Elsevier B.V. All rights reserved.
The implicit characterizations of the polynomial-time computable functions FP given by Bellantoni-Cook and Leivant suggest that this class is the complexity-theoretic analog of the primitive recursive functions. Hence...
详细信息
The implicit characterizations of the polynomial-time computable functions FP given by Bellantoni-Cook and Leivant suggest that this class is the complexity-theoretic analog of the primitive recursive functions. Hence, it is natural to add minimization operators to these characterizations and investigate the resulting class of partial functions as a candidate for the analog of the partial recursive functions. We do so in this paper for Cobham's definition of FP by bounded recursion and for Bellantoni-Cook's safe recursion and prove that the resulting classes capture exactly NPMV, the nondeterministic polynomial-time computable partial multifunctions. We also consider the relationship between our schemes and a notion of nondeterministic recursion defined by Leivant and show that the latter characterizes the total functions of NPMV. We view these results as giving evidence that NPMV is the appropriate analog of partial recursive. This view is reinforced by earlier results of Spreen and Stahl who show that for many of the relationships between partial recursive functions and ne. sets, analogous relationships hold between NPMV and NP sets. Furthermore, since NPMV is obtained from FP in the same way as the recursive functions are obtained from the primitive recursive functions (when defined via function schemes), this also gives further evidence that FP is properly seen as playing the role of primitive recursion. (C) 2003 Elsevier B.V. All rights reserved.
A key problem in implicit computational complexity is to analyse the impact on program run times of nesting restricted control structures, such as for-do statements in imperative languages. This problem has two aspect...
详细信息
A key problem in implicit computational complexity is to analyse the impact on program run times of nesting restricted control structures, such as for-do statements in imperative languages. This problem has two aspects. One is whether there are methods of extracting information from the syntax of such programs that give insight as to why some nesting of control structures may cause a blow up in complexity, e.g. from polynomial to (iterated) exponential time, while others do not. Bearing in mind that there are limitations to any such method, the other is whether a given method is “optimal” in the sense that it provides a full understanding of the mechanisms that cause and control the complexity of computations. This paper presents a graph theoretical analysis of control in stack programs, called “garland measure”. It is shown that (1) stack programs of garland measure n compute exactly those functions computed by a Turing machine whose running time (as a function of input size) lies in Grzegorczyk class E n+2 . In particular, stack programs of garland measure 0 compute precisely the polynomial-time computable functions. Furthermore, it is shown that the garland measure is “optimal” in the sense that no other measure on stack programs satisfying (1) can admit more algorithms at any level when restricting to “core programs” that comprise those stack manipulations which cause and control computationalcomplexity.
Minimization operators of different strengths have been studied in the framework of "predicative (safe) recursion." In this paper, a modi cation of these operators is presented. By adding the new operator to...
详细信息
Minimization operators of different strengths have been studied in the framework of "predicative (safe) recursion." In this paper, a modi cation of these operators is presented. By adding the new operator to those used by Bellantoni-Cook and Leivant to characterize the polynomial-time computable functions, one obtains a characterization of the nondeterministic polynomial-time computable multifunctions. Thus the generation of the nondeterministic polytime multifunctions from the deterministic polytime functions parallels the generation of the computable functions from the primitive recursive ones.
We give a machine-independent characterization of the class of functions bitwise computable in alternating logarithmic time, with output of polynomial size. Recall that ALogTime is the same, for decision problems, as ...
详细信息
We give a machine-independent characterization of the class of functions bitwise computable in alternating logarithmic time, with output of polynomial size. Recall that ALogTime is the same, for decision problems, as the U-E*-uniform variant of NC1 Ruzzo, J. Comput. System Sci. 22 (1981) 365-383. Our characterization is in terms of a weak form of ramified tree recurrence with substitutions. No initial functions other than basic tree operations are used, and no bounding conditions on the recurrence. (C) 2000 Elsevier Science B.V. All rights reserved.
暂无评论