Formalization of Process Calculi Using An Abstract Higher-Order Rewrite System

我们的目标是利用重写系统，特别是货车Oostrom提出的抽象高阶重写系统（abstract higher-order rewrite system，简称AHRS）对移动的进程演算，如π演算进行形式化。重写系统实际上是一个Meta重写系统，由于称为替换演算的机制，它给出了AHRS模拟的具体重写系统的替换行为。我们期望系统的这种灵活性对形式化几种移动的进程演算是有用的。我们称之为方程抽象高阶重写系统（EAHRS，简称）。我们发现EAHRS对于形式化π演算是非常有用的。我们发现的过程演算和重写系统之间的对应关系对于使用重写社区中研究的几种方法来研究过程演算的理论性质是有用的。基于该研究基金，我们的另一个研究结果是关于窄化和AHRSs之间的关系。众所周知，进程演算为并行逻辑程序设计语言提供了操作语义。另一方面，窄化是重写的扩展，为函数逻辑编程语言提供了操作语义，它包含函数和逻辑编程语言。因此，我们认为研究过程演算中的计算与缩窄化之间的关系是非常重要的。一些得到的演算有更窄的搜索空间比Prehofer的。然后，我们形式化的一阶和高阶缩小AHRSs抽象缩小两种方式。令人惊讶的是，如果底层（具体的）重写系统是所谓的模式重写系统，这些完全不同的形式化一致，这通常用于高阶窄化。我们还证明了抽象缩窄的完备性，其证明比一般的缩窄证明简单明了。

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.