检索结果-内蒙古大学图书馆

On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchy

INFORMATION AND COMPUTATION 2015年 241卷 3-31页

作者： Baillot, Patrick Univ Lyon LIP CNRS ENS LyonInriaUCBL Lyon France

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 lambda-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 !Bk+2, where Wand Bare 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)(ni)), for i >= 1. (C) 2014 Elsevier Inc. All rights reserved.

关键词： implicit computational complexity Linear logic Lambda-calculus Polynomial time complexity Type systems

来源：评论

学校读者我要写书评

暂无评论

Realizability models for a linear dependent PCF

引用

THEORETICAL COMPUTER SCIENCE 2015年 585卷 55-70页

作者： Brunel, Alois Gaboardi, Marco Univ Paris 13 UMR CNRS 7030 LIPN F-93430 Villetaneuse France Univ Dundee Sch Comp Dundee DD1 4HN Scotland

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.

关键词： implicit computational complexity Realizability model

来源：评论

学校读者我要写书评

暂无评论

Real or natural number interpretation and their effect on complexity

引用

THEORETICAL COMPUTER SCIENCE 2015年 585卷 25-40页

作者： Bonfante, Guillaume Deloup, Florian Henrot, Antoine Univ Lorraine LORIA Nancy France Univ Toulouse 3 Toulouse IMT F-31062 Toulouse France Univ Lorraine IECN Nancy France

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.

关键词： implicit computational complexity Term rewriting Polynomial interpretation Algebraic geometry

来源：评论

学校读者我要写书评

暂无评论

A higher-order characterization of probabilistic polynomial time

引用

INFORMATION AND COMPUTATION 2015年 241卷 114-141页

作者： Dal Lago, Ugo Toldin, Paolo Parisen Univ Bologna Dipartimento Sci Informaz Equipe FOCUS INRIA Sophia Antipolis I-40127 Bologna Italy

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.

关键词： implicit computational complexity Probabilistic classes

来源：评论

学校读者我要写书评

暂无评论

On Sharing, Memoization, and Polynomial Time 32

On Sharing, Memoization, and Polynomial Time

引用

32nd International Symposium on Theoretical Aspects of Computer Science (STACS)

作者： Avanzini, Martin Dal Lago, Ugo Univ Bologna Bologna Italy INRIA Bologna Italy

ISBN: (纸本)9783939897781

We study how the adoption of an evaluation mechanism with sharing and memoization impacts the class of functions which can be computed in polynomial time. We first show how a natural cost model in which lookup for an already computed result has no cost is indeed invariant. As a corollary, we then prove that the most general notion of ramified recurrence is sound for polynomial time, this way settling an open problem in implicit computational complexity.

关键词： implicit computational complexity data-tiering polynomial time

来源：评论

学校读者我要写书评

暂无评论

Algebras and Coalgebras in the Light Affine Lambda Calculus 2015

Algebras and Coalgebras in the Light Affine Lambda Calculus

引用

20th ACM SIGPLAN International Conference on Functional Programming (ICFP)

作者： Gaboardi, Marco Pechoux, Romain Univ Dundee Dundee DD1 4HN Scotland Univ Lorraine Nancy France

ISBN: (纸本)9781450336697

Algebra and coalgebra are widely used to model data types in functional programming languages and proof assistants. Their use permits to better structure the computations and also to enhance the expressivity of a language or of a proof system. Interestingly, parametric polymorphism a la System F provides a way to encode algebras and coalgebras in strongly normalizing languages without losing the good logical properties of the calculus. Even if these encodings are sometimes unsatisfying because they provide only limited forms of algebras and coalgebras, they give insights on the expressivity of System F in terms of functions that we can program in it. With the goal of contributing to a better understanding of the expressivity of implicit computational complexity systems, we study the problem of defining algebras and coalgebras in the Light Affine Lambda Calculus, a system characterizing the complexity class FPTIME. This system limits the computational complexity of programs but it also limits the ways we can use parametric polymorphism, and in general the way we can write our programs. We show here that while the restrictions imposed by the Light Affine Lambda Calculus pose some issues to the standard System F encodings, they still permit to encode some form of algebra and coalgebra. Using the algebra encoding one can define in the Light Affine Lambda Calculus the traditional inductive types. Unfortunately, the corresponding coalgebra encoding permits only a very limited form of coinductive data types. To extend this class we study an extension of the Light Affine Lambda Calculus by distributive laws for the modality . This extension has been discussed but not studied before.

关键词： implicit computational complexity algebra and coalgebra light logics

来源：评论

学校读者我要写书评

暂无评论

A new order-theoretic characterisation of the polytime computable functions

引用

THEORETICAL COMPUTER SCIENCE 2015年 585卷 3-24页

作者： Avanzini, Martin Eguchi, Naohi Moser, Georg Univ Innsbruck Inst Comp Sci A-6020 Innsbruck Austria

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. (C) 2015 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY license.

关键词： Term rewriting complexity analysis implicit computational complexity Automation

来源：评论

学校读者我要写书评

暂无评论

ON THE SYSTEM CL12 OF COMPUTABILITY LOGIC

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2015年第3期11卷

作者： Japaridze, Giorgi Villanova Univ Dept Comp Sci Villanova PA 19085 USA

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 tune 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 Catisequetice mechanism with respect to (simultatieously) A amplitude, S space and T time computability under certain minimal conditions on the triples (A, 5, 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.

关键词： Computability logic Interactive computation implicit computational complexity Game semantics Constructive logics Efficiency logics

来源：评论

学校读者我要写书评

暂无评论

Safe recursion revisited I: Categorical semantics for lower complexity

引用

THEORETICAL COMPUTER SCIENCE 2014年 515卷 19-45页

作者： Burrell, Mike Cockett, Robin Redmond, Brian Univ Western Ontario Dept Comp Sci London ON Canada Univ Calgary Dept Comp Sci Calgary AB T2N 1N4 Canada

The objective of this paper is to prove that the initial Polo setting, with both inductive and coinductive data, is sound for polynomial size (PSIZE). Explicitly this means all programs written in Pola have their output size bounded by a polynomial in their input size. The paper describes the polarized categorical semantics for Polo and establishes the result by providing categorical models for various fragments of Polo which have explicit size bound information built into the maps. To obtain PSIZE soundness for Pola with just inductive data, the semantics in sized sets suffices. Sized sets are sets equipped with a "size map" which associates to each element a size. Size is usually just a natural number but, more generally, the size could be an element of a size rig. A polarized category consists of an opponent and a player category joined by a module. Sized sets can be used to create a polarized category by letting the opponent and module maps be bounded by polynomials while the player category consists of maps bounded by a constant. This gives a Pola setting with inductive data and immediately establishes the PSIZE soundness of the initial Polo setting. The main technical difficulty of the paper is to provide a semantics which correctly models coinductive data as well. For this "amortized" sets are introduced: these are set in which a higher-order size function is associated to each element, which given a size returns a size. This is amortized as one is concerned with the asymptotic behavior of these functions. While amortized sets have coinductive data they are not affine closed: a final step, using equivalence relations, is required to obtain a model which includes this aspect of Polo structure. While PSIZE by itself is a very weak bound it is a crucial step in establishing polynomial space (PSPACE) and polynomial time (PTIME) bounds for these settings. (C) 2013 Elsevier B.V. All rights reserved.

关键词： Categorical semantics implicit computational complexity Safe recursion

来源：评论

学校读者我要写书评

暂无评论

Linear dependent types in a call-by-value scenario

引用

SCIENCE OF COMPUTER PROGRAMMING 2014年 84卷 77-100页

作者： Dal Lago, Ugo Petit, Barbara INRIA Sophia Antipolis Bologna Italy Univ Bologna I-40126 Bologna Italy INRIA Rhone Alpes Grenoble France

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 A-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 PCF is introduced, called dlPCF(v), whose types reflect the complexity of evaluating terms in the CEK machine. dlPCF(v) 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. (C) 2013 Elsevier B.V. All rights reserved.

关键词： complexity analysis implicit computational complexity Type systems Linear logic

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：