Abstraction of Nonterminating Processes and Its Algebraic Specification

非终止过程的抽象及其代数规范

• 批准号: 63580025
• 负责人: SAKABE Toshiki
• 金额: $ 1.34万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1988
• 资助国家: 日本
• 起止时间: 1988 至 1989
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-63580025/
• 关键词: nonterminating process; equational logic; algebraic specification; concurrent process; CCS; tree pattern matching; 代数的仕様

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.

本研究项目的目的是为非终止进程的代数描述奠定技术基础。具体的研究内容和结果如下：1.研究了表示非终止过程的有理方程逻辑的语义方面。采用Scott的序论方法，形式化地描述了术语重写系统的语义。语义的特点是(1)术语重写系统的计算复杂性被融入到语义中，(2)自然地给出了不终止计算的复杂性。对于实现代数语言的解释器或编译器，树模式匹配是最基本的操作。在代数语言的研究中，已经提出了三种树模式匹配算法。特别地，基于脉动阵列的并行树匹配算法以线性时间顺序运行，并且易于在VLSI中实现。CCS是一个包含非终止进程的并发进程的形式化模型。在CCS的研究中，对原有的CCS进行了扩展，使得进程之间的通信链路可以动态变化，并对扩展后的CCS的语义进行了研究。为了研究扩展CCS的表达能力，在扩展CCS中描述了监视器。通过扩展CCS的新特性，清晰地表达了监控器的互斥同步机制，并通过扩展CCS的观测等价语义自然地解释了监控器的抽象机制。提出了一种基于术语重写系统的并发进程模型。该模型被称为通信术语重写系统。本研究的主要结果是证明了处理的内部计算与通信计算的独立性和计算值的唯一性。

项目成果

山中英樹,坂部俊樹,稲垣康善: 電子情報通信学会技術研究報告. COMP88ー96. 61-70 (1989)

Hideki Yamanaka、Toshiki Sakabe、Yasuyoshi Inagaki：IEICE COMP88-96 (1989)。

結縁祥治: "CCSにおける通的通信名前づけについて" 情報処理学会研究報告. SF-86-26. 1-10 (1988)

Shoji Yuen：“关于 CCS 中的通用通信命名”日本信息处理学会研究报告 SF-86-26 (1988)。

酒井正彦: "代数的仕様における帰納的性質の証明法" 電子情報通信学会技術研究報告. COMP88-86. 83-92 (1989)

Masahiko Sakai：“代数规范中归纳性质的证明方法”IEICE COMP88-86 (1989)。

Tohru NAOI and Yasuyoshi INAGAKI: "Algebraic Semantics and Complexity of Term Rewriting Systems" Transactions on IEICE, vol.J71 D-I, pp.1893-1900, 1988.

Tohru NAOI 和 Yasuyoshi INAGAKI：“代数语义和术语重写系统的复杂性”，IEICE 交易，第 J71 D-I 卷，第 1893-1900 页，1988 年。

Shin-ichirou YAMAMOTO, Masahiko SAKAI, Toshiki SAKABE and Yasuyoshi INAGAKI: "An Implementation of the Outer-most Parallel Strategy of the TRS Interpreter," Technical Research Report of IEICE, COMP88-86, pp.41-50 1989.

Shin-ichirou YAMAMOTO、Masahiko SAKAI、Toshiki SAKABE 和 Yasuyoshi INAGAKI：“TRS 解释器最外层并行策略的实现”，IEICE 技术研究报告，COMP88-86，第 41-50 页，1989 年。