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

INFORMATION AND COMPUTATION 2011年第10期209卷 1312-1354页

作者： Japaridze, Giorgi Villanova Univ Dept Comp Sci Villanova PA 19085 USA Shandong Univ Sch Comp Sci & Technol Jinan 250100 Shandong Peoples R China

"Clarithmetic" is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic instead of the more traditional classical or intuitionistic logics. Formulas of clarithmetical theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Imposing various complexity constraints on such solutions yields various versions of clarithmetic. The present paper introduces a system of clarithmetic for polynomial time computability, which is shown to be sound and complete. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a polynomial time solution and, furthermore, such a solution can be efficiently extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is written in a semitutorial style and targets readers with no prior familiarity with computability logic. (C) 2011 Elsevier Inc. All rights reserved.

关键词： Computability logic Interactive computation implicit computational complexity Game semantics Peano arithmetic Bounded arithmetic

来源：评论

学校读者我要写书评

暂无评论

Linear Dependent Types and Relative Completeness

Linear Dependent Types and Relative Completeness

引用

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

作者： Dal Lago, Ugo Gaboardi, Marco Univ Bologna Dipartimento Sci Informaz I-40126 Bologna Italy INRIA Valbonne France

ISBN: (纸本)9780769544120

A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness holds in a strong sense: dlPCF is not only able to precisely capture the functional behaviour of P C F programs (i.e. how the output relates to the input) but also some of their intensional properties, namely the complexity of evaluating them with Krivine's Machine. dlPCF is designed around dependent types and linear logic and is parametrized on the underlying language of index terms, which can be tuned so as to sacrifice completeness for tractability.

关键词： implicit computational complexity lambda calculus relative completeness type systems

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Ramified Corecurrence and Logspace

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2011年 276卷 247-261页

作者： Ramyaa, Ramyaa Leivant, Daniel Indiana Univ Bloomington IN 47405 USA LORIA Nancy Villers Les Nancy France

Ramified recurrence over free algebras has been used over the last two decades to provide machine-independent characterizations of major complexity classes. We consider here ramification for the dual setting, referring to coinductive data and corecurrence rather than inductive data and recurrence. Whereas ramified recurrence is related basically to feasible time (PTime) complexity, we show here that ramified corecurrence is related fundamentally to feasible space. Indeed, the 2-tier ramified corecursive functions are precisely the functions over streams computable in logarithmic space. Here we define the complexity of computing over streams in terms of the output rather than the input, i.e. the complexity of computing the n-th entry of the output as a function of n. The class of stream functions computable in logspace seems to be of independent interest, both theoretical and practical. We show that a stream function is definable by ramified corecurrence in two tiers iff it is computable by a transducer on streams that operates in space logarithmic in the position of the output symbol being computed. A consequence is that the two-tier ramified corecursive functions over finite streams are precisely the logspace functions, in the usual sense.

关键词： Coinductive data stream automata corecurrence lazy corecurrence ramification logarithmic space implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

implicit characterizations of FPTIME and NC revisited

引用

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING 2010年第1期79卷 47-60页

作者： Niggl, Karl-Heinz Wunderlich, Henning Tech Univ Ilmenau Fak Informat & Automatisierung Inst Theoret Informat D-98684 Ilmenau Germany Univ Ulm Fak Ingenieurwissensch & Informat Inst Theoret Informat D-89069 Ulm Germany

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.

关键词： Bounded and ramified forms of recursion Function algebra implicit computational complexity NC Polynomial-time computability

来源：评论

学校读者我要写书评

暂无评论

A Semantic Proof of Polytime Soundness of Light Affine Logic

引用

THEORY OF COMPUTING SYSTEMS 2010年第4期46卷 673-689页

作者： Dal Lago, Ugo Hofmann, Martin Univ Bologna Dipartimento Sci Informaz Bologna Italy LMU Munchen Inst Informat Munich Germany

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.

关键词： implicit computational complexity Linear logic Realizability

来源：评论

学校读者我要写书评

暂无评论

Linear logic by levels and bounded time complexity

引用

THEORETICAL COMPUTER SCIENCE 2010年第2期411卷 470-503页

作者： Baillot, Patrick Mazza, Damiano Univ Paris 13 CNRS LIPN UMR 7030 F-93430 Villetaneuse France Univ Lyon ENS Lyon CNRS UMR 5668INRIAUCBLLIP Lyon France

We give a new characterization of elementary and deterministic polynomial time computation in linear logic through the proofs-as-programs correspondence. Girard's seminal results, concerning elementary and light linear logic, achieve this characterization by enforcing a stratification principle on proofs, using the notion of depth in proof nets. Here, we propose a more general form of stratification, based on inducing levels in proof nets by means of indices, which allows us to extend Girard's systems while keeping the same complexity properties. In particular, it turns out that Girard's systems can be recovered by forcing depth and level to coincide. A consequence of the higher flexibility of levels with respect to depth is the absence of boxes for handling the paragraph modality. We use this fact to propose a variant of our polytime system in which the paragraph modality is only allowed on atoms, and which may thus serve as a basis for developing lambda-calculus type assignment systems with more efficient typing algorithms than existing ones. (C) 2009 Elsevier B.V. All rights reserved.

关键词： implicit computational complexity Light linear logics Type systems for polynomial time

来源：评论

学校读者我要写书评

暂无评论

Light types for polynomial time computation in lambda calculus

引用

INFORMATION AND COMPUTATION 2009年第1期207卷 41-62页

作者： Baillot, Patrick Terui, Kazushige Univ Paris 13 CNRS UMR 7030 LIPN F-93430 Villetaneuse France Kyoto Univ Math Sci Res Inst Kyoto 6068501 Japan

We present a polymorphic type system for lambda calculus ensuring that well-typed programs can be executed in polynomial time: dual light affine logic (DLAL). DLAL has a simple type language with a linear and an intuitionistic type arrow, and one modality. It corresponds to a fragment of light affine logic (LAL). We show that contrarily to LAL, DLAL ensures good properties on lambda-terms (and not only on proof-nets): subject reduction is satisfied and a well-typed term admits a polynomial bound on the length of any of its beta reduction sequences. We also give a translation of LAL into DLAL and deduce from it that all polynomial time functions can be represented in DLAL. (c) 2008 Elsevier Inc. All rights reserved.

关键词： Linear logic Light linear logic Lambda calculus Type system implicit computational complexity Polynomial time complexity

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：