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

35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

作者： Hainry, Emmanuel Kapron, Bruce M. Marion, Jean-Yves Pechoux, Romain Univ Lorraine LORIA INRIA CNRS F-54000 Nancy France Univ Victoria Victoria BC Canada Univ Lorraine LORIA CNRS F-54000 Nancy France

ISBN: (纸本)9781450371049

The class of Basic Feasible Functionals BFF2 is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF2 based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not restrain strongly the expressive power of the language.

关键词： Feasible functionals BFF implicit computational complexity tiering type-2 type system

来源：评论

学校读者我要写书评

暂无评论

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 Path Order for Rewrite Systems that Compute Exponential Time Functions

A Path Order for Rewrite Systems that Compute Exponential Ti...

引用

22nd International Conference on Rewriting Techniques and Applications(RTA) held as part of Federated Conference on Rewriting, Deduction, and Programming (RDP)

作者： Avanzini, Martin Eguchi, Naohi Moser, Georg Univ Innsbruck Inst Comp Sci A-6020 Innsbruck Austria Japan Adv Inst Sci & Technol Sch Informat Sci Ishikawa Japan

ISBN: (纸本)9783939897309

In this paper we present a new path order for rewrite systems, the exponential path order EPO*. Suppose a term rewrite system is compatible with EPO*, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPO* equals the class of functions computable in exponential time on a Turing machine.

关键词： Runtime complexity Exponential Time Functions implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

A type system for complexity flow analysis

A type system for complexity flow analysis

引用

26th Annual IEEE Symposium on Logic in Computer Science (LICS)

作者： Marion, Jean-Yves Nancy Univ INPL ENSMN LORIA Nancy France

ISBN: (纸本)9780769544120

We propose a type system for an imperative programming language, which certifies program time bounds. This type system is based on secure flow information analysis. Each program variable has a level and we prevent information from flowing from low level to higher level variables. We also introduce a downgrading mechanism in order to delineate a broader class of programs. Thus, we propose a relation between security-typed language and implicit computational complexity. We establish a characterization of the class of polynomial time functions.

关键词： implicit computational complexity PTIME imperative information flow security types

来源：评论

学校读者我要写书评

暂无评论

Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories 32

Enumerating Error Bounded Polytime Algorithms Through Arithm...

引用

32nd EACSL Annual Conference on Computer Science Logic (CSL)

作者： Antonelli, Melissa Dal Lago, Ugo Davoli, Davide Oitavem, Isabel Pistone, Paolo Helsinki Inst Informat Technol Helsinki Finland Bologna Univ Bologna Italy Univ Cote Azur Inria Sophia Antipolis France NOVA FCT Ctr Math & Applicat NOVA Math Caparica Portugal NOVA FCT Dept Math Caparica Portugal

ISBN: (纸本)9783959773102

We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory a la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPPT and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPPT, where T = I Delta(0) + Exp is a well-studied theory based on bounded induction.

关键词： Bounded Arithmetic Randomized Computation implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

Course of value distinguishes the intentionality of programming languages

Course of value distinguishes the intentionality of programm...

引用

2nd Symposium on Information and Communication Technology, SoICT 2011

作者： Bonfante, Guillaume Université de Lorraine Nancy France

ISBN: (纸本)9781450308809

In this contribution, we propose to study the transformation of first order programs by course of value recursion. Our motivation is to show that this transformation provides a separation criterion for the intentionality of sets of programs. As an illustration, we consider two variants of the multiset path ordering, for the first, terms in recursive calls are compared with respect to the subterm property, for the second with respect to embedding. Under a quasi-interpretation, both characterize Ptime, the latter characterization being a new result. Once applied the transformation, we get respectively Ptime and Pspace thus proving that the latter set of programs contains more algorithms. © 2011 ACM.

关键词： implicit computational complexity program interpretation space and time resource evaluation theory of complexity and recursion theory of computing

来源：评论

学校读者我要写书评

暂无评论

An implicit Characterization of PSPACE

引用

ACM TRANSACTIONS ON computational LOGIC 2012年第2期13卷 18-18页

作者： Gaboardi, Marco Marion, Jean-Yves Della Rocca, Simona Ronchi Univ Bologna Dipartimento Sci Informaz INRIA Focus Team I-40127 Bologna Italy Univ Lorraine ENSMN INPL F-54506 Vandoeuvre Les Nancy France Univ Turin Dipartimento Informat I-10149 Turin Italy

We present a type system for an extension of lambda calculus with a conditional construction, named STAB, that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for Booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STA(B) is complete for PSPACE. Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.

关键词： Languages Theory Design implicit computational complexity linear logic operational semantics polynomial space type assignment

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

The Geometry of Linear Higher-Order Recursion

引用

ACM TRANSACTIONS ON computational LOGIC 2009年第2期10卷 1–38页

作者： Dal Lago, Ugo Univ Bologna Dipartimento Sci Informaz I-40127 Bologna Italy

Imposing linearity and ramification constraints allows to weaken higher-order (primitive) recursion in such a way that the class of representable functions equals the class of polynomial-time computable functions, as the works by Leivant, Hofmann, and others show. This article shows that fine-tuning these two constraints leads to different expressive strengths, some of them lying well beyond polynomial time. This is done by introducing a new semantics, called algebraic context semantics. The framework stems from Gonthier's original work (itself a model of Girard's geometry of interaction) and turns out to be a versatile and powerful tool for the quantitative analysis of normalization in the lambda calculus with constants and higher-order recursion.

关键词： Languages Performance Theory Geometry of interaction higher-order recursion implicit computational complexity lambda calculus type systems

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：