限定継続機構とfutureを持つ計算体系の透過的意味論

機関リポジトリ 情報処理学会 HANDLE オープンアクセス

書誌事項

タイトル別名
  • Transparent Semantics of a Calculus with Delimited Control and Future

この論文をさがす

抄録

継続機構は，種々の制御構造からモジュラで簡潔なウェブアプリケーションの記述まで，多岐にわたる応用を有する．並列計算による高性能化への要求が高まっている今日，継続機構を用いたプログラムを並列化するのは自然な要求である一方，逐次計算で考案された継続機構の並列化は困難な課題である．Moreauは，call/ccとfutureを持つ計算体系を提案し，並列意味論が逐次意味論と一致することを証明したが，彼の体系ではcall/ccを実行するとプログラム全体が逐次化されるという問題があった．本論文では，制御が及ぶ範囲をプログラムの一部に限定する継続機構を提供するshift/resetとfutureを持つ体系を提案し，先行研究の問題を解決した．また，提案する体系の意味論を逐次抽象機械と並列抽象機械によって与え，両者の意味が一致することを証明した．

Control operators for continuations have many applications such as implementation of various control structures, and modular description of web applications. It is a natural, but hard problem to parallelize the execution of programs with control operators due to the sequential nature of continuations. Moreau proposed a calculus with call/cc and future, and proved that parallel execution yields the same result as sequential execution does for his calculus. However, his solution is not fully satisfactory, since call/cc captures an unlimited continuation, and once it is called, the whole program must be executed sequentially. This paper presents a calculus with future and delimited-control operators shift/reset, which give an access to delimited continuation, part of the rest of computation. We define the semantics of the calculus in two ways by sequential and parallel abstract machines, and prove that these two semantics coincide.

収録刊行物

関連プロジェクト

もっと見る

キーワード

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

問題の指摘

ページトップへ