2002 Fiscal Year Final Research Report Summary
Formalization of Process Calculi Using An Abstract Higher-Order Rewrite System
| Project/Area Number |
13680388
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | The University of Aizu |
|---|
Principal Investigator |
SUZUKI Taro School of Comp. Sci. and Eng., Assistant Prof., コンピュータ理工学部, 講師 (90272179)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OKUI Satoshi Chubu University, Dept. of Computer Science, Associate Professor, 工学部, 助教授 (00283515)
|
|---|
| Project Period (FY) |
2001 – 2002
|
| Keywords | process calculus / π-calculus / abstract higher-order rewrite system / equational rewrite system / higher-order narrowing / abstract narrowing / pattern rewrite system |
|---|
| Research Abstract |
We have aimed formalization of mobile process calculi, such as π-calculus, using rewrite systems, especially, abstract higher-order rewrite system (AHRS, for short) proposed by van Oostrom. The rewrite system is actually a meta rewrite system due to the mechanism called substitution calculus, which gives behavior of substitution for a concrete rewrite system that the AHRS simulates. We expect such the flexible property of the system is useful for formalizing several mobile process calculi.
We extended the AHRS to an equational rewrite system. We call the system equational abstract higher-order rewrite system (EAHRS, for short). We found the EAHRS is very useful for formalizing π-calculus. The correspondence relation between process calculi and rewrite system we found is useful for studying theoretical properties of process calculi using several methods studied in rewriting community.
Another result of our research based on this research grant is about relationship between narrowing and AHRSs. It is well known that process calculi give operational semantics for parallel logic programming languages. On the other hand, narrowing, which is an extension of rewriting, gives operational semantics for functional-logic programming languages, which subsumes both functional and logic programming languages. Hence, we believe that it is important to study relationship between computation in process calculi and narrowing.
We first proposed some novel higher-order narrowing calculi, starting from Prehofer's calculus. Some of the obtained calculi has narrower search space than Prehofer's.
We then formalized first-order and higher-order narrowing using abstract narrowing on AHRSs in two ways. Surprisingly, these quite different formalization coincide if the underlying (concrete) rewrite systems are so-called pattern rewrite systems, which is often used in higher-order narrowing. We also show completeness of abstract narrowing, whose proof is very easy and clear than the ordinary one.
|
Research Products
(10 results)
