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

点击翻译按钮获取中文摘要

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.