• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2014 年度 実施状況報告書

古典論理計算系から直観主義論理計算系への翻訳

研究課題

研究課題/領域番号 24650002
研究機関千葉大学

研究代表者

桜井 貴文  千葉大学, 理学(系)研究科(研究院), 教授 (60183373)

研究期間 (年度) 2012-04-01 – 2016-03-31
キーワード古典論理 / 直観主義論理 / intersection-union / intersection-product
研究実績の概要

本研究の目的は、古典論理の計算系を型付ラムダ計算へ翻訳することであるが、24年度までで、古典論理の計算系 lambda-bar-mu の型付ラムダ計算への翻訳を定義し、さらに lambda-bar-mu-tilde-CBN および lambda-bar-mu-tilde-CBV の型付ラムダ計算への翻訳を定義した。これらの翻訳は簡約を保存する簡単な翻訳を合成することにより定義することができた。特に lambda-bar-mu-tilde-CBN の翻訳については、従来のものとは異なり簡約を保存するという性質を持っている。

lambda-bar-mu-tilde-CBN および lambda-bar-mu-tilde-CBV はlambda-bar-mu-tilde の部分計算体系であるが、lambda-bar-mu-tilde は非決定性を持つので計算体系として決定性を持つように制限されたものが lambda-bar-mu-tilde-CBN および lambda-bar-mu-tilde-CBV である。26年度も引き続きこれら3つのシステムについて考察する予定であったが、その予定を変更して菊池健太郎氏との共同研究により古典論理に基づく新たな型理論を構築した。そしてその体系を論文 ``A Translation of Intersection and Union Types for the λμ-Calculus'' (APLAS 2014) として発表した。この型理論は intersection-union型に基づいた型理論であり、この論文では S. van Bakel, F. Barbanera, and U. de'Liguoro による型理論との関係を明らかにしている。S. van Bakelらによる型理論はintersection-product型に基づく型理論であり、一見複雑なものであるが、lambda-mu をある種のCPS変換によって変換したものであると見なすと自然に理解できることがわかった。

現在までの達成度 (区分)
現在までの達成度 (区分)

3: やや遅れている

理由

当初予定していた、lambda-bar-mu-tilde が持つ非決定性に関する考察については、当初予想していたより困難な点が多いことがわかった。そのために、最初に予定していた体系とは少し異なる体系について共同研究を行ない、その手掛りにしようとしている。

また、lambda-bar-mu-tilde-CBN および lambda-bar-mu-tilde-CBV に関してわかった部分を論文にまとめて投稿する作業が遅れている。

今後の研究の推進方策

lambda-bar-mu-tilde が持つ非決定性に関する考察については、継続した考察を行なうために、その意味についてさらに考える。概要の所で述べた翻訳から導かれる lambda-bar-mu-tilde-CBN および lambda-bar-mu-tilde-CBV の意味は、continuationに相当する部分をproduct型を使って追加するような構造になっているが、その部分に関して以下のように別の考え方を導入する。研究実績の概要で述べたように、現在 lambda-bar-mu-tilde の変種である lambda-mu でintersection-union型の体系を構築し、それをintersection-product型に基づく体系に変換することができることを示した。この変換を lambda-bar-mu-tilde にも適用できるかどうかを考える手掛りにすることにより、lambda-bar-mu-tilde に対する考察を深める。

また、24年度に予定していたが十分にはできなかった、明示的代入を持つ体系に関する考察とそれを基にして古典論理の計算体系を抽象機械に翻訳する方法も引き続いて考えたい。そのために、現在並行して研究を行っているラムダ項の表現についての成果を利用して、抽象機械の構成に役立てる。

次年度使用額が生じた理由

本研究課題に関して菊池健太郎氏と共同研究を行ない、APLAS 2014という国際会議で論文を発表した。そのとき同じテーマで研究を行っているImperial College LondonのSteffen van Bakel教授とコンタクトを取り、本研究費を使用して招聘することになった。当初本年度中に来日してもらう予定であったが、先方の都合により本年度は来日できなくなった。

次年度使用額の使用計画

来年度中のvan Bakel教授の来日を実現するため、来日できるよう引き続き予定を調整してもらっている最中である。本年度の来日用の費用として使用予定であった額を未使用額とし、van Bakel教授が次年度に来日したときの費用に充てる。

  • 研究成果

    (2件)

すべて 2014

すべて 雑誌論文 (1件) (うち査読あり 1件、 謝辞記載あり 1件) 学会発表 (1件)

  • [雑誌論文] A Translation of Intersection and Union Types for the λμ-Calculus2014

    • 著者名/発表者名
      K. Kikuchi, T. Sakurai
    • 雑誌名

      Lecture Note in Computer Science (Proceedings of 12th Asian Symposium on Programming Languages and Systems)

      巻: LNCS 8858 ページ: 120 -- 139

    • DOI

      10.1007/978-3-319-12736-1_7

    • 査読あり / 謝辞記載あり
  • [学会発表] A Translation of Intersection and Union Types for the λμ-Calculus2014

    • 著者名/発表者名
      K. Kikuchi, T. Sakurai
    • 学会等名
      Fifth International Workshop on Classical Logic and Computation (CL&C'14)
    • 発表場所
      Vienna, Austria
    • 年月日
      2014-07-13 – 2014-07-13

URL: 

公開日: 2016-06-03  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi