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

使用抽象高阶重写系统的过程计算的形式化

• 批准号: 13680388
• 负责人: SUZUKI Taro
• 金额: $ 2.18万
• 依托单位: The University of Aizu
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2002
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13680388/
• 关键词: process calculus; π-calculus; abstract higher-order rewrite system; equational rewrite system; higher-order narrowing; abstract narrowing; pattern rewrite system; プロセス書換え系; 関数論理型言語

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.

利用重写系统，特别是van Oostrom提出的抽象高阶重写系统（AHRS，简称AHRS），对π-演算等移动过程演算进行了形式化研究。重写系统实际上是一个元重写系统，因为它的机制被称为替代演算，它为AHRS模拟的具体重写系统提供了替代行为。我们期望该系统的这种挠性对形式化若干移动过程演算是有用的。我们将AHRS扩展为一个等式重写系统。我们称该系统为方程抽象高阶重写系统（简称EAHRS）。我们发现EAHRS对于π微积分的形式化非常有用。本文所发现的过程演算与重写系统之间的对应关系，对于利用重写界研究的几种方法来研究过程演算的理论性质是有帮助的。我们在这项研究资助下的另一个研究结果是关于缩窄与ahrs之间的关系。众所周知，过程演算为并行逻辑程序设计语言提供了运算语义。另一方面，窄化是重写的扩展，它为函数逻辑编程语言提供了操作语义，它包含函数和逻辑编程语言。因此，我们认为研究过程演算与缩窄之间的关系是非常重要的。我们首先从Prehofer演算出发，提出了一些新的高阶狭窄演算。所得的一些演算比Prehofer的演算具有更窄的搜索空间。然后，我们以两种方式在AHRSs上使用抽象窄化形式化一阶和高阶窄化。令人惊讶的是，如果底层（具体的）重写系统是所谓的模式重写系统，那么这些完全不同的形式化是一致的，模式重写系统通常用于高阶窄化。我们还证明了抽象缩窄的完备性，它的证明比一般的证明简单明了。

项目成果

A.Middeldorp, T.Suzuki, M.Hamada: "Complete Selection Functions for a Lazy Conditional Narrowing Calculus"Journal of Functional Logic Programming. (To Appear). (2002)

A.Middeldorp、T.Suzuki、M.Hamada：“惰性条件窄化演算的完整选择函数”函数逻辑编程杂志。

M.Marin, T.Suzuki, T.Ida: "Higher-Order Lazy Narrowing for Left-Linear Fully-Extended Pattern Rewrite Systems"筑波大学電子・情報工学系テクニカルレポート. ISE-TR-01-180. (2001)

M.Marin、T.Suzuki、T.Ida：“左线性完全扩展模式重写系统的高阶惰性窄化”技术报告，筑波大学电子与信息工程系 ISE-TR-01-180。 （2001）

Taro Suzuki and Satoshi Okui: "Formalization of π-calculus using abstract higher-order rewrite systems"Technical report, the University of Aizu. (2003)

铃木太郎和奥井聪：“使用抽象高阶重写系统的 π 演算的形式化”技术报告，会津大学（2003 年）。

奥居哲, 鈴木太朗: "抽象高階書換え系におけるナローイング"会津大学テクニカルレポート. (2003)

Satoshi Okui、Taro Suzuki：“抽象高阶重写系统的窄化”会津大学技术报告（2003 年）。

A.Middeldorp, T.Suzuki, M.Hamada: "Complete Selection Functions for a Lazy Conditional Narrowing Calculus"Journal of Functional Logic Programming. 2002(3). (2002)

A.Middeldorp、T.Suzuki、M.Hamada：“惰性条件窄化演算的完整选择函数”函数逻辑编程杂志。