1989 Fiscal Year Final Research Report Summary
Abstraction of Nonterminating Processes and Its Algebraic Specification
| Project/Area Number |
63580025
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
SAKABE Toshiki Nagoya Univ., Faculty of Eng., Associate Professor, 工学部, 助教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HIRATA Tomio Nagoya Univ., Faculty of Eng., Associate Professor, 工学部, 助教授 (10144205)
INAGAKI Yasuyoshi Nagoya Univ., Faculty of Eng., Professor, 工学部, 教授 (10023079)
|
|---|
| Project Period (FY) |
1988 – 1989
|
| Keywords | nonterminating process / equational logic / algebraic specification / concurrent process / CCS / tree pattern matching |
|---|
| Research Abstract |
The purpose of this research project is to establish technical foundation of algebraic specification of nonterminating processes. Specific research topics and the results are as follows:
1. Semantical aspect of the rational equational logic, in which nonterminating processes are expressed, has been investigated. Adopting Scott's order theoretic approach, the semantics of term rewriting system has been formalized. Characteristic points of the semantics are (1) that computational complexity of term rewriting systems is incorporated in the semantics and (2) that complexity of nonterminating computation is naturally given.
2. For implementing interpreters or compilers of algebraic languages, tree pattern matching is the most fundamental operation. In the research of algebraic languages, three algorithms for tree pattern matching, have been proposed. Particularly, the parallel tree matching algorithm using systolic array is interesting in that it runs in linear time order and is easily implemented in VLSI.
3. CCS is a formal model of concurrent processes including nonterminating processes. In the research of CCS, the original CCS has been extended so that communication links among processed can be changed dynamically, and the semantics of the extended CCS has been investigated. To investigate the expressive power of the extended CCS, monitors has been described in the extended CCS. As results mutual exclusion synchronization mechanism of monitors are plainly expressed in terms of new features of the extended CCS, and abstraction mechanism of monitors is naturally explained through the semantics of the observational equivalence on the extended CCS.
4. A model of concurrent processes based on term rewriting system has been proposed. The model is called the communicating term rewriting systems. Main results of this research is that independence of internal computation of processed from computation for communication and uniqueness of computed values are proved.
|
