Light types for polynomial time computation in lambda-calculus
Patrick Baillot, Kazushige Terui
备注：
20 pages (including 10 pages of appendix). (revised version; in particular section 5 has been modified). A short version is to appear in the proceedings of the conference LICS 2004 (IEEE Computer Society Press)
We propose a new 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: subject reduction is satisfied and a well-typed term admits a polynomial bound on the reduction by any strategy. We establish that as LAL, DLAL allows to represent all polytime functions. Finally we give a type inference procedure for propositional DLAL.
本文对Manzonetto博士论文中关于纯无类型代数演算的指称语义和等式/序理论的内容作了简要的总结。主要的研究成果包括：（1）从自反对象构造了一个一般的自反模型，（可能非适点）范畴;（ii）组合代数的斯通式表示定理;（iii）证明没有有效的Eudda模型可以有Euda-beta或Euda-beta-eta作为其方程理论（这可以被看作是对Honsell-Ronchi Della Rocca在1984年提出的一个开放问题的部分回答）。
We revisit the Vectorial Lambda Calculus, a typed version of Lineal. Vectorial (as well as Lineal) has been originally designed for quantum computing, as an extension to System F where linear combinations of lambda terms are also terms and linear combinations of types are also types. In its first presentation, Vectorial only provides a weakened version of the Subject Reduction property. We prove that our revised Vectorial Lambda Calculus supports the standard version of said property, answering a long standing issue. In addition we also introduce the concept of weight of types and terms, and p…
超级演绎是一种专门设计的方法，以简化谓词逻辑中一阶理论的使用。运用这一理论，以系统、正确、完整的方式，用新的演绎规则丰富演绎体系。一个证明项语言和一个切消约化已经存在于超演绎中，两者都是基于克里斯蒂安·厄本在经典微积分上的工作。然而，克里斯蒂安·厄本的微积分的计算内容与柯里-霍华德对应（Curry-Howard correspondence）没有直接关系。相反，Lambda bar mu mu波浪线演算是经典波浪线演算的一种波浪线演算。这个简短的文件是第一步，进一步探索的计算内容的superdeduction证明，我们延长了Lambda酒吧亩亩波浪演算，以获得一个proofterm语言一起削减消除减少superdeduction。我们还证明了强大的规范化，这种扩展的λ酒吧亩亩波浪演算。
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggi's monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational lambda-calculus based on Wadler's variant with unit and bind combinators, and without let. We define a notion of reduction for the calculus and prove it confluent, and also we relate our calculus to the original work by Moggi showing that his untyped metalanguage can be interpreted and simulated in our calculus. We then introduce an intersection type system inspired to Ba…
Filinski constructed a symmetric lambda-calculus consisting of expressions and continuations which are symmetric, and functions which have duality. In his calculus, functions can be encoded to expressions and continuations using primitive operators. That is, the duality of functions is not derived in the calculus but adopted as a principle of the calculus. In this paper, we propose a simple symmetric lambda-calculus corresponding to the negation-free natural deduction based bilateralism in proof-theoretic semantics. In our calculus, continuation types are represented as not negations of formul…
We study an extension of Plotkin's call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characterizations of many semantic properties. We prove that this extended calculus is a conservative refinement of Plotkin's one. In particular, the notions of solvability and potential valuability for this calculus coincide with those for Plotkin's call-by-value lambda-calculus. The proof rests on a standardization theorem proved by generalizing Takahashi'…
This paper introduces a new term rewriting system that is similar to the embedded read-back mechanism for interaction nets presented in our previous work, but is easier to follow than in the original setting and thus to analyze its properties. Namely, we verify that it correctly represents the lambda calculus. Further, we show that there is exactly one reduction sequence that starts with any term in our term rewriting system. Finally, we represent the leftmost strategy which is known to be normalizing.
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.
In this short overview, we start with the basics of quantum computing, explaining the difference between the quantum and the classical control paradigms. We give an overview of the quantum control line of research within the lambda calculus, ranging from untyped calculi up to categorical and realisability models. This is a summary of the last 10+ years of research in this area, starting from Arrighi and Dowek's seminal work until today.
在我们的论文“Uniformity and the Taylor expansion of ordinary Aldada-terms”（与Laurent Regnier合作）中，我们研究了将Aldada-terms翻译为资源Aldada-terms的无限线性组合，这是基于微分线性逻辑和微分Aldada-演算的思想，从类似于Boudol的带资源Aldada-演算的演算开始的。这个翻译的好特性是。β归约由关于资源项的相干关系保证：归一化是“线性和稳定的”（在线性逻辑的相干空间语义的意义上）WRT。这种连贯性关系。当我们考虑非确定性的或代数的扩展时，这种相干性就丧失了（代数的非确定性的扩展是非确定性的扩展，其中的项可以线性组合）。我们引入了一个“有限性结构”的资源方面，导致一个线性拓扑向量空间结构的条款，并防止出现无穷大的系数在减少，在类型设置。
We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebraic lattices via Abramsky's domain-logic approach. This provides at the same time an interpretation of the type system and a proof of the completeness of the system with respect to the continuation models by means of a filter model construction. We then define a restriction of our system, such that a lambda-mu term is typeable if and only if it is …
We introduce two extensions of the $λ$-calculus with a probabilistic choice operator, $Λ_\oplus^{cbv}$ and $Λ_\oplus^{cbn}$, modeling respectively call-by-value and call-by-name probabilistic computation. We prove that both enjoys confluence and standardization, in an extended way: we revisit these two fundamental notions to take into account the asymptotic behaviour of terms. The common root of the two calculi is a further calculus based on Linear Logic, $Λ_\oplus^!$, which allows for a fine control of the interaction between choice and copying, and which allows us to develop a unified, modul…
The infinitary lambda calculi pioneered by Kennaway et al. extend the basic lambda calculus by metric completion to infinite terms and reductions. Depending on the chosen metric, the resulting infinitary calculi exhibit different notions of strictness. To obtain infinitary normalisation and infinitary confluence properties for these calculi, Kennaway et al. extend $β$-reduction with infinitely many `$\bot$-rules', which contract meaningless terms directly to $\bot$. Three of the resulting Böhm reduction calculi have unique infinitary normal forms corresponding to Böhm-like trees. In this paper…
