並行システムの実行時プログラム変換の形式化についての研究

并发系统运行时程序形式化转换研究

• 批准号: 10139229
• 负责人: 村上 昌己
• 金额: $ 0.38万
• 依托单位: Okayama University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas (A)
• 财政年份: 1998
• 资助国家: 日本
• 起止时间: 1998 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-10139229/
• 关键词: 並行プロセス; 線形論理; プログラム変換; 部分計算

本研究は,並行プロセスのソフトウェアの動的発展機能の形式的記述を確立することを目指すものである.その具体的手法として,与えられたプログラムの変換と実行を同時に進行させるプロセスの形式的記述を検討するものである.本研究で変換の対象とするプログラムのクラスは,応答型の並行プロセスである.まず本研究では、並行プロセスの機能の一部を起動中に外部からの要求に応じて変更する手法を提案した.ここで対象とする並行プロセスは線形論理の論理式の記法で記述されたものであり、非同期π計算と同等な記述能力をもつ.プロセスの起動及びメッセージの発信は○左導入の推論によって、またメッセージの受信は。左導入の推論規則によって表現される.その操作的意味論はシークエント計算LLの部分体系での証明によって記述される.本研究では、現在有効なプロセスの定義を機能の変更を求めるメッセージによって新しい機能のプロセス定義に置き換える機構を、線形論理の論理式の記法により記述する手法を提案した.このような機構の動作も、LLの推論規則によって構成される証明によって記述される.さらに本研究では逐次的に実行される部分を含も並行プロセスを並列実行する方法について考察する.ここで対象とする並行プロセスは線形論理で記述されたものであり、その操作的意味論はLK風のシークエント計算の推論規則によって記述される.本稿ではこの体系に並列実行のための規則として、プロセス定義の展開のための規則と値を将来実行される部分に伝搬して分岐を枝刈りのための規則を導入した.これらの規則を用いた推論がLLの体系で可能であることから、見込み計算によるプロセスの並列実行が線形論理におけるシークエント計算での証明の枠組みの中で記述できることを示した.またこれらの規則を用いた並列実行に対して、外部から観測した際に同等な計算とみなせる逐次実行が存在することを示した.

This study aims to establish a description of the form of the development function of the parallel motion of the software. The specific method and the implementation of the change of the form of the description of the change are discussed simultaneously. This paper presents a study on the relationship between the change of image and the change of image, and the change of image and the change of image. This research proposes ways to change the functionality of a parallel console in response to external requirements while starting up part of the functionality. The description of linear logic and the notation of logical expressions are parallel to each other. The description of asynchronous π calculation is equivalent to the description of linear logic. The information of the starting point and the starting point of the project is transmitted to the inferring point and the receiving point of the project. Left import inference rules are presented in the table below. The meaning of the operation of the system is described in detail. In this study, we propose a method for describing the structure, linear logic, and logical expression of a new functional definition. The action of the mechanism, the inference rule, the composition, the proof, the description. This study is carried out in a sequential manner, including parallel and parallel methods. This is a description of the linear logic, the meaning of the operation, and the inference rules of the calculation. This paper introduces the rules of parallel operation of the system, the rules of development of the definition of the system, the rules of future operation of the system, the rules of division of the system, and the rules of division of the system. The rules of the system are used to infer that the system is possible, and the parallel implementation of the linear logic is used to calculate the proof of the system. The rules are applied in parallel, and the rules are applied in parallel.

项目成果

村上昌己: "線形論理を用いた逐次型プロセスの並列実行" 情報処理学会論文誌. 発表予定.

Masami Murakami：“使用线性逻辑并行执行顺序处理”，日本信息处理学会会刊，计划出版。