Last modified on 2001.10.26.
本研究は、前者の段階を行う枠組みを提案する。
従来、逐次化が定式化されることはほとんど無かった。 そのため、個々の最適化技術の正当化は、 しばしばアドホックにしか行うことができなかった。 本研究は、それらの最適化技術の正当化を統一的に行うための 解析の枠組みを提案するものであり、 個々の解析を否定するものではないということは、 当然理解されなければならない。
振舞いを正確に定義するには、 対象とする言語の形式的な定義が必要となる。 振舞いの定義は後で行う。
下のGHCプログラムに相当する計算は、 上のように表現される。
定義した言語の特徴は以下の通り：
次のスライドのように、 プロセスの意味を述べるためにCCPの研究が使用できる。
i (X ) を、 青い四角で囲んだ制約から成る集合として定義する。
変数を除去する具体的な方法の説明は割愛する。
直感的には、 左のエージェントは右のエージェントに コンパイルされても問題無いということを表す。
この例では X=1 という特定の入力を仮定した場合のプロセスの振舞いを扱っていることに注意する。
(I4) は、以下の解析のための統一的な枠組みを与えている：
圧縮はインタフェース上の推論によって実現される。 個々のインタフェース上の推論の正当化は、 インタフェースの定式化に基づき操作的意味論のレベルで、 あらかじめ証明しておくことができることに注意する。
圧縮することにより、仮定を集約できるようになる。 集約によって仮定が強すぎるようになった場合、 解析の結果が役に立たなくなるため、 生成した中間コードは利用できなくなる。 この場合は逐次化しない通常の実行を行うことになる。 つまり、この集約によってプログラムがデッドロックするようにはならない。 逐次化の説明は次のスライドで行う。
インタフェース上の解析によって、 インタリーブの可能性と手順を発見できる。
中間コードの最適化を正当化するには、 中間コードを形式的に定義する必要がある。 これは今後の課題である。
［ 戻る ］