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

1993 Fiscal Year Annual Research Report

• Project/Area Number: 04650298
• Research Institution: Hokkaido University
• Principal Investigator: 栗原 正仁 北海道大学, 工学部, 助教授 (50133707)
• Keywords: 項書換え系 / 完備化 / 真偽維持システム / プログラム合成 / 学習

Research Abstract

本年度は,3年間で計画されている本研究の第2年度であり,主としてプログラム合成に関する知識の説明に基づく学習について研究し,実験的なソフトウェアを構築した.また,次年度で予定されているプログラム変換に関する知識の説明に基づく学習の準備的な研究を行なった.その研究成果の一部は,本報告書の「11.研究発表」に記載した3編の論文で発表した.以下,各論文に対応させて,その概要を箇条書きで述べる.
1.説明に基づく学習の研究は,通常,一階述語論理で表現された知識を対象にしてその理論が構築されている.ところが,本研究では項書換えシステムを対象としているため,知識表現言語は等式論理である.本研究成果は,この2つの論理をつなごうとした際に得られた副産物である.一階述語論理で良く知られた自然数とその計算の表現が,等式論理と関連付けられている.
2.Knuth-Bendixの完備化手続きは,与えられた等式仕様を満たす完備なプログラム(項書換えシステム)を生成するプログラム合成手続きと解釈できる.しかし,この手続きを効果的に実行するためには,停止性を保証するための適切な半順序を決めなければならない.本研究では,複数の半順序のもとでの完備化手続きを提案し,それを効率良く実行するために,完備化の推論結果を説明とともに真偽維持システムATMSで管理する手法を設計した.推論系はATMSの学習結果を効果的に利用することにより,効率良く実行できる.
3.プログラム変換の研究においては,プログラムをデータとみなして,手続きが構築される.本研究では,項書換えシステム(TRS)をデータとみる表現およびTRSで記述されたプログラムが動的に自分自身の一部を変換するような仕組みを自己反映計算の枠組みとして与えた.

Research Products

• [Publications] 栗原正仁: "Another representation of integers in logic" 情報処理学会論文誌. 34. 536-538 (1993)
• [Publications] 近藤久: "ATMSのデータ構造に基づいた複数の簡約順序を扱う完備化手続き" 北海道大学工学部研究報告. 166. 35-44 (1993)
• [Publications] 栗原正仁: "項書換えシステムにおける自己反映計算" 北海道大学工学部研究報告. 167. 57-66 (1994)