• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

コントロール・オペレータの計算系とプログラム合成

Research Project

Project/Area Number 11780213
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionKyoto University

Principal Investigator

亀山 幸義  京都大学, 情報学研究科, 助教授 (10195000)

Project Period (FY) 1999 – 2000
Project Status Completed (Fiscal Year 2000)
Budget Amount *help
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 2000: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1999: ¥1,700,000 (Direct Cost: ¥1,700,000)
Keywordsコントロール・オペレータ / 古典論理 / プログラム抽出 / 部分継続 / プログラム合成
Research Abstract

(1)前年度までの本研究で得た多重タグを持つ部分継続に対応する型理論的体系を洗練し,CPS変換を与えた.Aarhus大学(Denmark)のOlivier Danvy,Andrzej Filinski氏ら継続/部分継続の研究者と研究討論を行い、彼らの定式化と本研究の定式化について比較検討した.この結果、簡潔なCPS変換を得る事が適切な定式化の鍵である、との共通認識を得た。
(2)新しい計算系の定式化としての部分継続の理解ではなく、論理的基礎の固まっている体系から部分継続の理解を得る事が可能ではないか、との着想を得て、体系を再度検討した。この結果、catch/throw体系やλμ計算など既存の古典論理的体系を基礎として、ある種の部分継続を説明できる事を発見した。この手法により説明がつくコントロール・オペレータは、既存のDanvy-Filinskiのshift/resetオペレータと完全には一致するものではないが、shiftオペレータが1回しかあらわれない場合には、完全に一致する意味論を持つ事を示した。多くの部分継続の使用例では、shiftオペレータはただ1回しか使われないか、あるいは、ただ1回しか使われない形に書き換え可能であるので、本研究は、かなり広い範囲の部分継続の使用例を確固とした論理の立場から説明しているものといえる。
(3)上記の論理的説明から合流性、強正規化可能性などの性質を得る事ができた。また、簡潔なCPS変換も(論理体系に対するものとして、自動的に)得られる。さらに、これら全ての性質が2階論理に対しても(自動的に)得られている、という点は特筆すべきものである。
(4)上記成果を、IFIP TCS2000とACM CW'01という2回の国際会議で発表した。

Report

(2 results)
  • 2000 Annual Research Report
  • 1999 Annual Research Report
  • Research Products

    (6 results)

All Other

All Publications (6 results)

  • [Publications] Yukiyoshi Kameyama: "A Type System for Delimited Continuations"Proc.3^<rd> JSSST Workshop on Programming and Programming Languages (PPL2000). 4-11 (2000)

    • Related Report
      2000 Annual Research Report
  • [Publications] Yukiyoshi Kameyama: "A Type-theoretic Study on Delimited Continuations"Proc.IFIP International Conference on Theoretical Computer Science (TCS2000), Lecture Notes in Computer Science. 1872. 489-504 (2000)

    • Related Report
      2000 Annual Research Report
  • [Publications] Yukiyoshi Kameyama: "Towards Logical Understanding of Delimited Continuations"Proc.3^<rd> ACM SIGPLAN Workshop on Continuations (CW'01). 27-33 (2001)

    • Related Report
      2000 Annual Research Report
  • [Publications] Masahiko Sato et al.: "A Simply Typed Context Calculus with First-Class Environments"Proc.Fifth International Symposium on Functional and Logic Programming (FLOPS2001), Lecture Notes in Computer Science. (発表予定). (2001)

    • Related Report
      2000 Annual Research Report
  • [Publications] Y.Kameyama: "A Type System for Delimited Continuations"Proc.Workshop on Prog and Prog Lang.. (発表予定). (2000)

    • Related Report
      1999 Annual Research Report
  • [Publications] Furusawa,Kameyama et al.: "On Soundness and Completeness of Simulations wrt Refinement"Proc.Workshop on Refinement&Abstraction. (発表予定). (2000)

    • Related Report
      1999 Annual Research Report

URL: 

Published: 1999-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi