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

情報処理学会 Web Site

書誌事項

タイトル別名
  • セイギョ フロー ノ ゴウリュウ ノ タメ ノ ケイサンケイ
  • A Calculus for Merging Control Flows

この論文をさがす

抄録

本論文では，制御フローの合流を扱うための計算系を提案し，その計算系から導出される中間表現を構築する．制御フローの合流は，条件式などをコンパイルするうえで必須の機構である．たとえば，3 番地コードを用いた手続き型言語のコンパイラでは，条件式は，各分岐先のコードの実行の後，同一のラベルにジャンプするコードに翻訳される．しかしながら，関数型言語の中間表現として使用される継続渡し形式 （CPS） や A-正規形などでは，制御フローの合流の機構が含まれていないため，条件式などを機械的に翻訳すると，分岐の後に続く継続が各分岐に複製されてしまう．この問題は，それら中間表現に対応する計算系に，分岐後の制御フローの合流に相当する規則を追加することで解決できるはずである．本論文では，この洞察に基づき，著者の 1人によって示されたシーケント計算と A-正規形の対応を洗練し，論理和に対する左規則が唯一の前提（上式）を持つようなシーケント計算を構築する．この結果から，証明論的意味付けに立脚し，かつ制御フローの合流を取り扱うことができるコンパイラの中間表現と，その言語へのコンパイルアルゴリズムを導く．本論文の結果は関数型言語の実用的なコンパイラのより系統的な実現を可能にするものである． Standard ML の拡張言語である SML# のコンパイラの中間表現の 1 つは，この計算系に基づいて設計され，その中間言語へのコンパイルフェーズは本論文で示すコンパイルアルゴリズムを基礎に実装されている．

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.

収録刊行物

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ