Foundamental Study on Fundational Model of Concurrent Computation

本研究项目的目的是开发一种基于缩小的并发计算功能模型，以便利用重写技术对并发程序进行分析和验证。这是我们目标模型的初步版本。DTRC具有在计算过程中动态更改重写规则、分层声明函数符号、变量和重写规则等功能。我们得到了关于DTRC项的汇聚性和终止性的基本结果。我们还研究了进程代数的理论，并提出了CCS的两个扩展。一种是有限制值的CCS。它将术语重写系统作为定义(可能是限制)值的机制，并具有按限制值进行分支的功能。通过引入测试精度的新概念，给出了扩展的CCS的语义。另一个扩展是带有广播的CCS(称为CCS b)。它形式化地描述了广播的特点，即接收信号时的一对多通信和不确定性通信。我们得到了选择和并行复合算子的交换性和结合性低，以及展开低。对树模式匹配进行了研究，提出了一种并行的树模式匹配算法，改进了Ramesh等人的算法。在时间和空间上。

The purpose of this research project is to develop a functional model of concurrent computation based on narrowing such that we can analyze and verify concurrent programs by using rewriting techniques.The results we obtained in the research project are as follows.We first proposed a computation model called Dynamic Term Rewriting Calculus (DTRC, for short). It is a preliminary version of our target model. DTRC has features such as dynamically changing rewrite rules during computation and hierarchically declaring function symbols, variables and rewrite rules. We obtained fundamental results on confluency and termination of DTRC terms.We also investigated the theory of process algebras and proposed two extensions of CCS. One is CCS with limit values. It has term rewriting systems as the mechanism for defining (possibly limit) values and has the feature of branching by a limit value. We gave a semantics for the extended CCS by introducing a new concept of test precision. The other extension is CCS with broadcast (called CCS+b). It formalizes broadcast which is characterized with one-to-many communication and nondeterministic communication in receiving signals. We obtained commutativity and associativity lows for choice and parallel composition operators, and expansion low. These lows are useful for analyzing processes.We studied tree pattern matching and found a parallel algorithm for tree pattern matching which improved the algorithm of Ramesh et al. in time and space.