Studying resource-limited computation from a semantic angle, utilising the differential lambda-calculus along with quantitative semantics

利用微分 lambda 演算和定量语义，从语义角度研究资源有限计算

• 批准号: 1893511
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2017
• 资助国家: 英国
• 起止时间: 2017 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-1893511
• 关键词: Studying; resource; limited; computation; semantic

This project falls within the EPSRC Theoretical Computer Science research area, under the Mathematical Sciences research theme. As stated in the title, this project will focus upon utilising the differential lambda calculus' inherent resource-sensitivity to study resource-limited computation from a semantic angle. A highly promising approach is to use quantitative semantics to interpret these computations. We interpret types as vector spaces, addition as superposition of atomic states, and scalars as a measure of a superposition. Thus we may represent programs as power series, where programs that use their input exactly once are represented as linear functions. This semantic approach allows us to model properties such as run times and resource usage of programs. Examples of state-of-the-art work in this field include models of probabilistic programs and quantum programs. Some time earlier, Ehrhard developed a model of the differential lambda-calculus via quantitative semantics. Unfortunately, this model cannot interpret fixed-point operators, and therefore the idea of finiteness spaces used in Ehrhard's paper cannot be used to model the untyped lambda-calculus, or PCF.There are several questions stemming from this area, the answers to which this project may provide. Firstly, which computational phenomena can we model naturally using differential operators and Taylor expansion? Often, some property must be sacrificed to gain another. For example, in order to allow for divergent series, EhrhardÕs models restrict us in such a way that we lose the ability to model fixed-point combinators (recursion) and hence the untyped lambda-calculus. Another direction of interest is extending the differential lambda-calculus to differential PCF. Key challenges with this task would be the treatment of recursion (fixed-points) and conditionals, due to these required trade-offs mentioned above. Branching out further, there are the challenges of providing an algebraic model of the differential lambda-calculus, in the same fashion as the combinatory algebras with the regular lambda-calculus. An attempt at a similar problem for the resource calculus has been made in the past, but only the finite resource calculus was modelled, not the full fragment.This project will align with the strategic focus of the Theoretical Computer Science research area by utilising semantics to improve our understanding of computation, while being applicable to real-world problems such as the run-time/resource usage of programs.

该项目属于EPSRC理论计算机科学研究领域的数学科学研究主题下的福尔斯。如标题所述，这个项目将集中在利用微分lambda演算固有的资源敏感性，从语义的角度研究资源有限的计算。一个非常有前途的方法是使用定量语义来解释这些计算。我们将类型解释为向量空间，将加法解释为原子态的叠加，将标量解释为叠加的度量。因此，我们可以把程序表示为幂级数，其中只使用一次输入的程序表示为线性函数。这种语义方法允许我们对程序的运行时间和资源使用等属性进行建模。这一领域最先进的工作的例子包括概率程序和量子程序的模型。在此之前，埃哈德通过定量语义学建立了一个微分微积分模型。不幸的是，这个模型不能解释不动点算子，因此Ehrhard论文中使用的有限性空间的概念不能用来模拟无类型的无类型演算，或PCF。有几个问题源于这个领域，这个项目可能会提供答案。首先，哪些计算现象我们可以自然地使用微分算子和泰勒展开建模？通常，必须牺牲一些财产才能获得另一个财产。例如，为了允许发散级数，埃尔哈特模型限制了我们，以至于我们失去了对定点组合子（递归）建模的能力，从而失去了无类型的递归演算。另一个感兴趣的方向是将微分微积分扩展到微分PCF。这个任务的关键挑战是递归（定点）和条件的处理，因为上面提到了这些需要权衡的问题。进一步扩展，有提供微分代数演算的代数模型的挑战，以同样的方式与常规代数演算的组合代数。过去也曾尝试过类似的资源演算问题，但只对有限资源演算进行了建模，而不是完整的片段。本项目将通过利用语义来提高我们对计算的理解，同时适用于现实世界的问题，如程序的运行时/资源使用，从而与理论计算机科学研究领域的战略重点保持一致。