2014 Fiscal Year Research-status Report
| Project/Area Number |
24650002
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | 古典論理 / 直観主義論理 / intersection-union / intersection-product |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、古典論理の計算系を型付ラムダ計算へ翻訳することであるが、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変換によって変換したものであると見なすと自然に理解できることがわかった。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
当初予定していた、lambda-bar-mu-tilde が持つ非決定性に関する考察については、当初予想していたより困難な点が多いことがわかった。そのために、最初に予定していた体系とは少し異なる体系について共同研究を行ない、その手掛りにしようとしている。
また、lambda-bar-mu-tilde-CBN および lambda-bar-mu-tilde-CBV に関してわかった部分を論文にまとめて投稿する作業が遅れている。
|
| Strategy for Future Research Activity |
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年度に予定していたが十分にはできなかった、明示的代入を持つ体系に関する考察とそれを基にして古典論理の計算体系を抽象機械に翻訳する方法も引き続いて考えたい。そのために、現在並行して研究を行っているラムダ項の表現についての成果を利用して、抽象機械の構成に役立てる。
|
| Causes of Carryover |
本研究課題に関して菊池健太郎氏と共同研究を行ない、APLAS 2014という国際会議で論文を発表した。そのとき同じテーマで研究を行っているImperial College LondonのSteffen van Bakel教授とコンタクトを取り、本研究費を使用して招聘することになった。当初本年度中に来日してもらう予定であったが、先方の都合により本年度は来日できなくなった。
|
| Expenditure Plan for Carryover Budget |
来年度中のvan Bakel教授の来日を実現するため、来日できるよう引き続き予定を調整してもらっている最中である。本年度の来日用の費用として使用予定であった額を未使用額とし、van Bakel教授が次年度に来日したときの費用に充てる。
|
