指定的ラムダ計算といういくつかの体系,そしてそれらを拡張して作られたトランスフォーメーション計算系等は,ラムダ計算におけるカリー化の役割りに関する研究の産物である.

　ラムダ計算の抽象が基本的に1引数の関数の定義しか許さないのに,カリー化はいくつもの引数を取る関数をエンコードする方法である.値の対を取る関数をそれを2回に分けて取るものに変換し,まず1つ目の引数を取り,2つ目を取る関数を返す関数にする.形式化すると,f(a,b)＝((a))(b)になる.

　最初に定義される指定的ラムダ計算では,単なる値の対に代わり,ラベル付きレコードをカリー化する手段を提案する.ラベルを表現するためには,普通のラムダ計算より複雑な計算系が必要になる.しかしラムダ計算のほとんどの属性が保たれる.言うまでもなく合流性が成り立ち,ラムダ計算に近いモデルも作れる.そして単純型・多相型両方の型体系が適用でき,そのときラムダ計算のように強正規性も成り立つ.直接にそういう体系をML等,シンタクスがカリー化されている強い型付き関数型言語に組込み,順序が自由なラベル付き適用の導入が応用として考えられる.カリー化が部分適用を導入するので,この体系では可能な部分適用が組合せ的に増える.

　次に,カリー化に耐え得る合成の概念を導入し,指定的ラムダ計算をトランスフォーメーション計算系に拡張する.古典的な関数の合成はカリー化と相容れないが,同時にいくつもの出力と入力を接続し,それに耐える合成を定義する.この体系でも合流性が成り立ち,これに合った型体系も定義される.指定的ラムダ計算は元より含まれるが,この計算系には引数を,流れて来る値としてみなし,それを合成された変換によって扱えるという新しい力がある.純粋な関数的な枠組の中で,変数の値を変えるような手続的なアルゴリズムの書き方を許す.Algolの変数の意味論に関する今までの諸研究をシンタクスの面から照らし直すことにもなる.

　最後に紹介される,対照的変換という3つ目の計算系では,トランスフォーメーション計算系のカリー化を2個関係に拡張する.分散計算等,接続を重んじる問題に新しい表現を与え,逆転という概念のシンタクティックな視点をも提供する.

　この3つの計算系は,シンタクスの属性,型体系,及び意味論という3つの観点から研究される.

　本論文は大きく三つの部分からなっている。第一部(2章から5章)は、ラムダ計算のカリー化の操作を拡張して作られた指定的ラムダ計算という計算系の構文論と意味論、および、型付けに関するものである。第二部(6章と7章)は、トランスフォーメーション計算系と呼ぶ計算系に関するものである。指定的ラムダ計算が関数の入力に対するカリー化を拡張したものであるのに対して、トランスフォーメーション計算系では関数の出力に対してもカリー化が許されている。第三部(8章)は、トランスフォーメーシッン計算系をさらに発展させた対照的変換の計算系に関するものである。対照的変換は、関数ではなく関係に関する計算系である。

　第一部で定義されている指定的ラムダ計算では、単なる値の対に代わり、ラベル付きレコードをカリー化する手段が提案されている。ラベルを表現するために普通のラムダ計算より複雑な計算系が必要になるが、ラムダ計算のほとんどの性質が保たれている。いうまでもなく合流性が成り立ち、ラムダ計算に近いモデルも作ることができる。また、単純型・多相型両方の型体系が適用でき、その場合、ラムダ計算のように強正規性も成り立つ。本論文では、以上の性質に関して厳密な証明が与えられている。

　第二部で社、カリー化と整合性を持つ合成の概念が導入され、指定的ラムダ計算がトランスフォーメーション計算系に拡張されている。同時にいくつもの出力と入力を接続し、カリー化と整合性を持つような合成の操作が定義される。この計算系でも合流性が成り立ち、また、型の体系を定義することもできる。指定的ラムダ計算をその一部として含むが、この計算系には、引数を流れて来る値としてみなして合成された変換によって扱えるという新しい能力がある。純粋な関数的な枠組の中で、変数の値を変えるような手続的なアルゴリズムを書くことができ、Algolの意味論に関する諸研究を構文論の面から考察することが可能になった。

　第三部では、トランスフォーメーション計算系のカリー化を二項関係に拡張することによって、対照的変換という三つ目の計算系が導入されている。この計算系では、分散計算等、接続概念(continuation)が重要な問題に新しい表現を与えることができ、逆転(conjugation)という概念の構文論的な視点も提供されている。

　なお、本論文の2章から5章は、Hassan Ait-Kaciとの共同研究であるが、論文提出者が主体となて分析および検証を行ったもので、論文提出者の寄与が十分であると判断する。