- 著者
-
小谷 善行
- 出版者
- 一般社団法人情報処理学会
- 雑誌
- 情報処理学会研究報告. 記号処理研究会報告
- 巻号頁・発行日
- vol.95, no.35, pp.25-32, 1995-03-24
論理的なプログラム表現において、記述の間に同値関係を定義することによりプログラム代数が構成できることを示す。われわれは、述語の引数がなく、述語をメタ述語という演算子で結合することにより表されるひとつの論理型プログラム表現LONGを提案した。これを用いてプログラム代数を構成する。同値関係として、強・弱二つの同値性を定めた。前者は、非決定的に得られる計算結果の順序を含めた式の等価性を意味し、後者は順序を含めない等価性を意味する。まず、メタ述語で結び付けられた表現の間での等価性を定義から証明することにより、公理的規則群を導き出し、メタ述語の代数的性質を明らかにした。次に、これら規則を式にほどこして式を変形する手順で二つの式の等価性を証明することにより、プログラム変換を厳密に行えることを実例で示した。実例としては探索アルゴリズムを用い、非決定的記述と手続き的記述が強い等価性を持つこと等を証明した。本表現の計算モデルとしての有用性を明らかにするとともに論理的、非決定的プログラム言語における代数的手法の一方向を与えた。