| 研究課題/領域番号 |
24650002
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | 古典論理 / C(G)PS変換 / 簡約保存 |
|---|
| 研究概要 |
本研究の目的は、古典論理の計算系を型付ラムダ計算へ翻訳することであるが、まず、古典論理の計算系 lambda-bar-mu の型付ラムダ計算への翻訳について考察した。そのために、lambda-bar-mu を lambda-conj-neg に翻訳し、lambda-conj-neg をラムダ計算に翻訳する変換を考えた。それぞれは簡約を保存する簡単な翻訳であるが、それらを合成すると既知のCPS変換になることがわかった。さらに lambda-mu を同じ考え方で型付ラムダ計算に翻訳することを考えたが、lambda-mu に新しい規則を加えることにより lambda-conj-neg への簡約を保存する簡単な翻訳を定義することができた。これは従来のC(G)PS変換を使った翻訳をわかりやすく構成し直したものとみなすことができる。
次に lambda-bar-mu-tilde-CBN の型付ラムダ計算への翻訳について考察した。CurienとHerblinによる翻訳は簡約を保存せず、Espirito Santoらによる変換は直観主義に制限された変換である。本研究では、lambda-bar-mu-tilde-CBN をまず lambda-conj-neg に翻訳しさらに lambda-conj-neg を型付ラムダ計算に翻訳することにより新しい翻訳を定義することができた。これはCGPS変換を使わない新しい変換であり、簡約を保存するという今までにない性質を持っており、さらにこの変換からEspirito Santoらによる変換を得られることもわかった。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
当初予定していた、lambda-bar-mu-tilde が持つ非決定性に関する考察については、まだ不明な部分が残り、さらに考察が必要である。
また、わかった部分についても論文にまとめて投稿する作業が遅れている。
|
| 今後の研究の推進方策 |
lambda-bar-mu-tilde が持つ非決定性に関する考察については、継続した考察を行なう。
明示的代入を持つ体系の中では一番単純な体系である lambda-x に関する研究を行なう。「lambda-x において型付けできる項は強正規化可能である」という定理はよく知られているが、その証明は 明示的代入を持たない単純型付ラムダ計算の場合に比べて複雑である。現在、lambda-x の強正規化性の証明の新しい方法を開発してそれを完成させている所であるが、その方法を使うと今までになかった明示的代入の合成規則 t<y:=r><x:=s> → t<x:=s><y:=r<x:=s>> if x ∈ FV(r) を加えても強正規化性を証明できる。実際にはさらに強く、簡約列の中で t<y:=r><x:=s> → t<x:=s><y:=r> if not (x ∈ FV(r)) という明示的代入交換規則を有限回しか続かないという条件で使うなら、その簡約列は有限であるということを証明する。そして逆に、この意味で強正規化可能であるならばintersection型を用いて拡張した体系で型付け可能であることも証明する。
このようにして作った明示的代入の体系を基にして、古典論理の計算体系を抽象機械に翻訳する方法を考えるのが、その次の目標である。
|
| 次年度の研究費の使用計画 |
作った体系についての意見を求めるために、明示的代入に関して共同で研究を行なってきた京都大学の佐藤雅彦名誉教授、五十嵐淳准教授、中澤巧爾助手、筑波大学の亀山幸義教授を訪問し、講究を行う。24年度は、こちらの都合で共同研究者である佐藤雅彦名誉教授に千葉大に来学してもらうばかりだったので、25年度はその分を使用する予定である。さらに、他大学の研究者と討論をしたり、学会や研究集会に出席し発表をするための旅費や、資料とするための雑誌等を購入するための費用などが必要となる。また、24年度に購入予定であった計算機は25年度に購入し、さらに補助的に使うためにモバイル計算機および関連する消耗品を購入する。
|
