|
本研究の目的は、古典論理の計算系を型付ラムダ計算へ翻訳することであるが、まず、古典論理の計算系 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 をまず lambda-conj-neg に翻訳しさらに lambda-conj-neg を型付ラムダ計算に翻訳することにより新しい翻訳を定義することができた。これはCGPS変換を使わない新しい変換であり、簡約を保存するという今までにない性質を持っており、さらにこの変換からEspirito Santoらによる変換を得られることもわかった。
菊池健太郎氏との共同研究により intersection-union型に基づいた型理論を構築し、S. van Bakelらによる型理論との関係を明らかにした。S. van Bakelらによる型理論はintersection-product型に基づく型理論であり、一見複雑なものであるが、lambda-mu をある種のCPS変換によって変換したものであると見なすと自然に理解できることがわかった。今後、この体系と上述の変換の関係を考える。
|
