2026-05-12T07:13:16Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00016935 2025-01-22T23:36:16Z 934:935:978:980

古典線形論理型プログラミング言語の静的解析の一手法について A Static Analysis Method for a Classical Linear Logic Programming Language 姜京順 番原, 睦則 田村, 直之 Kyoung-Sun, Kang Mutsunori, Banbara Naoyuki, Tamura 通常論文 本稿では古典線形論理に基づいた論理型プログラミング言語の静的解析方法を提案する．線形論理に基づく論理型プログラミング言語としては　Lolli，LinLog，LO，Lygon，Forumなどが提案されている．特に，Forumは古典線形論理に対し完全である論理型プログラミング言語である．しかし，Forumのプログラムの証明探索は非決定性が非常に大きいため，静的解析することでプログラムの実行前に証明不可能なシーケントを取り除くことは重要である．Andreoliらは古典線形論理に基づく論理型プログラミング言語LOの静的解析方法を提案している．しかし，その方法は「リソースを意識した」線形論理型プログラミング言語で最も有用な演算子である乗法的論理積の解析には適用できないのである．そこで，我々は乗法的論理和，含意に加えて乗法的論理積を解析できる静的解析方法を考案した．我々の方法ではまず，プログラムと証明すべきゴールが与えられたら，そのシーケントのあり得る全ての証明を1つのAND‐ORグラフに表現する．そして，データフロー解析のための前方伝搬と後方伝搬を繰り返すことによって証明不可能な節点をグラフから取り除いていく．本稿の静的解析方法に基づくプロトタイプ解析機を開発し，実際にForumで書かれたソーティングプログラムを解析した結果，6要素のソーティングに対し，解析していない時の実行速度に比べ1000倍以上遠くなった． 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. journal article 情報処理学会 2000-06-15 application/pdf 情報処理学会論文誌プログラミング（PRO） SIG04(PRO7) 41 42 55 1882-7802 AA11464814 https://ipsj.ixsq.nii.ac.jp/record/16935/files/IPSJ-TPRO4104006.pdf jpn