制御フローの合流のための計算系

• Item type: Trans(1)
• 公開日: 2008-10-27
• タイトル: 制御フローの合流のための計算系
• タイトル / 言語: en
• タイトル: A Calculus for Merging Control Flows
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 東北大学電気通信研究所
• 著者所属: 東北大学電気通信研究所
• 著者所属(英): en
• 著者所属(英): Research Institute of Electrical Communication, Tohoku University
• 著者所属(英): en
• 著者所属(英): Research Institute of Electrical Communication, Tohoku University
• 著者名: 上野, 雄大; 大堀, 淳
• 著者名(英): Katsuhiro, Ueno; Atsushi, Ohori
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，制御フローの合流を扱うための計算系を提案し，その計算系から導出される中間表現を構築する．制御フローの合流は，条件式などをコンパイルするうえで必須の機構である．たとえば，3 番地コードを用いた手続き型言語のコンパイラでは，条件式は，各分岐先のコードの実行の後，同一のラベルにジャンプするコードに翻訳される．しかしながら，関数型言語の中間表現として使用される継続渡し形式 （CPS） や A-正規形などでは，制御フローの合流の機構が含まれていないため，条件式などを機械的に翻訳すると，分岐の後に続く継続が各分岐に複製されてしまう．この問題は，それら中間表現に対応する計算系に，分岐後の制御フローの合流に相当する規則を追加することで解決できるはずである．本論文では，この洞察に基づき，著者の 1人によって示されたシーケント計算と A-正規形の対応を洗練し，論理和に対する左規則が唯一の前提（上式）を持つようなシーケント計算を構築する．この結果から，証明論的意味付けに立脚し，かつ制御フローの合流を取り扱うことができるコンパイラの中間表現と，その言語へのコンパイルアルゴリズムを導く．本論文の結果は関数型言語の実用的なコンパイラのより系統的な実現を可能にするものである． Standard ML の拡張言語である SML# のコンパイラの中間表現の 1 つは，この計算系に基づいて設計され，その中間言語へのコンパイルフェーズは本論文で示すコンパイルアルゴリズムを基礎に実装されている．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: This article proposes a new calculus for representing control flow merge, which is necessary for compiling case or conditional expressions, and develops a compiler intermediate language based on this calculus. Existing formalisms such as A-normal forms or CPS do not contain a mechanism for control flow merge. As a consequence, in these formalisms, mechanical application of a compilation algorithm to a conditional expression results in duplication of its continuation. This seems to be due to the lack of proper formalism for representing conditional expressions in the underlying calculi. This article refines the correspondence between the sequent calculus and A-normal forms shown by one of the authors, and develops a proof system where control flow merge is directly represented as a logical rule for disjunction. These results yield a term calculus suitable for compiler intermediate representations and a compilation algorithm that deals with control flow merge. This approach scales up to intermediate languages for practical compilers. The proposed calculus and the compilation algorithm have been successfully used in implementation of SML# - an extension of the Standard ML.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 1, 号 3, p. 19-33, 発行日 2008-10-27
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会