Typed Lambda-Calculi with Sharing and Unsharing

该项目旨在开发一种基于深度推理证明理论的新方法，以有效地评估微积分。微积分是一种最小但完全表达的理论编程语言。它构成了函数式编程语言（如Haskell）的基础，并且可以应用于创建编译器以产生更快的程序。这种改进可以是有效的计算策略，也可以是语法的改变，或者两者兼而有之。Curry-Howard对应关系将演算与证明理论联系起来：类型是逻辑公式，程序是证明，计算是证明规范化（约简为行为良好的形式）。相反，对于一个给定的证明系统，我们可以问它的计算解释是什么。深度推理是证明理论的一个现代分支，其特点是在构造证明时的灵活性。这使得它能够捕获在其他证明系统中无法表达的逻辑，并产生令人惊讶的良好复杂性结果。这些结果的关键是中间规则方案，这是深度推理的核心创新，将其与相关的形式主义区分开来。该项目的基础是发现媒体使计算步骤与最佳效率相关联。共享图是使用共享和非共享的微积分计算的图形形式。共享是一个表达式的多次使用，然后只需要计算一次，从而提高效率。取消共享是一个对应的操作，它允许共享使用分部表达式。在理论上，共享图是最优有效的演算。然而，在现实世界中，管理复制的控制机制，即预言机，产生了太多的开销成本，并且它们在实践中没有使用。该项目所基于的发现是，中间规则方案使计算能够共享和不共享，如在共享图中，但除了证明本身的结构之外，不需要控制机制。该项目将开发对媒体的计算解释。最初的研究导致了原子的量子演算，第一个有共享和非共享的量子演算，以及第一个捕捉完全懒惰的量子演算，一个标准的效率概念，作为一种自然策略。该项目将在三个层面上建立在此基础上：结构、控制和测量。结构：该项目将开发直觉逻辑（与λ演算相关）深度推理中的证明规范化理论，其中中介取代了对控制机制的需求。根据原子λ演算的经验，假设证明系统通过改变证明规则的选择来自然适应不同的效率水平。控制：新的控制机制将从深度推理证明的结构中派生出来。这些将被用来实现各种有效的策略与共享和unsharing在类型的类演算和abstract machines.Measurement：该项目将使用规范化的深度推理，构建一系列的语义工具来衡量这些演算和控制机制的效率。在这里，一个单一的基础证明系统的可用性提供了一个新的和独特的机会，比较战略平等的foot.On理论方面，该项目解决了几个开放的问题，在文献中：如何衡量的效率与共享的计算演算？什么是用于共享图的全局类型系统？深度推理的计算意义是什么？在实践方面，该项目的类型化可编程演算和抽象机是实现函数式编程语言的新的有效方法的基础。

This project aims to develop a new approach to efficient evaluation in the lambda-calculus, based on deep-inference proof theory. The lambda-calculus is a minimal but fully expressive, theoretical programming language. It forms the basis of functional programming languages such as Haskell, and efficiency improvements in the lambda-calculus can be applied to create compilers that produce faster programs. Such improvements can be efficient computation strategies, or changes to the syntax, or both.The lambda-calculus is linked to proof theory by the Curry-Howard correspondence: types are logical formulas, programs are proofs, and computation is proof normalization (reduction to a well-behaved form). Conversely, for a given proof system we can ask what its computational interpretation is.Deep inference is a modern branch of proof theory characterized by its flexibility in composing proofs. This allows it to capture logics not expressible in other proof systems, and to yield surprisingly good complexity results. Key to these results is the medial rule scheme, a core innovation of deep inference that sets it apart from related formalisms. The basis of the project is the discovery that the medial enables computation steps associated with optimal efficiency.Sharing graphs are a graphical formalism for lambda-calculus computation using sharing and unsharing. Sharing is the multiple use of a single expression, which then needs to be evaluated only once, improving efficiency. Unsharing is a counterpart that enables the shared use of partial expressions. In theory, sharing graphs are optimally efficient for lambda-calculus. However, in a real-world setting, the control mechanism that manages duplication, the oracle, incurs too much overhead cost, and they are not used in practice.The discovery on which the project is based is that the medial rule scheme enables computation with sharing and unsharing, as in sharing graphs, but without the need for a control mechanism other than the structure of the proof itself.The project will develop a computational interpretation of the medial. An initial investigation led to the atomic lambda-calculus, the first typed lambda-calculus with sharing and unsharing, and the first lambda-calculus to capture full laziness, a standard notion of efficiency, as a natural strategy. The project will build on this on three levels: structure, control, and measurement.Structure: The project will develop a theory of proof normalization in deep inference for intuitionistic logic (associated with the lambda-calculus), where the medial replaces the need for a control mechanism. Based on the experience with the atomic lambda-calculus, the hypothesis is that the proof system adapts naturally to different levels of efficiency by varying the choice of proof rules.Control: New control mechanisms will be derived from the structure of deep inference proofs. These will be used to implement various efficient strategies with sharing and unsharing in typed lambda-calculi and abstract machines.Measurement: The project will use normalization in deep inference to construct a range of semantic tools to measure the efficiency of these calculi and control mechanisms. Here, the availability of a single underlying proof system provides a new and unique opportunity to compare strategies on an equal footing.On the theoretical side, the project addresses several open questions in the literature: How to measure the efficiency of lambda-calculi with sharing? What is a global type system for sharing graphs? What is the computational meaning of deep inference? On the practical side, the typed lambda-calculi and abstract machines of the project are a basis for new and efficient ways of implementing functional programming languages.