Abstraction of Nonterminating Processes and Its Algebraic Specification

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

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.