古典線形論理の計算的解釈に基づく関数型言語の並列実行モデル

• Item type: Trans(1)
• 公開日: 2000-11-15
• タイトル: 古典線形論理の計算的解釈に基づく関数型言語の並列実行モデル
• タイトル / 言語: en
• タイトル: A Parallel Evaluation Model of Functional Languages Based on a Computational Interpretation of Classical Linear Logic
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 東京理科大学大学院理工学研究科
• 著者所属: 東京理科大学理工学部
• 著者所属(英): en
• 著者所属(英): Graduate school of Science and Technology, science University of Tokyo
• 著者所属(英): en
• 著者所属(英): Faculty of Science and Technology, Science University of Tokyo
• 著者名: 佐藤伸也; 杉本, 徹
• 著者名(英): Shinya, Sato; Toru, Sugimoto
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 古典線形論理は並列計算の新しい理論的基盤を与えるとして期待されている．Abramskyは並行計算のモデルの一種であるCHAMの枠組みを用いて古典線形論理の計算的解釈を与えた．Linear CHAMと名付けられたこの計算体系において，古典線形論理の証明図に対応する項表現はproof expressionと呼ばれ，cut除去手続きに相当する書き換え規則によって簡約が行われる．本稿ではこのLinear CHAMに基づく関数型言語の並列実行モデルを提案する．まず，直観主義論理の線形論理への埋め込みを用いて型付き $ｴlambda$ 計算がLinear CHAMに埋め込めることを示す．この埋め込みは型付き $ｴlambda$ 計算に定数を加えて得られる単純な関数型言語へ拡張することができる．次に，Linear CHAMの簡約を並列に実行するモデルを与える．いくつかの具体的なプログラムをLinear CHAMに変換し並列に実行した場合の台数効果を調べ，このモデルの有効性を検証する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Classical Linear Logicｴ,(CLL) is expected to give new theoretical foundation of parallel computation. Abramsky gave a computational interpretation of CLL using the framework of CHAM. In this computational system which is called Linear CHAM, proof expressions are assigned to proof trees in CLL, and they are reduced by rewriting rules which correspond to cut elimination procedures of CLL. In this paper, we propose a parallel evaluation model of functional languages based on Linear CHAM. First, we show that the typed lambda calculus is embedded into Linear CHAM by Girard's embedding of Intuitionistic Logic into Linear Logic. This result is extended to a simple functional language obtained from the typed lambda calculus by adding constants. Then, we give a parallel execution model for reductions in Linear CHAM. We demonstrate adequacy of this model with several benchmark programs by measuring improvements in performance when we translate them into Linear CHAM and execute their reductions in parallel.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 41, 号 SIG09(PRO8), p. 107-107, 発行日 2000-11-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会