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.