Studying resource-limited computation from a semantic angle, utilising the differential lambda-calculus along with quantitative semantics
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
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.
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.
Organisations
People |
ORCID iD |
| Luke Ong (Primary Supervisor) | |
| Thomas Mattinson (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509711/1 | 01/10/2016 | 30/09/2021 | |||
| 1893511 | Studentship | EP/N509711/1 | 01/10/2017 | 01/09/2021 | Thomas Mattinson |
| Description | Formulation of two transformers: The first takes a probabilistic program and returns information on whether this program has a corresponding probability density function. The second takes a probabilistic program and returns a list of corresponding probability density functions, if they exist. This is a large extension to previous work stemming from a 2012 paper by Bhat et al. titled "A type theory for Probability Density Functions". |
| Exploitation Route | The first transformer doesn't have much practical application as of yet, but can provide a useful tool in guiding use towards stronger transformation rules for the second transformer. The second appears to have particular application in the field of nested inference (observing the output of a nested program, as discussed by Rainforth 2017). In general these transformers may also provide valuable insight in how to extend existence automatic disintegrators (discussed in a set of works by Shan and others). |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Healthcare,Pharmaceuticals and Medical Biotechnology |