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

Two Algorithms in Search of a Type-System

THEORY OF COMPUTING SYSTEMS 2009年第4期45卷 787-821页

作者： Danner, Norman Royer, James S. Wesleyan Univ Dept Math & Comp Sci Middletown CT 06459 USA Syracuse Univ Dept Elect Engn & Comp Sci Syracuse NY 13210 USA

The authors' ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable (ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR can fairly naturally express the classic insertion-and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based formalisms. The paper's main work is in refining the original time-complexity semantics for ATR to show that these new recursion schemes do not lead out of the realm of feasibility.

关键词： Compositional semantics implicit computational complexity Higher-type computation Higher-type complexity Basic feasible functionals

来源：评论

学校读者我要写书评

暂无评论

Introduction to clarithmetic II

引用

INFORMATION AND COMPUTATION 2016年 247卷 290-312页

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

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

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

来源：评论

学校读者我要写书评

暂无评论

Introduction to clarithmetic I

引用

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

来源：评论

学校读者我要写书评

暂无评论

Higher-order interpretations and program complexity

引用

INFORMATION AND COMPUTATION 2016年 248卷 56-81页

作者： Baillot, Patrick Dal Lago, Ugo Univ Lyon 1 CNRS INRIA Ecole Normale Super LyonLab Informat Parallelism F-69622 Villeurbanne France Univ Bologna I-40126 Bologna Italy INRIA Sophia Antipolis Nice France

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

关键词： implicit computational complexity Term rewriting systems Type systems Lambda-calculus

来源：评论

学校读者我要写书评

暂无评论

implicit recursion-theoretic characterizations of counting classes

引用

ARCHIVE FOR MATHEMATICAL LOGIC 2022年第7-8期61卷 1129-1144页

作者： Dal Lago, Ugo Kahle, Reinhard Oitavem, Isabel Univ Bologna Bologna Italy INRIA Sophia Antipolis Valbonne France Univ Tubingen Carl Friedrich von Weizsacker Ctr Tubingen Germany Univ Nova Lisboa CMA FCT Caparica Portugal Univ Nova Lisboa NOVA Sch Sci & Technol CMA & DM P-2829515 Caparica Portugal

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 is an element of 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.

关键词： #P Counting hierarchy implicit computational complexity Function algebras Recursion-theoretic characterizations

来源：评论

学校读者我要写书评

暂无评论

Light linear logics with controlled weakening: Expressibility, confluent strong normalization

引用

ANNALS OF PURE AND APPLIED LOGIC 2012年第7期163卷 854-874页

作者： Kanovich, Max Queen Mary Univ London Dept Comp Sci London E1 4NS England

Starting from Girard's seminal paper on light linear logic (LLL), a number of works investigated systems derived from linear logic to capture polynomial time computation within the computation-as-cut-elimination paradigm. The original syntax of LLL is too complicated, mainly because one has to deal with sequents which do not just consist of formulas but also of 'blocks' of formulas. We circumvent the complications of 'blocks' by introducing a new modality del which is exclusively in charge of 'additive blocks'. One of the most interesting features of this purely multiplicative del is the possibility of the second-order encodings of additive connectives. The resulting system (with the traditional syntax), called Easy-LLL, is still powerful to represent any deterministic polynomial time computations in purely logical terms. Unlike the original LLL, Easy-LLL admits polynomial time strong normalization together with the Church-Rosser property, namely, cut elimination terminates in a unique way in polytime by any choice of cut reduction strategies. (c) 2011 Elsevier B.V. All rights reserved.

关键词： Light linear logic Elementary linear logic Proofs-as-programs paradigm Cut-elimination-as-computation paradigm implicit computational complexity Polynomial-time strong normalization

来源：评论

学校读者我要写书评

暂无评论

A decidable characterization of the classes between lintime and exptime

引用

INFORMATION PROCESSING LETTERS 2006年第1期97卷 36-40页

作者： Caporaso, S Univ Bari Dipartimento Informat I-70125 Bari Italy

A language is defined by closure under safe iteration and under a new form of safe diagonalization that, unlike other forms of diagonalization used in literature to define sub-recursive hierarchies, is constructive and decidable. By counting the nesting levels of these schemes, an ordinal is assigned to each program. This yields a hierarchy T-alpha (alpha < omega(omega)) that singles-out the complexity classes DTIMEF(n(cnd+e)) for all c, d, e >= 0. (c) 2005 Elsevier B.V. All rights reserved.

关键词： computational complexity implicit computational complexity theory of computation

来源：评论

学校读者我要写书评

暂无评论

Polynomial Time and Dependent Types

引用

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL 2024年第POPL期8卷 2288-2317页

作者： Atkey, Robert Univ Strathclyde 26 Richmond St Glasgow G1 1XH Lanark Scotland

We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann. Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs' resource usage, and to theoretical use as a form of synthetic computational complexity theory.

关键词： type theory implicit computational complexity linear logic

来源：评论

学校读者我要写书评

暂无评论

Soft Linear Logic and Polynomial complexity Classes

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2008年第C期205卷 67-87页

作者： Gaboardi, Marco Marion, Jean-Yves Della Rocca, Simona Ronchi Univ Torino Dipartimento Informat Corso Svizzera 185 I-10149 Turin Italy Nancy Univ ENSMN INPL F-54506 Vandoeuvre Les Nancy France Univ Torino Dipartimento Informat I-10149 Turin Italy

We describe some results inspired to Lafont's Soft Linear Logic (SLL) which is a subsystem of second-order linear logic with restricted rules for exponentials, correct and complete for polynomial time computations. SLL is the basis for the design of type assignment systems for lambda-calculus, characterizing the complexity classes PTIME, PSPACE and NPTIME. PTIME is characterized by a type assignments system where types are a proper subset of SLL formulae. The characterization consists in the fact that a well typed term can be reduced to normal form by a number of beta-reductions polynomial in its lenght, and moreover all polynomial time functions can be computed by well typed terms. PSPACE is characterized by a type assignment system obtained from the previous one, by extending the set of types by a type for booleans, and the lambda-calculus by two boolean constants and a conditional constructor. The system assigns types to terms in such a way that the evaluation of programs (closed terms of type boolean) can be performed carefully in polynomial space. Moreover all polynomial space decision problems can be computed by terms typable in this system. In order to characterize NPTIME we extend the lambda-calculus by a nondeterministic choice operator, and the system by a rule for dealing with this new term constructor.

关键词： implicit computational complexity linear logic polynomial space type assignment

来源：评论

学校读者我要写书评

暂无评论

A lexicographic path order with slow growing derivation bounds

引用

MATHEMATICAL LOGIC QUARTERLY 2009年第2期55卷 212-224页

作者： Eguchi, Naohi Kobe Univ Grad Sch Engn Nada Ku Kobe Hyogo 6578501 Japan

This paper is concerned with implicit computational complexity of the exptime computable functions. Modifying the lexicographic path order, we introduce a path order EPO. It is shown that a termination proof for a term rewriting system via EPO implies an exponential bound on the lengths of derivations. The path order EPO is designed so that every exptime function is representable as a term rewrite system compatible with EPO. (C) 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim

关键词： implicit computational complexity term rewriting termination proof

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：