プログラムの合成・変換・検証に関する知識の説明に基づく学習とリフォーメーション

1992 Fiscal Year Annual Research Report

• Project/Area Number: 04650298
• Research Institution: Hokkaido University
• Principal Investigator: 栗原 正仁 北海道大学, 工学部, 助教授 (50133707)
• Keywords: 項書換えシステム / 停止性 / リフレクション / プログラム検証 / ATMS / EBL

Research Abstract

本研究課題はEBL(説明に基づく学習)などの機械学習の技法を,プログラムの合成・変換・検証などのソフトウェア工学の分野に応用することである.いずれも,対象とするプログラミング言語として項書換えシステム(等式言語)を想定している.
研究計画の初年度である平成4年度は主として,サーベイおよび準備的研究を行ない,次のような成果を得た.いずれも,すでに国際会議,研究報告等で公表している.
1.項書換えシステムの停止性の証明を「説明」としてEBL技法を使うには,機械学習システム自身がこの問題分野(停止性証明)の背景知識を持たなければならない.この背景知識として(1)非コピー項書換えシステムまたは(2)単純停止項書換えシステムの体系を用いると,停止性の証明がモジュール化できるため,背景知識として有望であることがわかった.
2.説明により与えられる知識をATMS(仮説に基づく真理維持システム)で管理することにより,停止性の検証を効率的に行なう手法を考案した.
3.本研究の対象分野はプログラムであるため,作成するAIプログラムはプログラムをデータとしてもつことになる.特に,知識のリフォーメーションを行ない,自らを改変していくのが究極の目標である.そのためのアーキテクチャとして,最近注目を浴びている自己反映計算(リフレクション)を採用し,項書換えシステムにこの機能を付加した言語を設計し,その処理系を作成した.

Research Products

• [Publications] Masahito Kurihara: "Noncopying term rewriting and modularity of termination" Proc.Pacific Rim International Conference on Artificial Intelligence. 1. 153-159 (1992)
• [Publications] Masahito Kurihara: "Modularity of simple termination of term rewriting systems with shared constructors" Theoretical Computer Science. 103. 273-282 (1992)
• [Publications] Masahito Kurihara: "Using ATMS to efficiently verify the termination of rewrite rule programs" International Journal of Software Engineering and Knowledge Engineering. 2. 547-565 (1992)
• [Publications] Masahito Kurihara: "An algebraic specification and an object-oriented implementation of a reflective language" Proc.IMSA'92 International Workshop on Reflection and Meta-level Architecture. 1. 137-142 (1992)
• [Publications] 佐藤 崇昭: "自己反映計算機能をもつ等式プログラム処理系の実現" 電子情報通信学会技術研究報告. SS92. 69-76 (1993)