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

An arithmetic for non-size-increasing polynomial-time computation

THEORETICAL COMPUTER SCIENCE 2004年第1-2期318卷 3-27页

作者： Aehlig, K Berger, U Hoffmann, M Schwichtenberg, H Univ Munich Inst Math D-80333 Munich Germany Univ Coll Swansea Dept Comp Sci Swansea SA2 8PP W Glam Wales Univ Munich Inst Informat D-80538 Munich Germany

An arithmetical system is presented with the property that from every proof a realizing term can be extracted that is definable in a certain affine linear typed variant of Godel's T and therefore defines a non-siz... 详细信息

关键词： logic arithmetic implicit computational complexity non-size-increasing polynomial time computation realizability higher types lambda calculus

来源：评论

学校读者我要写书评

暂无评论

Bounded Combinatory Logic and lower complexity

引用

INFORMATION AND COMPUTATION 2016年 248卷 215-226页

作者： Redmond, Brian F. Grande Prairie Reg Coll Dept Comp Math & Stat Sci 10726-106 Ave Grande Prairie AB T8V 4C4 Canada

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. (C) 2016 Elsevier Inc. All rights reserved.

关键词： Combinatory Logic Stratification implicit computational complexity Polynomial time and space Soft linear logic

来源：评论

学校读者我要写书评

暂无评论

A characterization of alternating log time by ramified recurrence

引用

THEORETICAL COMPUTER SCIENCE 2000年第1-2期236卷 193-208页

作者： Leivant, D Marion, JY Indiana Univ Dept Comp Sci Bloomington IN 47405 USA Univ Nancy 2 Loria Projet Calligramme F-54506 Vandoeuvre Nancy France

We give a machine-independent characterization of the class of functions bitwise computable in alternating logarithmic time, with output of polynomial size. Recall that ALogTime is the same, for decision problems, as the U-E*-uniform variant of NC1 Ruzzo, J. Comput. System Sci. 22 (1981) 365-383. Our characterization is in terms of a weak form of ramified tree recurrence with substitutions. No initial functions other than basic tree operations are used, and no bounding conditions on the recurrence. (C) 2000 Elsevier Science B.V. All rights reserved.

关键词： alogtime alternation ramified recursion recursion with substitution parameters tree recursion implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

Certifying polynomial time and linear/polynomial space for imperative programs

引用

SIAM JOURNAL ON COMPUTING 2006年第5期35卷 1122-1147页

作者： Niggl, KH Wunderlich, H Tech Univ Ilmenau Inst Theoret Informat D-98684 Ilmenau Germany

In earlier work of Kristiansen and Niggl the polynomial-time computable functions were characterized by stack programs of mu-measure 0, and the linear-space computable functions by loop programs of mu-measure 0. Until recently, an open problem was how to extend these characterizations to programs with user-friendly basic instructions, such as assignment statements, and with mixed data structures. It is shown how to strengthen the above characterizations to imperative programs built from arbitrary basic instructions by sequencing and by if-then-else and for-do statements. These programs operate on variables, each of which may represent any data structure such as stacks, registers, trees, or graphs. The paper presents a new method of certifying "polynomial size boundedness" of such imperative programs under the natural assumption that the basic instructions used are polynomially size bounded, too. The certificate for a program P with variables among X-1,...,X-n will be an (n+1) x (n+1) matrix M(P) over the finite set {0, 1,infinity}. It is shown that certified string programs (i.e., stack programs, but with any polynomial-time computable basic instructions) exactly compute the functions in FPTIME. Accordingly, certified general loop programs (using any linear-space computable basic instructions) exactly compute the functions in FLINSPACE. Furthermore, it is shown that certified power string programs (i.e., string programs, but built from polynomial-space computable basic instructions and extended by power loop statements) exactly compute the polynomial-space computable functions in FPSPACE. In addition, examples of certified "natural" (implementations of) algorithms, such as insertion-sort or binary addition and multiplication, are given.

关键词： polynomial time linear space polynomial space static program analysis property testing implicit computational complexity imperative programming languages

来源：评论

学校读者我要写书评

暂无评论

BUILD YOUR OWN CLARITHMETIC II: SOUNDNESS

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2016年第3期12卷

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

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 soli ion 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.

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

来源：评论

学校读者我要写书评

暂无评论

On sharing, memoization, and polynomial time

引用

INFORMATION AND COMPUTATION 2018年第Part1期261卷 3-22页

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

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. (C) 2018 The Authors. Published by Elsevier Inc.

关键词： implicit computational complexity Data-tiering Polynomial time

来源：评论

学校读者我要写书评

暂无评论

Computation by interaction for space-bounded functional programming

引用

INFORMATION AND COMPUTATION 2016年 248卷 150-194页

作者： Dal Lago, Ugo Schoepp, Ulrich Univ Bologna I-40126 Bologna Italy INRIA Sophia Antipolis Nice France Univ Munich Marchioninistr 15 D-81377 Munich Germany

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. (C) 2016 Elsevier Inc. All rights reserved.

关键词： implicit computational complexity Logarithmic space Type system Geometry of interaction Functional programming

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Realizability models and implicit complexity

引用

THEORETICAL COMPUTER SCIENCE 2011年第20期412卷 2029-2047页

作者： Dal Lago, Ugo Hofmann, Martin Univ Bologna Dipartimento Sci Informaz I-40126 Bologna Italy Univ Munich Inst Informat D-8000 Munich Germany

New, simple, proofs of soundness (every representable function lies in a given complexity class) for Elementary Affine Logic, LFPL and Soft Affine Logic are presented. The proofs are obtained by instantiating a semantic framework previously introduced by the authors and based on an innovative modification of realizability. The proof is a notable simplification on the original already semantic proof of soundness for the above mentioned logical systems and programming languages. A new result made possible by the semantic framework is the addition of polymorphism and a modality to LFPL, thus allowing for an internal definition of inductive datatypes. The methodology presented proceeds by assigning both abstract resource bounds in the form of elements from a resource monoid and resource-bounded computations to proofs (respectively, programs). (C) 2010 Elsevier B.V. All rights reserved.

关键词： implicit computational complexity Realizability Linear logic

来源：评论

学校读者我要写书评

暂无评论

Minimization and NP multifunctions

引用

THEORETICAL COMPUTER SCIENCE 2004年第1-2期318卷 105-119页

作者： Danner, N Pollett, C Univ Calif Los Angeles Dept Math Los Angeles CA 90095 USA San Jose State Univ Dept Math & Comp Sci San Jose CA 95192 USA

The implicit characterizations of the polynomial-time computable functions FP given by Bellantoni-Cook and Leivant suggest that this class is the complexity-theoretic analog of the primitive recursive functions. Hence, it is natural to add minimization operators to these characterizations and investigate the resulting class of partial functions as a candidate for the analog of the partial recursive functions. We do so in this paper for Cobham's definition of FP by bounded recursion and for Bellantoni-Cook's safe recursion and prove that the resulting classes capture exactly NPMV, the nondeterministic polynomial-time computable partial multifunctions. We also consider the relationship between our schemes and a notion of nondeterministic recursion defined by Leivant and show that the latter characterizes the total functions of NPMV. We view these results as giving evidence that NPMV is the appropriate analog of partial recursive. This view is reinforced by earlier results of Spreen and Stahl who show that for many of the relationships between partial recursive functions and ne. sets, analogous relationships hold between NPMV and NP sets. Furthermore, since NPMV is obtained from FP in the same way as the recursive functions are obtained from the primitive recursive functions (when defined via function schemes), this also gives further evidence that FP is properly seen as playing the role of primitive recursion. (C) 2003 Elsevier B.V. All rights reserved.

关键词： implicit computational complexity non-deterministic partial multifunctions safe recursion minimization

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：