In this article we present the implementation of an environment supporting Lévy's \emph{optimal reduction} for the $λ$-calculus \cite{Lev78} on parallel (or distributed) computing systems. In a similar approach to Lamping's one in \cite{Lamping90}, we base our work on a graph reduction technique known as \emph{directed virtual reduction} \cite{DPR97} which is actually a restriction of Danos-Regnier virtual reduction \cite{DanosRegnier93}.
The environment, which we refer to as PELCR (Parallel Environment for optimal Lambda-Calculus Reduction) relies on a strategy for directed virtual reduction, namely {\em half combustion}, which we introduce in this article. While developing PELCR we have adopted both a message aggregation technique, allowing a reduction of the communication overhead, and a fair policy for distributing dynamically originated load among processors.
We also present an experimental study demonstrating the ability of PELCR to definitely exploit parallelism intrinsic to $λ$-terms while performing the reduction. By the results we show how PELCR allows achieving up to 70/80% of the ideal speedup on last generation multiprocessor computing systems. As a last note, the software modules have been developed with the {\tt C} language and using a standard interface for message passing, i.e. MPI, thus making PELCR itself a highly portable software package.
本文对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).
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…
Here I report about the modifications of and relations between graphic lambda calculus, various formalisms which appeared under the name chemlambda and a version of directed interaction combinators. This is part of the study and experiments with the artificial chemistry chemlambda and the relations with lambda calculus or interaction combinators, as described in arXiv:2003.14332 and available from the entry page at https://chemlambda.github.io/index.html
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。这种连贯性关系。当我们考虑非确定性的或代数的扩展时，这种相干性就丧失了（代数的非确定性的扩展是非确定性的扩展，其中的项可以线性组合）。我们引入了一个“有限性结构”的资源方面，导致一个线性拓扑向量空间结构的条款，并防止出现无穷大的系数在减少，在类型设置。
