WEKO3
アイテム
論理型プログラムにおける同値関係の分析
https://ipsj.ixsq.nii.ac.jp/records/30395
https://ipsj.ixsq.nii.ac.jp/records/30395b024e9aa-4ea2-4c4f-ba78-f505020383f4
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-PRO94078004.pdf (968.0 kB)
|
Copyright (c) 1995 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 1995-03-24 | |||||||
| タイトル | ||||||||
| タイトル | 論理型プログラムにおける同値関係の分析 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Analysis of Equivalence Relations between Logical Programs | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 東京農工大学工学部電子情報工学科情報工学講座 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Computer Science, Tokyo University of Agriculture and Technology | ||||||||
| 著者名 |
小谷, 善行
× 小谷, 善行
|
|||||||
| 著者名(英) |
Yoshiyuki, Kotani
× Yoshiyuki, Kotani
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 論理的なプログラム表現において、記述の間に同値関係を定義することによりプログラム代数が構成できることを示す。われわれは、述語の引数がなく、述語をメタ述語という演算子で結合することにより表されるひとつの論理型プログラム表現LONGを提案した。これを用いてプログラム代数を構成する。同値関係として、強・弱二つの同値性を定めた。前者は、非決定的に得られる計算結果の順序を含めた式の等価性を意味し、後者は順序を含めない等価性を意味する。まず、メタ述語で結び付けられた表現の間での等価性を定義から証明することにより、公理的規則群を導き出し、メタ述語の代数的性質を明らかにした。次に、これら規則を式にほどこして式を変形する手順で二つの式の等価性を証明することにより、プログラム変換を厳密に行えることを実例で示した。実例としては探索アルゴリズムを用い、非決定的記述と手続き的記述が強い等価性を持つこと等を証明した。本表現の計算モデルとしての有用性を明らかにするとともに論理的、非決定的プログラム言語における代数的手法の一方向を与えた。 | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | It is shown that program algebra can be constructed in logical program description, by defining specific equivalence relations between expressions of the description. We have proposed a logical program description. Two equivalence relations are introduced, strong and weak. The former means the equivalence of expressions in the computation which includes the temporal order to execute non-determinism. The latter allows the disorder. First, a set of axiomatic rules is derived by proving the equivalence between simple expressions generated by meta-predicates. Program transformation is shown to be constructed by applying the rules to an example, which is a set of search algorithms written in LONG. It is proved that the non-deterministic recursive algorithm of depth-first search is strongly equivalent to the procedural one of it. This description is useful as a computational model. Also the result gives a perspective of new algebraic methods of logical or non-determinstic programming languages. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN10485570 | |||||||
| 書誌情報 |
情報処理学会研究報告プログラミング（PRO） 巻 1995, 号 35(1994-PRO-078), p. 25-32, 発行日 1995-03-24 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
