|
| EPSRC Reference: |
GR/A11731/01 |
| Title: |
MODELS AND AXIOMS FOR THE SEMANTICS OF COMPUTATION |
| Principal Investigator: |
Dr AK Simpson |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Sch of Informatics |
| Organisation: |
University of Edinburgh |
| Scheme: |
Advanced Fellowship |
| Starts: |
01 October 2001 |
Ends: |
31 March 2007 |
Value (£): |
241,366
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
07 Dec 2000
|
IT Fellowship Sift Panel
|
Deferred
|
|
11 Jan 2001
|
IT Advanced Fellowship Interview Panel
|
Deferred
|
|
|
Summary |
This proposal studies mathematical models of computation. Such models are useful in the specification and verification of computational systems. Their study also constitutes basic research, contributing to the development of a general science of computation.
The proposal consists of two threads: "models", which examines applications of particular mathematical models to specific computational situations; and "axioms", which seeks axiomatic accounts of the common properties amongst such models.
Three specific forms of computation are examined under "models". One is exact real number computation, i.e. real arithmetic without round-off errors. The goal is to achieve a systematic comparison of competing approaches to this within functional programming. The second form of computation is nondeterminism, including probabilistic computation. Again the goal is a classification of competing approaches, aiming in particular at the first treatment of notions of computability for probabilistic functional computation. The third application is concurrency, a broad paradigm that includes distributed, and reactive systems. Here, I shall make contributions to the development of notions of model and to methods of verification.
Under "axioms", I shall develop axiomatic accounts of: models for recursively defined datatypes; equational theories of higher-order recursion; and exact real arithmetic.
|
| Final Report Summary |
The field of "semantics" seeks to assign mathematical meanings to
computational processes, thereby providing mathematical models of
computational behaviour. This fellowship undertook a programme
of basic research into the construction and study of the required
mathematical models of computation.
The research was divided into two threads. In the first, "models",
the concern was the development and study of various concrete models
of computation, modelling different computational situations.
The aim of the second thread, "axioms", was to provide and exploit
axiomatic accounts of the common properties amongst such models.
Three topics were investigated in the "models" thread.
The first was exact real-number computation, i.e. real arithmetic without round-off errors. Different approaches to this form of computation were modelled. Surprisingly the relationship between different approaches was shown to depend on the answer to an open question in the field of mathematical topology.
The second topic was obtaining a mathematical model capable of modelling a rich variety of computational features in combination, including: imperative aspects of computation (so-called "computational effects"), a wide collection of datatype constructions (including "polymorphic types"), and a notion of computability for elements of such datatypes. This was achieved
through the development of "topological domain theory", a mathematical framework for building models of comutation generalising the "domain theory" of Scott.
The third topic was a study of models of probabilistic choice. A new
method for modelling probabilistic choice was proposed, based on using a natural notion of probabilistic observation to determine
a canonical "probabilistic powerdomain". The approach suggests a
general method of modelling other "computational effects" (non-functional aspects of computation) which will be the subject of follow-up research.
The "axioms" thread explored four topics.
The first was an application of "synthetic domain theory" (an axiomatic framework for semantics based on intuitionistic set theory) to provide a general axiomatic account of recursively defined datatypes, generalising research from the 1990's.
The second topic examined the use of synthetic domain theory to prove operational properties of programming languages. A simple axiomatization was given that was particularly suitable for this purpose, and this was applied to prove properties of a language with "parametric polymorphism".
The third topic looked at the interaction between parametric polymorphism and computational effects. An axiomatic account providing a uniform approach to modelling parametric polymorphism in
combination with arbitrary computational effects was developed.
This incorporates and generalises accounts that have previously been given for few special cases of particular effects.
Finally, I developed novel methods for reasoning about concurrent processes and reasoning with inductive definitions, based on the application of methods (sequent-calculus proof systems) from the mathematical field of proof theory.
|
| Further Information: |
|
| Organisation Website: |
http://www.ed.ac.uk |
|
|