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

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

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.