関係代数によるUNITYループの意味づけ Relational Definition of UNITY Loop

関係は一対多の対応を記述するものである。関係代数はプログラム、特に、ある入力値に対する可能な出力値が複数あるような非決定的なプログラムを記述する数学モデルとして重要な役割を果たしてきた。一方、UNITY(Unbounded Nondeterministic Iterative Transformations)は並列計算プログラムの設計、検証に有用なアプローチとして知られている。従来、UNITYに対する意味定義、推論は一種の時制論理(Temporal Logic)を基本としてきたが、その記法はvariable-wiseスタイルであって簡潔さに欠ける。本論文では、関係代数により抽象化された局所エンゼリック選択(locally angelic choice)の定義を利用して、UNITYループに対して形式的な意味定義を与える。さらに、UNITYループ固有の性質を関係代数を用いて推論し証明する方法を、簡単な例とともに示す。

Relation is a set of pairs which is suitable for describing one-input-multiple-output correspondences. Relational algebra as a mathematical model has been playing important role in specification of nondeterministic programs. UNITY(Unbounded Nondeterministic Iterative Transformations), on the other hand, is an approach to specification, design and verification of parallel programs. UNITY loop is usually reasoned by some kind of temporal logic which is in variable-wise style. In this paper, we give a formal definition of the UNITY loop with the help of the relational definition of the locally angelic choice. The purpose of this paper is to make a variable-free definition and give a concise proof tool on UNITY loop by means of relations.