本論文「関係代数による非決定的プログラムの意味定義に関する研究」は数学上の関係を用いて、様々な非決定的なプログラムから抽象化した代表的な選択(エンゼリック選択(locally angelic choice)、デモニック選択(locally demonic choice)とエラティック選択(erratic choice))の意味定義を形式的に与え、それらの意味定義を用いて、非決定的なゲームの推論とUNITY(Unbounded Nondeterministic iterative transformations)(Chandy and Misra)ループの意味定義を与える。さらに、関係で表現した問題の仕様からアルゴリズムの導出方法を提案する。

　三種類の選択は次のように記述することができる(⊥は計算が失敗する場合を表す)

図表

　非決定的なプログラムの全体の実行結果を考慮すると、エンゼリック選択とデモニック選択は大局と局所の2種類に分けられる。大局選択はプログラム全体の結果によって、選択肢を決める。一方、局所選択は選択子両側の式のみによって、選択肢を決める。

　従来の手法では、Plotkin、Hoare及びSmyth意味ドメインを用いて、単独に、エラティック選択、大局エンゼリック選択または大局デモニック選択の意味定義しか扱えないが、本論文の手法によって、局所エンゼリック選択、局所デモニック選択の意味定義が可能となり、それらの選択が同時に現われる式の意味定義も可能となる。

　本論文は次のように構成される。第1章「Introduction」で、本研究の背景、目的及び成果を論じ、本論文で提案した手法の概略を紹介する。まず、非決定的プログラムを抽象化した3つの選択について紹介し、それらの選択に対する従来の意味定義方法を述べ、本論文の手法の概略を述べる。最後に、関係代数を用いて問題仕様からアルゴリズムを導出する方法を紹介する。

　第2章「Relational Algebra」で、本論文に使われる関係における数学の記法、性質、特に、Tarski定理などを導入する。本論文はBackhouseの研究に使われた記法を使用する。この章では、関係(R)の上にオーダ(⊆)を導入し、(R,⊆)はCPOであることを証明する。Tarski定理によって、任意の⊆単調関数f∈R→Rについて不動点が存在することが保証される。この事実は非決定的な式のデモニック側面の意味定義に使われる。

　第3章「A Small Language」で、3つの選択が同時に現われることを許す非決定的なプログラム言語を定義する。また、本論文で提案した手法はデータ構造を持つような言語に対しても有効であることを検証するために、polynomial relatorは⊆-単調で、かつ、関係のデモニック合成に対する分配律を満たしていることを証明する。この章で定義した言語を用いて作成されたプログラムに対する推論、証明などを関係の上で行なうことができる。

　第4章「Application Examples」で、二つの応用例を挙げる。第1例は、関係の上で、デモニック側面の意味定義を利用して、非決定的なゲームを推論する例である。第2例は良く知られるUNITY(Unbounded Nondeterministic iterative transformations)(Chandy and Misra)ループの意味定義を与え、関係の上にUNITYループに対して推論、証明を行なう。このアプローチと従来のUNITYループに対する推論方法との関連も述べる。我々の関係上のアプローチはプログラムの入力/出力のみを観察可能(observable)とし、定義の結合が可能となり、証明を簡潔に行なわれるようになる。この章までは、関係によって、非決定的なプログラム言語(局所エンゼリック選択、局所デモニック選択、エラティック選択の意味定義を与える。

　第5章「An Approach of Transformation」で、関係で書かれた問題の仕様から、生成&テストアルゴリズムを導出する方法を示す。その基本的なアイデアは関係定義に生成関数を導入することである。このアプローチは一つの仕様から異なるアルゴリズムを導出することを可能にする。

　第6章「Related Work and Conclusions」で、関連研究との比較及び残された課題について述べる。非決定的なプログラムの意味定義についての関連研究ではBroy、Hughes、Berghammer、Henkなどの研究にふれる。アルゴリズムの導出についての関連研究ではNogi、Birdなどの研究にふれる。我々の手法はsingular形式の非決定的なプログラムにのみ有効であるがplural形式のプログラムに対しては今後の課題となる。

　本論文はRelational Semantics of Nondeterministic Programs(関係代数による非決定的プログラムの意味定義に関する研究)と題し、英文で書かれ、6章からなる。数学上の関係を用いて、さまざまな非決定的なプログラムから抽象化した代表的な3種類の選択、すなわち、エンゼリック選択(angelic choice)、デモニック選択(demonic choice)、およびエラティック選択(erratic choice)に対して意味定義を形式的に与え、それらを用いて、非決定的ゲームに関する推論とUNITY(Unbounded Nondeterministic Iterative Transformation)ループの意味定義を与えることによって形式的定義の有効性を主張している。

　従来は、非決定的なプログラムの振舞いをエンゼリック選択とデモニック選択として捉え、これらは大局的なものと局所的なものに分けられていた。大局的な選択はプログラム全体の望まれる結果に応じて選択肢を決めようとするものであり、局所的な選択は非決定的な選択の式のみによって選択肢を決めるものである。従来の手法ではそれぞれが単独に、エラティック選択、大局的エンゼリック選択、または大局的デモニック選択を扱うものであって、局所的エンゼリック選択、局所的デモニック選択の意味定義を行なうことは不可能であった。本研究は、これらを統一的な枠組みで扱い、それらの形式的な定義を与えることによって、種々の選択が同時に現われるプログラムの非決定性について議論する基盤を与えることを目的としている。

　第1章「Introduction」では本研究の背景、目的、および成果を論じ、本論文で提案している形式的定義の概略を述べている。まず、非決定的プログラムを抽象化した3種類の非決定的選択について紹介し、それらの選択に対する従来の意味定義の方法を述べ、関係代数による本論文の手法の位置づけを明確にしている。

　第2章「Relational Algebra」では、本論文で用いている「関係」に関する数学の記法、性質、および、Tarskiの定理などを導入している。この章では、関係の集合の上に各種の順序を導入し、それらが完備半順序集合(Complete Partial Order,CPO)をなすことを証明している。この性質は、任意のCPO上の単調関数が不動点を有するというTarskiの定理に基づく形式的議論に帰着させるための基礎であり、非決定的な式のデモニック側面の意味定義に使われるものである。

　第3章「A Small Language」では、3種類の選択が同時に現われることを許す非決定的な式の構成を含むプログラム言語を与え、意味を定義している。また、本論文で提案した手法がデータ構造を持つ言語に対しても有効であることを検証するために、それらの基礎となる関係がデモニック合成に対する分配律を満たしていることを証明している。本章で定義した言語によるプログラムに対する推論、証明などは関係代数を用いて行なうことができることを例証している。

　第4章「Application Examples」では非決定的な選択を含むプログラムに関する2つの応用例を挙げている。第1例では、関係の上でデモニック側面の意味定義を利用して、非決定的なゲームの推論を行なう例であり、第2例はUNITYループの意味定義を与えるものである。そこでは、従来の手法との違いを明確にし、本手法ではプログラムの入出力のみを観察可能なものとし、定義を結合することによって、簡潔に性質の証明を行なうことができると主張している。

　第5章「An Approach of Transformation」では、関係で書かれた問題の仕様から生成・テストのアルゴリズムを導出する方法を示している。これは関係を用いた定義に関する別の側面からの議論であるが、仕様からプログラムを導出する際にも非決定性による柔軟さが有効であることを例証している。

　第6章「Related Work and Conclusions」では関連研究との比較、および課題について述べている。従来の代表的な研究成果と本研究を比較検討し、本研究の新規性を明確にするとともに、その限界についても言及している。また、本研究で対象としたものとは異なる構造の非決定的なプログラムに対して今後の課題を述べている。

　以上を要するに、本論文は従来、十分には検討されていなかった非決定性をもつプログラムの意味を「関係」によって定義し、3種類の非決定性の差異を明確に記述する方法を示したものであり、情報工学上貢献するところが少なくない。よって本論文は博士(工学)の論文として合格と認められる。