Search

We give recursion-theoretic characterizations of the counting class # P , the class of those functions which count the number of accepting computations of non-deterministic Turing machines working in polynomial time. Moreover, we characterize in a recursion-theoretic manner all the levels { # P k } k ∈ N of the counting hierarchy of functions FCH , which result from allowing queries to functions of the previous level, and FCH itself as a whole. This is done in the style of Bellantoni and Cook's safe recursion, and it places # P in the context of implicit computational complexity. Namely, it relates # P with the implicit characterizations of FPTIME (Bellantoni and Cook, Comput Complex 2:97–110, 1992) and FPSPACE (Oitavem, Math Log Q 54(3):317–323, 2008), by exploiting the features of the tree-recursion scheme of FPSPACE . [ABSTRACT FROM AUTHOR]

Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular, some systems allow one to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by sized types and by input/output types, with additional temporal information about communications. [ABSTRACT FROM AUTHOR]

We show how to represent polynomial time computation in an untyped version of proof-nets for elementary linear logic. This follows previous work by P. Baillot but which was developed in a typed and affine setting. We describe how these two properties can be adapted. [ABSTRACT FROM AUTHOR]

Several type systems have been proposed to statically control the time complexity of lambda-calculus programs and characterize complexity classes such as FPTIME or FEXPTIME. A first line of research stems from linear logic and restricted versions of its !-modality controlling duplication. An instance of this is light linear logic for polynomial time computation [5]. A second approach relies on the idea of tracking the size increase between input and output, and together with a restricted recursion scheme, to deduce time complexity bounds. This second approach is illustrated for instance by non-size-increasing types [8]. However, both approaches suffer from limitations. The first one, that of linear logic, has a limited intensional expressivity, that is to say some natural polynomial time programs are not typable. As to the second approach it is essentially linear, more precisely it does not allow for a non-linear use of functional arguments. In the present work we incorporate both approaches into a common type system, in order to overcome their respective constraints. The source language we consider is a lambda-calculus with data-types and iteration, that is to say a variant of Gödel's system T. Our goal is to design a system for this language allowing both to handle non-linear functional arguments and to keep a good intensional expressivity. We illustrate our methodology by choosing the system of elementary linear logic (ELL) and combining it with a system of linear size types. We discuss the expressivity of this new type system, called sEAL, and prove that it gives a characterization of the complexity classes FPTIME and 2k-FEXPTIME, for k ≥ 0. [ABSTRACT FROM AUTHOR]

We define a call-by-value variant of Gödel's system T with references, and equip it with a linear dependent type and effect system, called d ℓ T , that can estimate the time complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, in the sense that it over-approximates the complexity of executing the programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of d ℓ T . Finally, we demonstrate the usefulness of d ℓ T for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich–Levin theorem. [ABSTRACT FROM AUTHOR]

This article exhibits a series of semantic characterisations of sublinear nondeterministic complexity classes. These results fall into the general domain of logic-based approaches to complexity theory and so-called implicit computational complexity (icc), i.e., descriptions of complexity classes without reference to specific machine models. In particular, it relates strongly to icc results based on linear logic, since the semantic framework considered stems from work on the latter. Moreover, the obtained characterisations are of a geometric nature: each class is characterised by a specific action of a group by measure-preserving maps. [ABSTRACT FROM AUTHOR]

In this paper an implicit characterization of the complexity classes k - EXP and k - FEXP , for k ≥ 0 , is given, by a type assignment system for a stratified λ -calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic ( ELL ), and the hierarchy of complexity classes k - EXP is characterized by a hierarchy of types. [ABSTRACT FROM AUTHOR]

Clarithmetics are number theories based on computability logic. Formulas of these theories represent interactive computational problems, and their "truth" is under- stood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a param- eterized/schematic version CLA11P1,P2,P3 P4. By tuning the three parameters P1, P2, P3 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 P3), space (set by P2) and so called amplitude (set by P1) 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, further- more, 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 P4, 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 previous Part I has introduced the system and proved its completeness, while the present Part II is devoted to proving soundness. [ABSTRACT FROM AUTHOR]

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 a way 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. [ABSTRACT FROM AUTHOR]

When programming with sublinear space constraints one often needs to use special implementation techniques even for simple tasks, such as function composition. In this paper, we study how such implementation techniques can be supported in a functional programming language. Our approach is based on modelling computation by interaction using the Int construction of Joyal, Street & Verity. We apply this construction to a term model of a first-order programming language and use the resulting structure to derive the functional programming language intml . Intml can be understood as a programming language simplification of Stratified Bounded Affine Logic. We formulate intml by means of a type system inspired by Baillot & Terui's Dual Light Affine Logic. We show that it captures the complexity classes flogspace and nflogspace . We illustrate its expressiveness by showing how typical graph algorithms, such a test for acyclicity in undirected graphs, can be represented. [ABSTRACT FROM AUTHOR]

We introduce a stratified version of Combinatory Logic 1 in which there are two classes of terms called player and opponent such that the class of player terms is strictly contained in the class of opponent terms. We show that the system characterizes Polynomial Time in a similar way to Soft Linear Logic. With the addition of explicit “lazy” products to the player terms and various notions of distributivity, we obtain a characterization of Polynomial Space. This paper is an expanded version of the abstract presented at DICE 2013. [ABSTRACT FROM AUTHOR]

Polynomial interpretations and their generalizations like quasi-interpretations have been used in the setting of first-order functional languages to design criteria ensuring statically some complexity bounds on programs [10] . This fits in the area of implicit computational complexity, which aims at giving machine-free characterizations of complexity classes. In this paper, we extend this approach to the higher-order setting. For that we consider simply-typed term rewriting systems [35] , we define higher-order polynomial interpretations for them, and we give a criterion ensuring that a program can be executed in polynomial time. In order to obtain a criterion flexible enough to validate interesting programs using higher-order primitives, we introduce a notion of polynomial quasi-interpretations, coupled with a simple termination criterion based on linear types and path-like orders. [ABSTRACT FROM AUTHOR]

The earlier paper “Introduction to clarithmetic I” constructed an axiomatic system of arithmetic based on computability logic, and proved its soundness and extensional completeness with respect to polynomial time computability. The present paper elaborates three additional sound and complete systems in the same style and sense: one for polynomial space computability, one for elementary recursive time (and/or space) computability, and one for primitive recursive time (and/or space) computability. [ABSTRACT FROM AUTHOR]

This work completes the definition of a library which provides the basic arithmetic operations in binary finite fields as a set of functional terms with very specific features. Such a functional terms have type in Typeable Functional Assembly ( TFA ). TFA is an extension of Dual Light Affine Logic ( DLAL ). DLAL is a type assignment designed under the prescriptions of Implicit Computational Complexity (ICC), which characterises polynomial time costing computations. We plan to exploit the functional programming patterns of the terms in the library to implement cryptographic primitives whose running-time efficiency can be obtained by means of the least hand-made tuning as possible. We propose the library as a benchmark. It fixes a kind of lower bound on the difficulty of writing potentially interesting low cost programs inside languages that can express only computations with predetermined complexity. In principle, every known and future ICC compliant programming language for polynomially costing computations should supply a simplification over the encoding of the library we present, or some set of combinators of comparable interest and difficulty. We finally report on the applicative outcome that our library has and which is a reward we get by programming in the very restrictive scenario that TFA provides. The term of TFA which encodes the inversion in binary fields suggested us a variant of a known and efficient imperative implementation of the inversion itself given by Fong. Our variant, can outperform Fong's implementation of inversion on specific hardware architectures. [ABSTRACT FROM AUTHOR]

Interpretation methods are important tools in implicit computational complexity. They have been proved particularly useful to statically analyze and to limit the complexity of programs. However, most of these studies have been so far applied in the context of term rewriting systems over finite data. In this paper, we show how interpretations can also be used to study properties of lazy first-order functional programs over streams. In particular, we provide some interpretation criteria useful to ensure two kinds of stream properties: space upper bounds and input/output upper bounds . Our space upper bounds criteria ensure global and local upper bounds on the size of each output stream element expressed in terms of the maximal size of the input stream elements. The input/output upper bounds criteria consider instead the relations between the number of elements read from the input stream and the number of elements produced on the output stream. This contribution can be seen as a first step in the development of a methodology aiming at using interpretation properties to ensure space safety properties of programs working on streams. [ABSTRACT FROM AUTHOR]

Computability logic (CoL) is a long-term project for redeveloping logic on the basis of a constructive game semantics, with games seen as abstract models of interactive computational problems. Among the fragments of CoL successfully axiomatized so far is CL12 - a conservative extension of classical first-order logic, whose language augments that of classical logic with the so called choice ("constructive") sorts of quantifiers and connectives. This system has already found fruitful applications as a logical basis for constructive and complexity-bound versions of Peano arithmetic, such as arithmetics for polynomial time computability,polynomial space computability, and beyond. The present paper introduces a third, indispensable complexity measure for interactive computations termed amplitude complexity, and establishes the adequacy (soundness/completeness) of CL12 and the associated Logical Consequence mechanism with respect to (simultaneously) A amplitude, S space and T time computability under certain minimal conditions on the triples(A,S,T)of function classes. This result very substantially broadens the potential application areas of CL12, even when time and/or space complexity is the only concern. It would be sufficient to point out that, for instance, now CL12 can be reliably used as a logical basis of systems for logarithmic space or exponential time computabilities - something that the earlier-known crude adequacy results for CL12 were too weak to allow us to do. This paper is self-contained, and targets readers with no prior familiarity with the subject. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

Recently, Dal Lago and Gaboardi have proposed a type system, named d ℓ PCF as a framework for implicit computational complexity. d ℓ PCF 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 à la Dependent ML. In this work, we adapt the framework of quantitative realizability and obtain a model for d ℓ PCF . The quantitative realizability model aims at a better understanding of d ℓ PCF type decorations and at giving an abstract semantic proof of intensional soundness. [ABSTRACT FROM AUTHOR]

We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define the small polynomial path order ( sPOP ⁎ for short). This termination order entails a new syntactic method to analyse the innermost runtime complexity of term rewrite systems fully automatically: for any rewrite system compatible with sPOP ⁎ that employs recursion up to depth d , the (innermost) runtime complexity is polynomially bounded of degree d . This bound is tight. Thus we obtain a direct correspondence between a syntactic (and easily verifiable) condition of a program and the asymptotic worst-case complexity of the program. [ABSTRACT FROM AUTHOR]

Elementary linear logic is a simple variant of linear logic due to Girard and which characterizes in the proofs-as-programs approach the class of elementary functions, that is to say functions computable in time bounded by a tower of exponentials of fixed height. Other systems like light and soft linear logics have then been defined to characterize in a similar way the more interesting complexity class of polynomial time functions, but at the price of either a more complicated syntax or of more sophisticated encodings. These logical systems can serve as the basis of type systems for λ -calculus ensuring polynomial time complexity bounds on well-typed terms. This paper aims at reviving interest in elementary linear logic by showing that, despite its simplicity, it can capture smaller complexity classes than that of elementary functions. For that we carry a detailed analysis of its normalization procedure, and study the complexity of functions represented by a given type. We then show that by considering a slight variant of this system, with type fixpoints and free weakening (elementary affine logic with fixpoints) we can characterize the complexity of functions of type ! W ⊸ ! k + 2 B , where W and B are respectively types for binary words and booleans. The key point is a sharper study of the normalization bounds. We characterize in this way the class P of polynomial time predicates, and more generally the hierarchy of classes k - EXP , for k ≥ 0 , where k - EXP is the union of DTIME ( 2 k n i ) , for i ≥ 1 . [ABSTRACT FROM AUTHOR]

We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cut-elimination procedure (the so-called “light” subsystems), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a general categorical construction applicable to all models of linear logic. We thus learn that stratification may be formulated independently of exponential modalities; when it is forced to be connected to exponential modalities, it yields interesting complexity properties. In particular, from our analysis stem three alternative reformulations of Baillot and Mazza's linear logic by levels: one geometric, one interactive, and one semantic. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

We show that probabilistic computable functions, i.e., those functions outputting distributions and computed by probabilistic Turing machines, can be characterized by a natural generalization of Church and Kleene's partial recursive functions. The obtained algebra, following Leivant, can be restricted so as to capture the notion of a polytime sampleable distribution, a key concept in average-case complexity and cryptography. [ABSTRACT FROM AUTHOR]

Abstract: Linear dependent types were introduced recently (Dal Lago and Gaboardi, 2012) [26] as a formal system that allows to precisely capture both the extensional behavior and the time complexity of -terms, when the latter are evaluated by Krivine’s abstract machine. In this work, we show that the same paradigm can be applied to call-by-value computation. A system of linear dependent types for Plotkin’s is introduced, called , whose types reflect the complexity of evaluating terms in the machine. is proved to be sound, but also relatively complete: every true statement about the extensional and intentional behavior of terms can be derived, provided all true index term inequalities can be used as assumptions. [Copyright &y& Elsevier]