古典線形論理型プログラミング言語の静的解析の一手法について

• Item type: Trans(1)
• 公開日: 2000-06-15
• タイトル: 古典線形論理型プログラミング言語の静的解析の一手法について
• タイトル / 言語: en
• タイトル: A Static Analysis Method for a Classical Linear Logic Programming Language
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 神戸大学大学院自然科学研究科
• 著者所属: 奈良工業高等専門学校
• 著者所属: 神戸大学工学部
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Technology, Kobe University
• 著者所属(英): en
• 著者所属(英): Nara National College of Technology
• 著者所属(英): en
• 著者所属(英): Faculty of Engineering, Kobe University
• 著者名: 姜京順; 番原, 睦則; 田村, 直之
• 著者名(英): Kyoung-Sun, Kang; Mutsunori, Banbara; Naoyuki, Tamura
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿では古典線形論理に基づいた論理型プログラミング言語の静的解析方法を提案する．線形論理に基づく論理型プログラミング言語としては Lolli，LinLog，LO，Lygon，Forumなどが提案されている．特に，Forumは古典線形論理に対し完全である論理型プログラミング言語である．しかし，Forumのプログラムの証明探索は非決定性が非常に大きいため，静的解析することでプログラムの実行前に証明不可能なシーケントを取り除くことは重要である．Andreoliらは古典線形論理に基づく論理型プログラミング言語LOの静的解析方法を提案している．しかし，その方法は「リソースを意識した」線形論理型プログラミング言語で最も有用な演算子である乗法的論理積の解析には適用できないのである．そこで，我々は乗法的論理和，含意に加えて乗法的論理積を解析できる静的解析方法を考案した．我々の方法ではまず，プログラムと証明すべきゴールが与えられたら，そのシーケントのあり得る全ての証明を1つのAND‐ORグラフに表現する．そして，データフロー解析のための前方伝搬と後方伝搬を繰り返すことによって証明不可能な節点をグラフから取り除いていく．本稿の静的解析方法に基づくプロトタイプ解析機を開発し，実際にForumで書かれたソーティングプログラムを解析した結果，6要素のソーティングに対し，解析していない時の実行速度に比べ1000倍以上遠くなった．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We propose a new static analysis method applicable to a classical linear logic programming language. Andreoli et al. proposed a static analysis method for a classical linear logic programming language LO, but their method cannot handle multiplicative connectives, which can be seen as the most important connective for a resource-sensitive feature of linear logic. Our method, in contrast, covers multiplicative conjunctions in addition to multiplicative disjunctions and linear implications. Abstract proof graph, which is an AND-OR graph representing all possible sequent proofs, is constructed from a given program and goal sequent. The graph can be repeatedly refined by propagating information to remove unprovable nodes from the graph. We applied the result of our prototype analyzer to a sorting program written in Forum. The sorting program was improved more than 1000 times faster for sorting 6 elements.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 41, 号 SIG04(PRO7), p. 42-55, 発行日 2000-06-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会