2013 Fiscal Year Research-status Report
| Project/Area Number |
24650002
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| Keywords | 古典論理 / 直観主義論理 / 簡約保存 / 表示的意味 |
|---|
| Research Abstract |
本研究の目的は、古典論理の計算系を型付ラムダ計算へ翻訳することであるが、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 である。25年度は lambda-bar-mu-tilde が持つ非決定性に関して考察する予定であったが、それを直接考えても手掛りが少ない。そこで、拡張した型付ラムダ計算に翻訳したときその振舞いが適切であるかどうかを判断するためには、lambda-bar-mu-tilde の意味を考え、その意味が拡張した型付ラムダ計算の意味に反映されているかどうかを考えることにした。しかし、意味といっても唯一に定まるわけではないので、手掛りとして以下の2つの意味を考えた。ひとつは、二重否定翻訳の考え方を使って型の意味をDCPO上で与える方法である。もうひとつは、強正規化性を証明するときに使うreducilibity setを意味を与える集合と見なすことである。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
当初予定していた、lambda-bar-mu-tilde が持つ非決定性に関する考察については、当初予想していたより困難な点が多く、さらに考察が必要である。
また、わかった部分についても論文にまとめて投稿する作業が遅れている。
|
| 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型を用いた体系を考案しているが、この体系の意味を lambda-bar-mu-tilde の意味に反映させることにより考える手掛りにする。
また、24年度に予定していたが十分にはできなかった、明示的代入を持つ体系に関する考察とそれを基にして古典論理の計算体系を抽象機械に翻訳する方法も引き続いて考えたい。そのために、現在並行して研究を行っているラムダ項の表現についての成果を利用して、抽象機械の構成に役立てる。
|
| Expenditure Plans for the Next FY Research Funding |
物品購入費の予定との差により生じた。
物品購入費の補充にあてる。
|
