μ冠頭形証明の計算的意味に関する基礎的研究

論理式を型と解釈する原理(カリ-・ハ-ワード同型)により,μ冠頭形証明に計算的意味(プログラム)を割当てるための基礎的研究として以下のことが明らかになった.(1)シーケントの右側に高々2種類の論理式しか出現することのないμ冠頭形証明の基本的性質について(発表論文2):1-1)古典命題論理における定理に対しては,必ずμ冠頭形証明が存在する;1-2)μ冠頭形証明におけるシーケントの右側に対しては,直観主義的証明の特徴であるdisjunction propertyがある意味で成立している;1-3)古典的証明であるμ冠頭形証明から直観主義的証明への埋め込みは容易に与えることができ,これはグリベンコの定理の拡張となっている.(2)μ冠頭形証明のプログラミングへの応用について(発表論文1):2-1)μ冠頭形証明は,型付き関数型言語であるMLの例外処理プログラムに自然に対応付け可能である;2-2)μ冠頭形証明では,シーケントの右側に高々2種類の論理式しか出現することのない.その2種類のうちで,証明図全体に出現している論理式は不変論理式と呼ばれる.その不変論理式は,与えられた定理の構文のみから,“含意"と"かつ"に関してstrictly positiveな部分論理式として特徴付けられる.したがって,シーケント計算における右減規則の適用方法がこの不変論理式により規定できることがわかった.そしてこの不変論理式は,例外処理で外に脱出する値の型に対応していることが解明された.

論理式を型と解釈する原理(カリ-・ハ-ワード同型)により,μ冠頭形証明に計算的意味(プログラム)を割当てるための基礎的研究として以下のことが明らかになった.(1)シーケントの右側に高々2種類の論理式しか出現することのないμ冠頭形証明の基本的性質について(発表論文2):1-1)古典命題論理における定理に対しては,必ずμ冠頭形証明が存在する;1-2)μ冠頭形証明におけるシーケントの右側に対しては,直観主義的証明の特徴であるdisjunction propertyがある意味で成立している;1-3)古典的証明であるμ冠頭形証明から直観主義的証明への埋め込みは容易に与えることができ,これはグリベンコの定理の拡張となっている.(2)μ冠頭形証明のプログラミングへの応用について(発表論文1):2-1)μ冠頭形証明は,型付き関数型言語であるMLの例外処理プログラムに自然に対応付け可能である;2-2)μ冠頭形証明では,シーケントの右側に高々2種類の論理式しか出現することのない.その2種類のうちで,証明図全体に出現している論理式は不変論理式と呼ばれる.その不変論理式は,与えられた定理の構文のみから,“含意"と"かつ"に関してstrictly positiveな部分論理式として特徴付けられる.したがって,シーケント計算における右減規則の適用方法がこの不変論理式により規定できることがわかった.そしてこの不変論理式は,例外処理で外に脱出する値の型に対応していることが解明された.