| Budget Amount *help |
¥3,400,000 (Direct Cost: ¥3,400,000)
Fiscal Year 2002: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 2001: ¥2,300,000 (Direct Cost: ¥2,300,000)
|
|---|
| 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.
|
