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

11th Annual Conference on Theory and Applications of Models of Computation (TAMC)

作者： Marion, Jean-Yves Pechoux, Romain Univ Lorraine CNRS Nancy France

ISBN: (纸本)9783319060897;9783319060880

In this paper, we propose a type system to analyze the time consumed by multi-threaded imperative programs with a shared global memory, which delineates a class of safe multi-threaded programs. We demonstrate that a safe multi-threaded program runs in polynomial time if (i) it is strongly terminating wrt a non-deterministic scheduling policy or (ii) it terminates wrt a deterministic and quiet scheduling policy. As a consequence, we also characterize the set of polynomial time functions. The type system presented is based on the fundamental notion of data tiering, which is central in implicit computational complexity. It regulates the information flow in a computation. This aspect is interesting in that the type system bears a resemblance to typed based information flow analysis and notions of non-interference. As far as we know, this is the first characterization by a type system of polynomial time multi-threaded programs.

关键词： implicit computational complexity Ptime multi-threaded imperative language non-interference type system

来源：评论

学校读者我要写书评

暂无评论

Type-Based complexity Analysis for Fork Processes

Type-Based Complexity Analysis for Fork Processes

引用

16th International Conference on Foundations of Software Science and Computation Structures (FOSSACS) Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS)

作者： Hainry, Emmanuel Marion, Jean-Yves Pechoux, Romain Univ Lorraine Nancy France LORIA Villers Les Nancy France

ISBN: (纸本)9783642370755;9783642370748

We introduce a type system for concurrent programs described as a parallel imperative language using while-loops and fork/wait instructions, in which processes do not share a global memory, in order to analyze computational complexity. The type system provides an analysis of the data-flow based both on a data ramification principle related to tiering discipline and on secure typed languages. The main result states that well-typed processes characterize exactly the set of functions computable in polynomial space under termination, confluence and lock-freedom assumptions. More precisely, each process computes in polynomial time so that the evaluation of a process may be performed in polynomial time on a parallel model of computation. Type inference of the presented analysis is decidable in linear time provided that basic operator semantics is known.

关键词： implicit computational complexity Tiering Secure Information Flow Concurrent Programming PSpace

来源：评论

学校读者我要写书评

暂无评论

POLYNOMIAL PATH ORDERS

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2013年第4期9卷

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

This paper is concerned with the complexity analysis of constructor term rewrite systems and its ramification in implicit computational complexity. We introduce a path order with multiset status, the polynomial path order POP*, that is applicable in two related, but distinct contexts. On the one hand POP* induces polynomial innermost runtime complexity and hence may serve as a syntactic, and fully automatable, method to analyse the innermost runtime complexity of term rewrite systems. On the other hand POP* provides an order-theoretic characterisation of the polytime computable functions: the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP*.

关键词： Term Rewriting complexity Analysis implicit computational complexity Automation

来源：评论

学校读者我要写书评

暂无评论

A logical basis for constructive systems

引用

JOURNAL OF LOGIC AND COMPUTATION 2012年第3期22卷 605-642页

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

The work is devoted to Computability logic (CoL)-the philosophical/mathematical platform and long-term project for redeveloping classical logic after replacing truth by computability in its underlying semantics. This article elaborates some basic complexity theory for the CoL framework. Then it proves soundness and completeness for the deductive system CL12 with respect to the semantics of CoL, including the version of the latter based on polynomial time computability instead of computability-in-principle. CL12 is a sequent calculus system, where the meaning of a sequent intuitively can be characterized as 'the succedent is algorithmically reducible to the antecedent', and where formulas are built from predicate letters, function letters, variables, constants, identity, negation, parallel and choice connectives and blind and choice quantifiers. A case is made that CL12 is an adequate logical basis for constructive applied theories, including complexity-oriented ones. MSC: primary: 03F50;secondary: 03D75;03D15;03D20;68Q10;68T27;68T30.

关键词： Computability logic interactive computation implicit computational complexity game semantics constructive logics efficiency logics

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

LINEAR DEPENDENT TYPES AND RELATIVE COMPLETENESS

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2012年第4期8卷

作者： Dal Lago, Ugo Gaboardi, Marco Univ Bologna Dipartimento Sci Informaz EPI FOCUS INRIA Sophia Antipolis I-40126 Bologna Italy Univ Bologna Dipartimento Sci Informaz Comp & Informat Sci Dept Univ PennEPI FOCUS INRIA Sophia Antipolis I-40126 Bologna Italy

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 behavior of PCF 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.

关键词： Resource Consumption Linear Logic Dependent Types implicit computational complexity Relative Completeness

来源：评论

学校读者我要写书评

暂无评论

ON CONSTRUCTOR REWRITE SYSTEMS AND THE LAMBDA-CALCULUS

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2012年第3期8卷

作者： Dal Lago, Ugo Martini, Simone Univ Bologna I-40126 Bologna Italy

We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduction can simulate each other with a linear overhead. In particular, weak call-by-value beta-reduction can be simulated by an orthogonal constructor term rewrite system in the same number of reduction steps. Conversely, each reduction in a term rewrite system can be simulated by a constant number of beta-reduction steps. This is relevant to implicit computational complexity, because the number of beta steps to normal form is polynomially related to the actual cost (that is, as performed on a Turing machine) of normalization, under weak call-by-value reduction. Orthogonal constructor term rewrite systems and lambda-calculus are thus both polynomially related to Turing machines, taking as notion of cost their natural parameters.

关键词： lambda calculus term rewriting implicit computational complexity

来源：评论

学校读者我要写书评

暂无评论

Light logics and optimal reduction: Completeness and complexity

引用

INFORMATION AND COMPUTATION 2011年第2期209卷 118-142页

作者： Baillot, Patrick Coppola, Paolo Dal Lago, Ugo Univ Lyon ENS Lyon LIP UMR CNRS ENSL INRIA UCBL 5668 F-69364 Lyon 07 France Univ Udine Dipartimento Matemat & Informat I-33100 Udine Italy Univ Bologna Dipartimento Sci Informaz I-40127 Bologna Italy Univ Paris 13 F-93430 Villetaneuse France Univ Paris 07 F-75221 Paris 05 France

Typing of lambda-terms in elementary and light affine logic (EAL and LAL, respectively) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, respectively) proof-nets admits a guaranteed polynomial (elementary, respectively) bound: on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping's algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL, respectively) typed terms, Lamping's abstract algorithm also admits a polynomial (elementary, respectively) bound. We also give a proof of its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics). (C) 2010 Elsevier Inc. All rights reserved.

关键词： Lambda calculus Linear logic Optimal reduction implicit computational complexity Proof-nets Light linear logic

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：