並行論理型言語における同期ポイントの移動の安全性について

• Item type: Trans(1)
• 公開日: 2000-03-15
• タイトル: 並行論理型言語における同期ポイントの移動の安全性について
• タイトル / 言語: en
• タイトル: On the Safety of Moving Synchronization Points in Concurrent Logic Programming Languages
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 早稲田大学大学院理工学研究科
• 著者所属: 早稲田大学理工学部
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Engineering, Waseda University
• 著者所属(英): en
• 著者所属(英): School of Science and Engineering, Waseda University
• 著者名: 加藤, 紀夫; 上田, 和紀
• 著者名(英): Norio, Kato; Kazunori, Ueda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 並行論理型言語では，プロセス間の同期は変数に対する入出力によって行われる．したがって入力が不完全なために何も出力できないプロセスは，必要な入力を待った後で実行すればよいであろう．このプロセス変換は同期ポイントの移動と呼ばれており，プロセスの最適な実行順序を計算するために使用して実装の最適化に応用可能である．この手法を実装するには，プロセスが何かを出力するために必要な入力を求める必要があるが，並行論理型言語のような非決定的な枠組みにおいて，それを正確に求めることは一般には難しい．そこで本論文では，何らかの値に具体化されている必要のある変数を指摘する抽象実行の方法を紹介し，その正当性を論じる．発散も失敗もしないプロセスは，同期ポイントの移動の前後で表示的意味が保存されることを証明した．正当性を論じるために使用した表示的意味論は，操作的意味論におけるプロセスの入出力の時系列を集めたものであり，その定義の簡素さによって表示的意味の等価性の証明を容易にしている．また，述語呼び出しの書き換え時に起こる変数名の付け替えについて，式の上で新しい変数を入手可能にする変数変換と呼ばれる記法を導入し，いくつかの性質を証明した．それを利用して構成した，プロセスの書き換えの親子関係を明示的に残す操作的意味論についても説明する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In concurrent logic programming languages, processes synchronize through inputs and outputs on the global store. Therefore, a process that requires some input to produce any output may postpone its execution until the necessary input becomes available. Such transformation, which we call the moving of synchronization points, helps us to determine the order of reductions within a process, and is applicable to compiler optimization. To implement this method, it is necessary to calculate inputs a process requires for producing any output. In the nondeterministic paradigm like concurrent logic programming, however, it might seem hard to calculate them precisely. This paper presents an abstract execution method that finds input variables of a process that are required to have been instantiated, and proves its correctness. For a process that neither diverges nor aborts, we have proved that the denotation of the process does not change after moving synchronization points. The denotational semantics we used to justify our method derives from the set of execution sequences of a process in the operational semantics, whose simplicity of definition facilitates the proofs of process equivalences. We have also introduced a notation, which we call variables translation, to express the variable renamings occurring in a reduction. The notation enables us to bring new variables freely. The paper also shows how to use the notation to construct the operational semantics which keeps track of parent/children relationship between processes.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 41, 号 SIG02(PRO6), p. 13-28, 発行日 2000-03-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会