|
| EPSRC Reference: |
EP/D001307/1 |
| Title: |
Priorities in Operational Semantics and Term Rewriting |
| Principal Investigator: |
Dr I Ulidowski |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Computer Science |
| Organisation: |
University of Leicester |
| Scheme: |
Overseas Travel Grants |
| Starts: |
19 July 2005 |
Ends: |
18 November 2008 |
Value (£): |
7,270
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
Operational semantics and term rewriting are well established fields of theoretical computer science. Priority, according to Oxford Paperback Dictionary, means "being earlier or more important" and indicates that an object has "precedence in rank" when compared with other objects. In the context of this project, priorities specify the order of application of operational rules and rewrite rules when deriving transitions and rewrites of terms. The initial research on priorities in operational semantics and term rewriting shows that they extend expressiveness. Priorities replace awkward negative premises in SOS rules and they help to control the ambiguity of term rewriting and to improve the modularity and confluence. The aim of this project is to establish new (and strengthen the existing) collaboration links with the scientists in the Netherlands and Japan in order to explore further the potential of priorities in operational semantics and term rewriting. We intend to extend the Ordered SOS framework with additional features such as predicates and complex terms in the premises, prove congruence results, investigate fully expressive formats and explore their applications in concurrency. In term rewriting with priorities, we plan to re-investigate its operational semantics, find methods for internalising rewrite strategies with priority orders, and explore reasoning for systems with infinite behaviour. Finally, we aim to study Term Deduction Systems with priorities as uniform formalisms for representing such diverse notions as Ordered SOS, priority term rewriting and logic programming languages such as Prolog.
|
| Final Report Summary |
Operational semantics and term rewriting are well established fields of theoretical computer science. Priority, according to Oxford Paperback Dictionary, means "being earlier or more important" and indicates that an object has "precedence in rank" when compared with other objects. In the context of this project, priorities specify the order of application of operational rules and rewrite rules when deriving transitions and rewrites of terms. The initial research on priorities in operational semantics and term rewriting shows that they extend expressiveness. Priorities replace awkward negative premises in SOS rules and they help to control the ambiguity of term rewriting and to improve the modularity and confluence. The aim of this project is to establish new (and strengthen the existing) collaboration links with the scientists in the Netherlands and Japan in order to explore further the potential of priorities in operational semantics, term rewriting and the modelling of reversible computation. We intend to extend the Ordered SOS framework with additional features such as predicates and complex terms in the premises, prove congruence results, investigate fully expressive formats and explore their applications in concurrency. In term rewriting with priorities, we plan to re-investigate its operational semantics, find methods for internalising rewrite strategies with priority orders, and explore reasoning for systems with infinite behaviour. Finally, we aim to research the use of operational semantics, with and without rule priorities, in the modelling of reversible computation within the setting of process algebras. I intend to develop a reversible version of Milner's CCS and to give operational definitions of reversible versions of operators of other process algebras. Such reversible process algebras could become formalisms for the modelling of biochemical systems or for giving semantics to reversible debugging or memory models of multi-threaded programming languages.
|
| Further Information: |
|
| Organisation Website: |
http://www.le.ac.uk |
|
|