首页    期刊浏览 2025年04月16日 星期三
登录注册

文章基本信息

  • 标题:対称λ計算の基礎理論
  • 本地全文:下载
  • 作者:阪上 紗里 ; 浅井 健一
  • 期刊名称:コンピュータ ソフトウェア
  • 印刷版ISSN:0289-6540
  • 出版年度:2009
  • 卷号:26
  • 期号:2
  • 页码:2_3-2_17
  • DOI:10.11309/jssst.26.2_3
  • 出版社:Japan Society for Software Science and Technology
  • 摘要:

    「プログラムの残りの計算」を表す継続を扱う為の基礎言語体系として,対称λ計算(Symmetric λ-calculus, SLC)がFilinskiによって提案されている.SLCにおいては項と継続が完全に対称な形をしており,項を扱うのと同じように継続を扱うことができる.そのため,項と継続を統一的に議論するのに適していると思われるが,これまでSLCについての研究はほとんどなされていない.ここでは,まずSLCをsmall step semanticsで定式化し直し,型付き言語の基本的な性質であるProgressとPreservationを満たすことを証明する.次に,SLCが継続計算を議論・表現するのに適していることを示すため,(1) FelleisenのCオペレータを含むcall-by-value言語,ΛC計算,および(2) Parigotのcall-by-name λμ計算が,どちらも自然にSLCに変換できることを示す.近年call-by-valueとcall-by-nameの双対性が項と継続の対称性と絡めて注目されているが,ここでの結果はそれに対する洞察を与えるものと期待される.

国家哲学社会科学文献中心版权所有