博士（工学）近藤 学位論文題名
真 偽維持 システムを用いた項書換えシステムの 推論 手続きに 関する 研究
学位論文内容の要旨
項書換えシステムは，等式を左辺から右辺への書換え規則とみなし，項と呼ばれる 式を書換えることによって計算を行う計算システムである．その応用として，ソフト ウェア工学の分野では代数的仕様記述，関数型プログラミングに，また，人工知能の 分野では定理自動証明などに用いられている．
項書換えシステムのもつべき望ましい性質にはいろいろなものがあるが，その中で も停止性と合流性は特に重要である．書換え規則を適用する順序や場所によらず，停 止性は無限に書換えが続かないこと，合流性は計算結果が一意であることを保証する．
停止性の検証に最もよく用いられる方法は，簡約順序と呼ばれるクラスに属する半順 序トを適当に定め，すべての書換え規則について（左辺）ト（右辺）の成立を確認するこ とであるf停止性が検証できれば，合流性の検証は容易であることが知られている）．
与えられた等式仕様をみたす完備な項書換えシステムを生成する推論手続きは完備化 手続きと呼ばれている．
従来から停止性検証及び完備化を行う推論手続きが提案されているが，その実現手 法では推論の重複などを多く生じ，非効率的である．そのような推論の高速化技法とし て，人工知能の分野においては真偽維持システム(Truth Maintenance System:TMS） が提案されている．真偽維持システムは推論手続き（問題解決器）の行った推論をその 根拠と共に保持することによって，その後の推論手続きを効率よく実行させるサブシ ステムである．ただし，推論手続きが真偽維持システムにどのような推論を与え，ま た，どのような問い合わせを行えばよいかを設計することは一般に難しく，問題領域 ごとに考察する必要がある．
本論文は，問題領域として項書換えシステムの停止性検証と完備化を対象とし，そ こに含まれる効率上の問題点を解決するために著者が設計・開発した真偽維持システ ムとそれを用いた推論手続きについて述べたものである．その成果は以下のように要 約できる．
1．従来の停止性検証手続きの問題点である，（1）無駄なバックトラック，(2)推論 の再検知，及び(3)矛盾の再検知を避けることにより，実行時間が非常に短縮さ れた．
2．複数の簡約順序を扱うことによる推論の重複を避けることができ，完備化手続 きの実行時間が非常に短縮された，
− ，525ー
久
論文の構成は以下のとおりである．
第 1章 は 序 論 で あ り ， 本 研 究 の 背 景 と そ の 目 的 を 述 べ て い る ． 第2章は本論の準備として，抽象書換えシステムをとおして項書換えシステムの諸 性質を述べている．また，項書換えシステムの停止性検証法と完備化手続きについて 紹介している．
第3章では，真偽維持システムについて述べている．特に真偽維持システムとして よ く 知 ら れ て い るATMS (Assumption‑based TMS)に つ い て 紹 介 し て い る ． 第4章では，項書換えシステムの停止性検証手続きの計算効率上の問題点を説明し，
それを解決するために著者が設計・開発した真偽維持システム及びそれを用いた検証 手続きについて述べている．項書換えシステムの停止性を検証するためには，項を構 成している演算子の集合上に，ある制約をみたす簡約順序を決定しなければならない．
この半順序は，従来の実現手法のようにバックトラック法を用いて決定することが可 能であるが，その際，無駄なバックトラック，推論の再検知，矛盾の再検知という効 率上の問題点を数多く生ずる．本章では，著者の推論手続きがいかにしてこれらの問 題 点 を 避 け て い る の か を 明 ら か に し ， そ の 有 効 性 を 論 じ て い る ． 第5章では，完備化手続きの問題点を解決するために著者が設計した真偽維持シス テム及びそれを用いた完備化手続きについて述べている．一般に，完備化手続きは等 式の集合及び適切な簡約順序を入カとし，完備な項書換えシステムを出カする．特に 本論文で対象としている手続きは，入カとして簡約順序の候補を複数個受けとり，そ の中から適切なものを自動的に選択するものとしている．この手続きは，論理的には，
入 カとして簡約順序を1っだけ 受けとる手続きを1っのプロセスとし，これらを並行 に動作させたものと等価である．しかし，その場合には，各プロセス間で多くの推論 の重複が生じ，無駄が多い．著者の考案した完備化手続きでは，その問題のために設計 された特別なデー夕構造をノ―ドとしてもつ真偽維持システムにより，それらの重複 が生じないように推論を管理することにより，この問題を解決し効率を改善している．
第 6章 で は ， 本 研 究 の 結 論 及 び 今 後 の 展 望 に つ い て 述 べ て い る ．
―526ー
学位論文審査の要旨
学 位 論 文 題 名
真偽維持システムを用いた項書換えシステムの 推論手続きに関する研究
項 書 換え シ ス テ ム は、 等 式 を 左 辺か ら 右 辺 への 書換え 規則と みなし 、項 と呼ば れる式 を書 換 え る こ とに よ っ て 計 算 を行 う 計 算 シ ステ ム であ る。 その応 用とし て、ソ フ卜ウ ェア 工学の 分 野 で は 代数 的 仕 様 記 述 や関 数 型 プ ロ グラ ミ ング に、 また、 人工知 能の分 野では 定理 自動証 明 な ど に 用い ら れ て い る 。項 書 換 え シ ステ ム に関 する 推論手 続きに は停止 性検証 や完 備化な ど が あ る が、 い ず れ も 従 来の 実 現 手 法 では 推 論 の 重 複な ど を 多 く 生じ 、 非 効 率 的 であ る 。 そ の よう な 推 諭 の 高速 化 技 法 と して 、 人 工 知能 の分野 におい ては真 偽維 持シス テムが 提案 さ れて いる。 真偽維 持シス テム は推論 手続き （問題 解決 器）の 行った 推論を その根 拠と 共に保 持 す る こ とに よ っ て 、 そ の後 の 推 論 手 続き を 効率 よく 実行さ せるサ ブシス テムで ある 。ただ し 、 推 論 手続 き が 真 偽 維 持シ ス テ ム に どの よ うな 推論 を与え 、また 、どの ような 問い 合わせ を 行 え ば よ い か を 設 計 す る こ と は 一 般 に 難 し く 、 問題 領 域 ご と に考 察 す る 必 要 があ る 。 本 揄 文は 、 項 書 換 えシ ス テ ム の 推論 手 続 き であ る停止 性検証 手続き 及び 完備化 手続き に含 ま れ る 効 率上 の 問 題 点 を 解決 す る た め に著 者 が設 計・ 開発し た真偽 維持シ ステム とそ れを用 い た新 たな推 論手続 きにつ いて 述べた もので ある。 本論 文の成 果は以 下のよ うに要 約で きる。
停 止 性検 証 に 対 し ては 、
従 来の 停 止 性検 証手続 きの問 題点 である 、（1）無 駄なパ ックト ラッ ク、(2)推論 の再検 知 、 及 び(3)矛 盾 の 再 検 知 を 避 け る こ と に よ り 、 実 行 効 率 を 改 善 し て い る 。 完 備化に対しては、
複数 の 簡 約 順 序を 扱 う こ と によ る 推 論 の 重複 を 避 け る こ とがで き、 完備化 手続き の実 行効 率 を 改 善 して い る 。
本 論 文 は6章 か ら 構 成 され て い る 。
第1章 は序 論 で あ り 、 本研 究 の 背 景 とそ の 目 的 を 述べ て い る 。
第2章 は本 論 の 準 備 と して 、 抽 象 書 換え シ ス テ ム を通 し て 項 書 換え システ ムの諸 性質を 述 べて い る 。 ま た、 項 書 換 え シス テ ム の 停 止 性検証 法と完 備化手 続きに つい て紹介 してい る。
第3章 では 、 真 偽 維 持 シス テ ム に つ いて 述 べ て い る。 特 に 真 偽 維持 システ ムとし てよく 知
― 527 ‑
東 勝
市 昇
仁
衛
侑
正
内
保
本
数
原
大 新
宮 嘉
栗
授 授
授 授
授
教
教
教
教
教
助
査
査
査
査
査
主
副
副
副
副
ら れ て い る ATMS (Assumption‑based TMS)に つ い て 紹 介 し て い る 。 第4章では、項書換えシステムの停止性検証手続きの計算効率上の問題点を説明し、それ を解決するために著者が設計・開発した真偽維持システム及びそれを用いた検証手続きにつ いて述べている。項書換えシステムの停止性を検証するためには、項を構成している演算子 の集合上に、ある制約をみたす簡約順序を決定しなければならない。この半順序は、従来の 実現手法のようにバックトラック法を用いて決定することが可能であるが、その際、無駄な バックトラック、推論の再検知、矛盾の再検知という効率上の問題点を数多く生ずる。本章 では、著者の推論手続きがいかにしてこれらの問題点を避けているのかを明らかにし、その 有効性を論じている。
第5章では、完備化手続きの問題点を解決するために著者が設計した真偽維持システム及 びそれを用いた完備化手続きについて述べている。一般に、完備化手続きは等式の集合及び 適切な簡約順序を入カとし、完備な項書換えシステムを出カする。特に本論文で対象として いる手続きは、入カとして簡約順序の候補を複数個受けとり、その中から適切なものを自動 的に選択するものとしている。この手続きは、論理的には、入カとして簡約順序を1っだけ 受けとる手続きを1つのプロセスとし、これらを並行に動作させたものと等価である。しか し、その場合には、各プロセス間で多くの推論の重複が生じ、無駄が多い。著者の考案した 完備化手続きでは、その問題のために設計された特別なデー夕構造をノ―ドとしてもつ真偽 維持システムにより、それらの重複が生じないように推論を管理することにより、この問題 を解決し効率を改善している 。
第6章 で は 、 本 研 究 の 結 論 及 び 今 後 の 展 望 に つ い て 述 べ て い る 。 これを要するに、著者は、項書換えシステムに関する推論手続きについて、その効率化の ため、真偽維持システムを用いた新たな推論システムの開発手法に関する新知見を得たもの で あ り 、 情 報 シ ス テ ム 工 学 に 対 し て 貢 献 す る と こ ろ 大 な る も の か あ る 。 よ って著者は、北海道大学 博士（工学）の学位を授与さ れる資格あるものと認める 。
‑ 528―
