博 士 （ 情 報 科 学 ） 三 浦 克 宜

学位論文題名
GenerationofEquiv
alentTransformationRulesviaLogicalEquiv
alenCe（論理等価式を経由した等価変換ルールの生成に関する研究）

学位 論文内容の要旨
ソフトウェアシステムが大規模化するにっれ，優れた信頼性を持っソフトウェア開発の必要性が高まっている．その際，良いアルゴリズムを探索することは効率的なプログラムを作るためにきわめて重要である．等価変換皿）計算モデルに基づくプログラム生成の枠組みは，アルゴリズム探索を達成するための有望な枠組みである，そこでは，ETルールの集合によってアルゴリズムを構築し，そ の集合 からプ ログラ ム変換 によっ てC言語 やHw記述言語たどのプログラムを生成する．このとき，効率的なプログラムの生成に繋がる良いETルールを発見し，生成することが求められる．本論
文では，仕様からETルールを生成するための新しい方法を提案し，その基盤となる理論を明らかにした．提案方法は，まず仕様から論理等価式を作成し，その論理等価式からETルールを生成する，
本論文は8章立てで構成されている．
1章では，序論として研究の背景，研究目的，研究方法にっいて述ぺている．主要な研究課題は，仕様 から論 理等価 式をど う作るか，その論理等価式の正しさをどう保証するか，論理等価式からE
T
ル ー ル を ど う 作 る か ， そ の ETル ー ル の 正 し さ を ど う 保 証 す る か ， の 4っ で あ る ．
2章では，ET計算モデルにおける仕様，プログラムおよぴ計算にっいて説明し，ETルールとは何かを示している.ET計算モデルにおいて仕様は，問題の背景知識と，質問の集合のペアであり，これら は確定飾の集合によって記述されている.
ETルールは，飾集合を宣言的な意味が等しい別の節集合に置き換える手続きを記述する．計算は，問題の背景知識に関して正当なETルールを使った質問
節 集 合 の 変 換 で あ り ， そ の 変 換 は 適 用 可 能 な ETル ー ル が あ る 限 り 繰 り 返 さ れ る ．
3章では，仕様から論理等価式を作成する方法を提案した．論理等価式はアトム集合同士の等価性を記述する論理式である，重要な論理等価式のクラスとして，アトム集合中の異なる2つの変数が等し くなる条件を記述するSp
eqクラス，述語の制約を満たさないアトムの条件を記述するFa
lseクラスを具体的に示し，それぞれの作成方法を提案した．これら2つのクラスは，ETルールのクラスのひと っであ るSpeqルー ルやFalseルール のクラ スに対 応してい る.Speqル ールは確定節の具体化を促進させ，F
alseルールは述語の制約を満たさなぃアトムを持っ節を取り除くため，これらを効果的に使うことで，より少ない変換回数で答えを求めることができ，効率的なプログラム生成に繋がる．
さらに，ETルールを用いて論理等価式の正しさを自動的に証明するための枠組みを提案した．簡単な 論理等 価式の 正しさ は基本的なETルールを使って自動的に証明でき，より複雑な論理等価式は基 本的な ETルール と得ら れるETルールを再帰的に使うことで自動的に証明できることを示した・
4章では，一般的な論理等価式を定義し＿論理等価式からETルールを生成する方法を提案した．

― 781 ‑

一般的な論理等価式は，ある前提条件の基でのアトム集合同士の等価性を記述する式である．前提条
件を含む論理等価式を作成するとき，前提条件を作るための述語を発見することが要求される．この前提条件は複雑になるにっれて発見が難しくなり，その生成の難易度が高くなる.
ET
ルールは，論理等価式を構成するアトム集合と前提条件から作られるルールの適用条件を用いて生成される．前提
条件を含まない場合，ETルールは，単純に論理等価式を構成するアトム集合だけを用いて生成される．ルールの適用条件は，まず論理等価式の前提条件を満たすアトム集合Sを決定し，次に入カされたアト ム集合 がSの要素のときにtrueを返す関数を作成する，そして最後にアトムを用いてその関数を記述することで作成される．
5章では ，提案 した生 成方法 によっ て正し いETルー ルが生 成できることを証明した．正しいETルールとは，問題の背景知識に関して正しく等価変換を行うルールである．生成されたルールが節集合を別の節集合に等価に置き換えているならぱ，その生成されたルールはETルールである．本章の証明は，論理等価式が問題の背景知識に関して正しいときに，その論理等価式によって節集合同士の等価な関係が決まることの証明と，生成されたルールによる置き換えがこの等価な関係の一部であることの明の2ステップからなる・
6章では，提案方法の有効性を示した．有効性の検証のために，ET言語を用いたプログラミング実習で学生が作成したETルールを対象にして生成の可能範囲を調査した．その結果，論理等価式を適切に与 えるこ とで， 全406ルー ル中の 305ルール のETルー ルが生 成でき ること を確認 した．提案
方法は ，膨大 なETルー ルの空 間の中 からあ らかじめ 選択し たクラ スに属 するETル ールだけを探索することができ，帰納的な処理を用いて多様なETルールを作ることができるため，メタ計算を用いた等 価変換 の有限 合成で は生成す ることが困難なETルールを生成できることを確認した．その結 果 ， 提 案 方 法 に よ り ETル ー ル 生 成 の 可 能 範 囲 が 拡 大 で き る こ と を 示 し た ．
7章では ，プロ グラム生成システムに提案方法を組み込むための枠組みを検討した．そのシステムは， 逐次的 にETルー ルを生 成し， そのETルールを蓄積する繰り返し作業によルアルゴリズムを構築す る.ETルー ル生成の方式として，メタ計算の方法と論理等価式の方法を併用することを提案した．提案方法を組み込むことの有効性を示すために，従来では生成が困難である問題を使った実行例を示し，システムを使うことでこの問題を解決するプログラムを生成できることを確認した．その結果．本論文の成果によってより多くの問題に対するプログラムの生成が可能になることを示した．
8章では ，結論 として 本論文 で得ら れた成 果にっ いてまと め，今後の研究課題を示している‐

ー 782一

学位論文審査の要旨
主 査 教 授 赤 間清副 査 教 授 大 宮学
副 査 教 授 栗 原 正 仁
副 査 教 授 水 田 正 弘，
学位論文題名
Generatjon of Equivalent Transformation Rules via
Logic
alEquivalence（論理等価式を経由した等価変換ルールの生成に関する研究）プログラムは現代 社会を構成する主要を基盤 の1つであり、プログラムを作る技術は極めて重要である。しかし正し く高速をプログラムを構築 するには高い技術が必要であり、大きく複雑をプログラムを作るには、大き誼困難が伴う。そこで、問題の記述（仕様）から正しく高速をプログラムを自動的に生成するた めの研究が行われている。 重要をアプローチの1っはプログラム変換の研究であり、仕様に近く正 しいが遅いプログラムを順 次変換して正しくしかも高速をプログラムを得ようとする。しかしこの 方法では、必ずしも十分を 高速化を達成できるとは限らをい。プログラム空間上の探索は本質的に 困難を課題であり、その結 果、探索は限定された範囲内にとどまる傾向があるからである。
この欠点を克服す る有カを方法は、プログラ ムを等価変換ルールの集合とみをし、プログラムの空間でよりよいプロ グラムを探索するのではを く、．等価変換ルールの空間で、よりよい等価変換ルールを探索するも のである。問題がプログラ ムの探索から等価変換ルールの探索に明快に分割され、探索のコストが 大幅に削減できるからであ る。等価変換ルールからをるプログラムの部分正当性を 厳 密に 保証 でき ることが、 等価変換ルールに分割すべき ことの理由の1つである。等 価変換
ルー ルの 多様 性が 、と の方 法の 豊か をプロ グラ ム生 成の 可能 性を 示している。
この背景のもとで本研究は、仕様か．ら等価変換ルールを生成するという課題に着目し、その新しい方法を提案し、そ の基盤と誼る理論を明らか にしている。また、提案方法を用いたプログラム生成実験システムを構 築し、有用性を確かめてい る。提案方法の特徴は論理等価式という論理式を用いることであり、仕 様から論理等価式を経由し て等価変換ルールを生成する方法を研究している。
本 論 文は 8章で 構 成さ れて いる 。 1章、 2章 で、 研究 の 背景 、研 究目 的、研究方法、ET計算モデル、プログラム生 成について説明したあと、 3章では、論理等価式のいろいろをクラスを定義している。一般的を論 理等価式は、ある前提条件 の基でのアトム集合同士の等価性を記述する式である。また、与えられ た仕様から、それに関して 正しい論理等価式を生成する方法を提案している。
その基本的をやり方 は、論理等価式の候補を生 成し、その正当性を等価変換ルールを使って背理法で証明することであ る。低コストで有望を論理 等価式を提案するために、Sp
eqクラスやFalse
クラ―783ースを どの特別を論理等価式のクラ スが提案され、そのクラスの論理等価式の候補を生成するアルゴリズ ムを与えている。
4章 では 、論 理 等価 式か らETルールを生成する 方法を提案している。論理 等価式が前提条件を
含 まを い 場合 、ETルー ル は、 単純に論理等価式 を構成する2つのアトム集合 を矢印で結んで生成さ れる 。 前提 条件 を含 む 論理 等価 式か らETル ール を作 成する場合、ETルー ルは、論理等価式を構成 する2つのアトム集合を矢印 で結び、前提条件から作られ るルールの適用条件を条件部において作 成される。
5章 では 、4章で 提案 し たル ール 生成 方法 に よっ て、 正しいETルールが生 成できることを証明
し てい る 。正 しい ETル ー ルと は、 問題 を記 述 する 確定 節に関して常に正し い等価変換を与える
ルー ルである。本章の証明は、(1)論理等価式が問題を記述する確定節（背景知識）に関して正しいとき に、その論理等価式によって 節集合同士の等価を関係が 決まり、(2)生成されるルールによる置 き 換 え が こ の 等 価 関 係 に 含 ま れ る こ と を 示 す こと に よ っ てを され ている 。
6章 では、提案方法の有効性を 調査によって示している。ま たメタ計算を用いた等価変換の有限合成 という従来方法と比較して、 提案方法の有用性を論じて いる。7章では、提案方法をプログラム生 成システムに組み込み、提案 方法の有効性を確認してい る。最後に8章では、成果をまとめ、今後 の課題を示している。て れを要するに、著者は、プロ グラム自動生成のために、仕様から論理等価式を経由して等価変換ル ールを生成するための、技術 的をらびに理論的を新知見を得たものであり、ソフトウエア工学と知 識情報処理の発展に貢献する ところ大をるものがある。よって著者は、北海道大学博士（情報科学 ）の学位を授与される資格あ るものと認める。

‑ 784―