Recently, Dal Lago and Gaboardi have proposed a type system, named dlPCF as a framework for implicit computational complexity. dlPCF is a non-standard type system for PCF programs which is relatively complete with res...
详细信息
Recently, Dal Lago and Gaboardi have proposed a type system, named dlPCF as a framework for implicit computational complexity. dlPCF is a non-standard type system for PCF programs which is relatively complete with respect to quantitative properties thanks to the use of linear types inspired by Bounded linear logic and dependent types a la Dependent ML. In this work, we adapt the framework of quantitative realizability and obtain a model for dlPCF. The quantitative realizability model aims at a better understanding of dlPCF type decorations and at giving an abstract semantic proof of intensional soundness. (C) 2015 Elsevier B.V. All rights reserved.
Soft type assignment systems STA, STA(+), and STA(B) characterise by means of reduction of terms computation in complexity classes PTIME, NP, and PSPACE, respectively. All these systems are inspired by linear logic an...
详细信息
Soft type assignment systems STA, STA(+), and STA(B) characterise by means of reduction of terms computation in complexity classes PTIME, NP, and PSPACE, respectively. All these systems are inspired by linear logic and include polymorphism similar to the one of System F. We show that the presence of polymorphism gives the undecidability of typechecking and type inference. We also show that reductions in decidable monomorphic versions of these systems also capture the same complexity classes in away sufficient for the traditional complexity theory. The translations we propose show in addition that the monomorphic systems to serve as a programming language require some metalanguage support since the program which operates on data has form and type which depend on the size of the input. (C) 2016 Elsevier Inc. All rights reserved.
Interpretation methods have been introduced in the 70s by Lankford [1] in rewriting theory to prove termination. Actually, as shown by Bonfante et al. [2], an interpretation of a program induces a bound on its complex...
详细信息
Interpretation methods have been introduced in the 70s by Lankford [1] in rewriting theory to prove termination. Actually, as shown by Bonfante et al. [2], an interpretation of a program induces a bound on its complexity. However, Lankford's original analysis depends deeply on the Archimedean property of natural numbers. This goes against the fact that finding a real interpretation can be solved by Tarski's decision procedure over the reals (as described by Dershowitz in [3]), and consequently interpretations are usually chosen over the reals rather than over the integers. Doing so, one cannot use anymore the (good) properties of the natural (well-)ordering of N used to bound the complexity of programs. We prove that one may take benefit from the best of both worlds: the complexity analysis still holds even with real numbers. The reason lies in a deep algebraic property of polynomials over the reals. We illustrate this by two characterizations, one of polynomial time and one of polynomial space. (C) 2015 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.
Various simplified or improved, and partly corrected well-known implicit characterizations of the complexity classes FPTIME and NC are presented. Primarily, the interest is in simplifying the required simulations of v...
详细信息
Various simplified or improved, and partly corrected well-known implicit characterizations of the complexity classes FPTIME and NC are presented. Primarily, the interest is in simplifying the required simulations of various recursion schemes in the corresponding (implicit) framework, and in developing those simulations in a more uniform way, based on a step-by-step comparison technique, thus consolidating groundwork in implicit computational complexity. (C) 2009 Elsevier Inc. All rights reserved.
We present RSLR, an implicit higher-order characterization of the class PP of those problems which can be decided in probabilistic polynomial time with error probability smaller than 1/2. Analogously, a (less implicit...
详细信息
We present RSLR, an implicit higher-order characterization of the class PP of those problems which can be decided in probabilistic polynomial time with error probability smaller than 1/2. Analogously, a (less implicit) characterization of the class BPP can be obtained. RSLR is an extension of Hofmann's SLR with a probabilistic primitive, which enjoys basic properties such as subject reduction and confluence. Polynomial time soundness of RSLR is obtained by syntactical means, as opposed to the standard literature on SLR-derived systems, which use semantics in an essential way. (C) 2014 Elsevier Inc. All rights reserved.
We define realizability semantics for Light Affine Logic (LAL) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-sound...
详细信息
We define realizability semantics for Light Affine Logic (LAL) which has the property that denotations of functions are polynomial time computable by construction of the model. This gives a new proof of polytime-soundness of LAL which is considerably simpler than the standard proof based on proof nets and is entirely semantical in nature. The model construction uses a new instance of a resource monoid;a general method for interpreting systems based on Linear Logic introduced earlier by the authors.
Clarithmetics are number theories based on computability logic. Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solutio...
详细信息
Clarithmetics are number theories based on computability logic. Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schematic version CLA11(P4)(P1,P2,P3). By tuning the three parameters P-1, P-2, P-3 in an essentially mechanical manner, one automatically obtains sound and complete theories with respect to a, wide range of target tricomplexity classes, i.e., combinations of time (set by P-3), space (set by P-2) and so called amplitude (set by P-1 complexities. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a solution from the given tricomplexity class and, furthermore, such a solution can be automatically extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a, solution from the given tricomplexity class is represented by some theorem of the system. Furthermore, through tuning the 4th parameter P-4, at the cost of sacrificing recursive axiomatizability but not simplicity or elegance, the above extensional completeness can be strengthened to intensional completeness, according to which every formula representing a problem with a solution from the given tricomplexity class is a theorem of the system. This article is published in two parts. The present Part T introduces the system and proves its completeness, while the forthcoming Part II is devoted to proving soundness.
The work is devoted to Computability logic (CoL)-the philosophical/mathematical platform and long-term project for redeveloping classical logic after replacing truth by computability in its underlying semantics. This ...
详细信息
The work is devoted to Computability logic (CoL)-the philosophical/mathematical platform and long-term project for redeveloping classical logic after replacing truth by computability in its underlying semantics. This article elaborates some basic complexity theory for the CoL framework. Then it proves soundness and completeness for the deductive system CL12 with respect to the semantics of CoL, including the version of the latter based on polynomial time computability instead of computability-in-principle. CL12 is a sequent calculus system, where the meaning of a sequent intuitively can be characterized as 'the succedent is algorithmically reducible to the antecedent', and where formulas are built from predicate letters, function letters, variables, constants, identity, negation, parallel and choice connectives and blind and choice quantifiers. A case is made that CL12 is an adequate logical basis for constructive applied theories, including complexity-oriented ones. MSC: primary: 03F50;secondary: 03D75;03D15;03D20;68Q10;68T27;68T30.
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.
暂无评论