構成的、ないしは直観主義的な数学の興味深い点のひとつに、もしそのような数学の中での存在言明の証明を形式化すると、そこからその存在言明で存在が主張されている対象が実際に抽出できることがある。さらに、構成的な論理と、計算の体系との間には密接な関連があり、カリー・ハワード対応と呼ばれている。この対応は、プログラミング言語の理論や型理論の一つの指導原理になっている。これらの性質を用いることで、構成的な論理は、計算機のプログラムの抽出や検証に応用されている。

　一方、古典論理では存在言明の証明から、その対象を抽出することは一般に不可能である、しかし、決定可能な性質についての存在言明に限ればそのような抽出が可能であることが理論的には知られている。また、グリフィンがスキーム・プログラミング言語のcall/ccオペレータと、古典論理の二重否定除去の推論規則との間に関連を指摘して以来、カリー・ハワード対応を古典論理の上に拡張するこことみが計算機科学において興味を集めている。この観察を明確にするため、古典論理と関連づけられた計算の体系が数多く提案されている。

　しかし、こういった計算の体系でのカリー・ハワード対応と、存在言明からの対象の抽出との間の関係は、直観主議論理ほど明確ではない。これら古典論理と関連する計算の体系では、最終的な計算結果を得るために証明では直接表されていない計算を行なう必要がある。これは古典論理をプログラミング言語の研究やプログラムの正当性の検証に用いることを困難にしている。

　この論文では、パリゴーが提案したλμ計算と、それを対称的な構造簡約を行なう計算規則で拡張した体系についておもに考察する。この論文の主な結果はλμ計算に対称的な構造簡約を付け加えた計算体系について、その中で行なわれる計算が必ず停止することを示したことである。この停止性は、値による呼出によってのみ計算を行なう場合には知られていたが、この論文の結果によって、計算順序に何の制限を加えなくとも停止性が成り立つことが示された。これに加えて、この論文では2階算術をλμ計算を用いて形式化し、直観主義の場合と同じような方法で、決定可能な性質については、その性質を満たす対象の存在証明から、その対象を求めることができることを示す。

Curry-Howardの原理は,型理論における基本原理の一つである.計算機科学におけるある種の計算体系と,論理学の形式的体系とがほぼ同等とみなせることを主張するのがこの原理である.ここで,計算体系といっているのは,関数型プログラミング言語の中心を担っている型付きラムダ計算であり,形式的体系といっているのは,Brouwerに端を発する直観主義論理の体系である.この原理を用いると,たとえば,仕様に対する形式的証明から,プログラムを抽出することができ,そのプログラムの正しさは自動的に保証されることになる.

　Curry-Howardの原理に現れる形式的体系である直観主義論理は,普通に数学で用いられる論理とは異なるものであり,たとえば背理法を用いる場合には制限がある.このことから,古典論理と呼ばれる普通に用いられている論理に拡張しようという要求が出てくるのは自然なことである.

　他方,ラムダ計算の体系に対してのある種の拡張が計算機科学においてFelleisenらによって考えられていた.これは,コントロール・オペレータと呼ばれるものをラムダ計算に付け加えようという試みである.コントロール・オペレータは実行をある瞬間に打ち切って,以前の実行状態に帰るものであり,プログラミングにおいてはエラー処理の際によく用いられる.

　1990年に,Griffinは,コントロール・オペレータに対して型付けを試み,それが古典論理に現れる代表的な論理規則ときわめて類似性が高いことを指摘した.これに刺激されて,その後,Curry-Howardの原理を拡張して,コントロール・オペレータを持った計算体系と古典論理との間の関係を見出そうという試みがいろいろとなされることになった.

　Parigotによって導入されたλμ計算は,このような観点から古典論理に対応する計算体系として考え出されたものである.山形頼之が博士審査提出論文において扱っているのは,主としてこのλμ計算である.

　山形頼之が提出論文において証明したことは主に次の二点である.第一に,λμ計算の体系が強正規性を満たすこと,第二に,ある種の論理式の証明から抽出された項(プログラムに相当する)がその論理式を満たすことである.第一の主張である強正規性とは,プログラムを任意の評価戦略にそって実行したときに必ず停止することを主張するものである.仕様の証明からプログラムを抽出したとしても,そのプログラムが無限ループに陥ってしまっては意味がないので,この性質が重要であるのは論を待たないであろう.第二の主張は,抽出された項の正当性を主張するものであり,当然必要な性質である.

　Parigotらによる先行研究において,λμ計算の強正規性は証明されていたが,これは計算規則を制限した場合に対してであった.このように制限してしまうと,第二の主張である抽出されたプログラムの正当性を,そのままでは満たさなくなってしまう.山形頼之による今回の結果のもっとも重要な点は,第二の主張を満たすように計算規則を十分拡張した上で,強正規性を証明したことにある.

　山形頼之は,提出論文において、二階述語論理に対する古典論理の体系を提示し,その証明に対応する体系としてλμ計算を導入している.さらに,この体系に対する計算規則をもっとも強い形で与えている.このように与えることで,上に述べた第二の主張が成り立つことが第3章において証明されている.

　また,第4章においては,得られた体系の強正規性が証明されている.一般に,体系の強制規制を証明することは非常に困難な作業である.特に,二階の論理に対応する体系の強制規制を証明するには,更に高階の論理を用いなければならないので,多大な困難を伴う.この際に用いられる一般的な手法は,Tait-Girardによるreducibilityの方法で,直観主義論理に対応する体系の場合は,この手法で強正規性が証明されている.しかし,古典論理の場合には,この手法の単純な拡張では対応できない.この困難を乗り越えるために,Barbaneraらによって編み出された手法を高階の体系に拡張し,ある種の閉包の操作を非可算回繰り返すことにより,reducibilityの議論が適用できるように工夫したのが,提出論文においてもっとも労力と独創性を発揮した部分である.また第5章においては,このように工夫された手法が対称ラムダ計算という他の体系にも適用できることを示している.

　このように,山形頼之の博士審査提出論文は,λμ計算にたいして当然要求されるべき性質を始めて完全な形で与えたものであり,その証明には独創性と卓越した構成力が見出される.よって,山形頼之は博士(数理科学)の学位を授与される十分な資格があるものと認定される.