2020 Fiscal Year Research-status Report
| Project/Area Number |
20K03712
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
鹿島 亮 東京工業大学, 情報理工学院, 准教授 (10240756)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | ２階型付けラムダ計算 / 完全性 |
|---|
| Outline of Annual Research Achievements |
本研究課題である中間２階命題論理の基本は直観主義２階命題論理である。そして直観主義２階命題論理は２階型付きラムダ計算と実質的に同じである（カリー・ハワード同型対応）。このような背景のもとで、２階型付きラムダ計算の完全性に関する研究をおこなった。
一般に論理の体系（Lと呼ぶ）について、論理式の「意味」を適切に定義した上で、論理式に関する２条件「恒真である」と「Lで導出できる」が同値になることを、Lの完全性と呼ぶ。完全性は論理の体系に求めらる最も基本的な性質である。
ところが型付きラムダ計算の体系については、β同値な項を同一視するという特別な規則を加えた体系については完全性が知られていたが、特別な規則を入れない最も基本的な体系（単純型付きラムダ計算）については完全性が未解決であった。そこで文献[1]（研究協力者松田直祐ほか１名との共同研究）でこの問題を解決した。具体的には、ラムダ項の冪集合を用いて Term Space という自然な意味を定めて完全性を示した。さらにこの結果を、私の学生との共同研究によって２階型付きラムダ計算に拡張した（投稿論文準備中）。ただしここでの２階型付きラムダ計算の体系には、η同値な項を同一視するという特別な規則を追加してある。これはTerm Space を自然に定義するための必然的な追加であるのだが、この追加規則なしの最も基本的な体系に対する完全性は今後の研究課題である。
[1] Ryo Kashima, Naosuke Matsuda, and Takao Yuyama: Term-Space Semantics of Typed Lambda Calculus, Notre Dame Journal of Formal Logic 61[4], pp.591-600 (2020).
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
先述の文献[1]は2019年度後半から2020年度前半にかけての業績であり、実際には2019年度に実施された複数の研究集会において共同研究者松田と対面で議論することで研究が開始され、その後2020年度に入ってからも松田（そして遅れて研究に加わった湯山）との共同で研究が進んだ。このようにラムダ計算との関わりで中間２階命題論理を研究することは、計画通りに進んでいる。
一方で、中間１階述語論理との関わりで中間２階命題論理を研究するという計画については、まったく進んでいない。この大きな理由は新型コロナウイルス感染症である。2020年度に入り感染症対策により他研究者と対面で議論することが困難になった（先述の２階型付きラムダ計算に関する結果は私の研究室の学生との共同研究なので、ある程度の制約はあるが対面で議論が可能であった）。こんな状況で、当初計画されていた研究協力者と対面で議論することが不可能になり、特に中間１階述語論研究の第一人者である鈴木信行（静岡大）との議論ができないことが、本研究が進んでいない大きな理由である。
|
| Strategy for Future Research Activity |
一般に共同研究は、ある程度問題が明確化した段階ではオンラインでの遠隔議論やメールのやりとりによって効果的に進めことができる。しかし研究の端緒ではもやもやしたアイデアをざっくばらんに話し合う必要があり、それを行うのは対面での議論が圧倒的に有利である。研究集会の参加についても同様で、現状はすべての研究集会がオンライン開催であり、これは海外の研究集会に気軽に参加できるという利点もあるが、やはり直に見聞きするのとは密度が異なる。
このような状況で、先述の２階型付きラムダ計算に関する結果の発展を身近な学生と議論しながら進めていくことが、直近に推進可能な研究課題となる。中間１階述語論理方向からのアプローチについては、共同研究者との遠隔での議論を随時行い、できる範囲で始めていく。
|
| Causes of Carryover |
新型コロナウイルス感染症対策により対面での研究打ち合わせや研究集会への対面参加が不可能になったことにより、旅費がまったく使用できなかった。代わりにオンラインでの議論のための機器を購入した。
2021年度後半には旅費使用が可能なることを期待しており、そうなれば当初の計画通りに使用していく計画である。
|
