@misc{oai:ir.soken.ac.jp:00000858,
 author = {木村, 大輔 and キムラ, ダイスケ and KIMURA, Daisuke},
 month = {2016-02-17, 2016-02-17},
 note = {本論文の主題は古典論理における計算手続きの双対性を明らかにすることである。論理と<br />プログラミング言語理論の間にはカリー・ハワード対応と呼ばれる密接な対応関係が知られ<br />ている。これはプログラミング言語における型,プログラムおよびプログラムの計算手続き<br />を論理における論理式,証明および証明の正規化手続きに対応させる関係である。カリー・<br />ハワード対応は直観主義論理とラムダ計算についての関係がよく研究されてきたが,この関<br />係はプログラミング言語理論における継続の概念を考慮することで古典論理についての関係<br />へと拡張できる。拡張された計算体系の一つとしてParigotのラムダミュー一計算は単純な文<br />法でありながら強力な表現力を持ち,合流性や強正規化性などの良い性質を持つことからよ<br />く研究されている。プログラミング言語理論では,名前呼び戦略と値呼び戦略と呼ぼれる2<br />つの計算戦略がよく研究されている。これらは継続の概念を考慮することで対称的な計算手<br />続きとして見ることが出来る。一方,古典論理にはド・モルガン双対と呼ばれる双対性をも<br />つことがよく知られている。Wadlerは古典シーケント計算に対応する双対計算を提唱し,値<br />呼び計算と名前呼び計算の双対性をシーケント計算の双対性を用いて説明した。双対計算は<br />古典シーケント計算に見られる明確な対称性を持つ計算体系であり,継続に相当する概念を<br />項として扱えるのが特徴である。また,双対計算の計算手続きはシーケント計算のカット除<br />去手続きに対応するように設計されている。本論文ではラムダミュー計算と双対計算および<br />極性双対計算を用いて古典論理の計算手続きの双対性を研究する。<br />　第2章ではWadlerの未解決問題に対する良い部分解を与える。Wadlerはラムダミュー計<br />算と双対計算の間の相互変換を与え,ラムダミュー計算の名前呼びおよび値呼び戦略の双対<br />性を双対計算の対称性で説明した。しかし,彼が考えた体系は等式に基づく体系であり,計<br />算を手続きに従って順番に行なっていくことを意味する簡約関係は考慮されていなかった。<br />Wadlerの未解決問題は彼の結果を簡約関係に置きかえられるかどうかという問題である。本<br />研究ではまずWadlerの結果を見直し,問題を解くにあたって困難な部分を分析した。その結<br />果,連言,選言そして否定に関するη規則,値呼び計算における構造制御規則である(name)<br />規則,そして値呼び計算における対称μ規則の変数を代入する場合が困難であることをつ<br />きとめた。これらの規則のうち,前者2つの規則は証明図の正規化やカット除去とは対応し<br />ない規則であること,そして最後の対称μ規則についてはそれを外しても閉項の計算結果が<br />変わらないという理由により本質的ではない。そこで本研究では困難の原因であるこれらの<br />規則を取り除き,または変更して定義したラムダミュー計算と双対計算に対して簡約体系を<br />考え,Wadlerが与えた変換を改良することでこの問題を解決した。また,この研究により<br />得られた結果から,値呼びラムダミュー計算と名前呼びラムダミユー計算の相互変換を,互<br />いの簡約関係を保つようなものとして得ることができる。Wadlerは計算順序を考慮しない<br />等式体系においてラムダミュー計算の値呼び戦略と名前呼び戦略の双対性を説明したが,本<br />研究の結果は計算順序を考慮しても双対性を説明できることを意味している。<br />　第3章では極性双対計算を提案する。これはLaurentの極性線形論理の部分体系に対応す<br />るようにWadlerの双対計算のアイデアを用いて構築した項計算体系である。極性線形論理<br />において論理式はその性質により正負の極性を持つものとして分類される。極性双対計算は<br />双対計算のように明示的な左右の対称性ではなく,論理式の極性という形で双対性を持つ。<br />また,極性双対計算の簡約規則は極性線形論理のカット除去手続きに対応するように定義さ<br />れる。本研究の貢献は極性線形論理に対して項計算体系を与え,それに関する性質を明らか<br />にしたことである。極性線形論理の証明図の表現はシ「ケント計算かプルーフネットと呼ば<br />れるグラフを用いた表現のどちらかのみであったが,本研究により極性線形論理のカット除<br />去手続きが計算手続きとして得られる。また,本研究ではラムダミュー計算から極性双対計<br />算への2つの変換を与える。これらは値呼び計算の項を正論理式の証明図へ,名前呼び計算<br />の項を負論理式の証明図へと変換し,それぞれの簡約規則を保つ。これはラムダミュー計算<br />により極性線形論理のカット除去手続きが模倣されることを意味する。また,これらの変換<br />が充満性,すなわち極性線形論理における証明図が変換の像の論理式を証明するとき,この<br />証明図と同等な証明図に変換されるラムダミュー計算の項が存在することを示す。, application/pdf, 総研大甲第1048号},
 title = {Computation in Classical Logic and Dual Calculus},
 year = {}
}