Abstraction of Nonterminating Processes and Its Algebraic Specification

本研究目的在于建立非终止过程的代数规范的技术基础。具体的研究课题和结果如下：1。研究了表达非终止过程的理性等式逻辑的语义问题。采用斯科特的顺序理论方法，形式化了术语重写系统的语义。该语义的特征点是：(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.