|
平成15-16年度の科学研究費補助研究「カテゴリカル・リダクション」においてわれわれは、直観主義線形論理の圏論モデル上に計算体系を構築した。ラムダ計算と圏論との間に親密な関係があることは半世紀以上前から知られていたが、ラムダ計算のもっている計算の概念が圏論の側でどのように反映されるべきなのかは、まだほとんど未解明であった。われわれの計算体系は、圏論の側にも計算の機構を導入することで、ラムダ計算と圏論とのギャップを埋めようという試みである。この方向の研究では、成功を収めた先行研究がないので、得られた計算体系の優劣を比較するような対象がない。そこで、計算体系の正当性を主張するためには、いろいろな角度から、その性質を検討する必要がある。そのような性質の中で重視される伝統的なものは、正規化性やChurch-Rosser性である。すでに弱正規化性についてはある程度の結果を得ている。しかしそこで用いられている議論はあまりにコンビナトリアルに複雑すぎるので、簡略化の可能性を検討した。一つの方向は、直観主義線形論理のかわりに古典的線形論理にスイッチすることである。そのような伝統的な性質以外にも、操作的意味論との関連も検討した。圏論モデル上の体系は、ラムダ計算における簡約よりも細部のコントロールが可能なので、操作的意味論で重視される環境の共有や、値の評価の単一性などが捉えられる可能性があると考えているからである。また、関連する周辺分野の研究として、エキゾチック・パラメトリシティとでも呼ぶべきパラメトリシティ原理の変種、特に線形パラメトリシティや、継続のCPS変換による意味論の周辺の性質についても研究した。
|
