関数論理型言語とは,宣言型パラダイムにもとづく代表的な言語族である,関数型言語と論理型言語の特徴を併せ持つ宣言型プログラミング言語族である.これまでに,様々な関数論理型言語が提案されているが,現在では,ナローイングと呼ばれる計算メカニズムに基づくものが最も一般的である.ナローイングとは,項書換え系を用いた書換えの一種であり,関数型言語の計算モデルである項書換えと,論理型言語の計算モデルであるSLD導出の両者を包含しているため,これら二つの言語を自然に融合することができる.なかでも条件付き項書換え系を用いる条件付きナローイングは,関数型言語におけるifやwhere,および論理型言語におけるホーン節を,条件付き書換え規則を用いて記述できるので特に有用である.条件付きナローイングに基づく関数論理型言語としては,K-LEAF,BABELなどが知られている.条件付き項書換え系の例として,除算のプログラム

　のモデルである条件付き項書換え系を以下に示す.

　三番目の書換え規則の右辺(S(q),r)は,左辺div(S(x),S(y))に現れない変数qとrを含む.書換え規則の左辺に現れない変数を外変数(extra variable)と呼ぶ.このように,外変数が書換え規則の右辺に現れることを許すと,条件部のみに許した場合に比べて,より多くのプログラムを自然に記述できるようになる.しかし,このような条件付き項書換え系は,外変数の存在を書換え規則の条件部のみに許す場合に比べて,数学的取り扱いが著しく複雑になる.たとえば,ナローイングにおける重要な性質である等式の求解完全性は,このような条件付き項書換え系に対しては,停止性をもつ条件付き項書換え系に対する結果しか得られていない.遅延評価の機構を用いた無限データ構造の有用性を考慮すると,停止性の仮定は,プログラミング言語にとっては厳しすぎる制限である.たとえば,前述した既存の関数論理型言語では,停止性を仮定しなくてもナローイングの求解完全性が保証できるように,外変数の存在を条件部のみに制限している.本論文は,外変数を含む条件付き項書換え系を用いた条件付きナローイングの求解完全性について新たな結果を提出することで,関数論理型言語のプログラムのモデルとなる条件付き項書換え系のクラスを拡張することを目的としている.特に重要なのは,停止性をもたず,書換え規則の右辺に外変数を持つ条件付き項書換え系におけるナローイングの求解完全性である.

　井田と奥居は,停止性を仮定しない条件付き項書換え系においてナローイングの求解完全性を保証する十分条件を与えた.この十分条件は,階層合流性(level-confluence)と階層正規性(level-normality)と呼ばれる,条件付き項書換え系での書換えに関する性質からなる.この結果は,書換え規則の条件部のみに外変数をもつ条件付き項書換え系に対するものである.本論文では,有向な(oriented)条件付き項書換え系に対して,この結果を拡張した.有向な条件付き項書換え系とは,条件部の各等式について,左辺から右辺への到達可能性(reachability)が成り立つときのみ条件が満たされるとする解釈を伴う条件付き項書換え系である.関数型言語のletやwhereにおいて局所的定義を与える等式は,等式の一方の辺だけを評価した後,その値を他方の辺へ代入する.したがって,letやwhereのような局所的定義をもつプログラムは,有向な条件付き項書換え系を用いてモデル化できる.本論文では,有向な条件付き項書換え系については,階層正規性をより緩めた独立階層正規性(independent level-normality)と呼ばれる条件を階層合流性とともに用いれば,ナローイングの求解完全性を保証する十分条件を与えることができることを示した.さらに,停止性を仮定しない場合の,書換え規則の右辺に外変数をもつ条件付き項書換え系への拡張を試みた.その結果,定向性(proper orientedness)という構文的な条件を付加すれば,このような有向条件付き項書換え系に対してもナローイングの求解完全性を保証できることが明らかになった.

　階層合流性と独立階層正規性は,ともに条件付き項書換え系における書換えに関する性質である.プログラミング言語処理系で,与えられたプログラムがナローイングの求解完全性を保証する条件付き項書換え系に基づいているかどうかを迅速にチェックするためには,これらの性質を保証する構文的な条件を明らかにする必要がある.本論文では,定向性をもつ条件付き項書換え系が,正交性(orthogonal)と右安定性(right-stability)と呼ばれる構文的な性質を満たすならば,階層合流性と独立階層正規性をみたすことを明らかにした.

　正交な条件付き項書換え系は,関数論理型言語のプログラムのモデルとして適当であることが,多くの研究者によって指摘されている.実際,関数型言語と論理型言語の多くのプログラムは,このクラスに属する.また,定向性と右安定性は,我々がプログラムを記述するときに,しばしば自然に仮定する条件である.たとえば,前述の除算のプログラムをモデル化する条件付き項書換え系は,定向かつ右安定である.したがって,ここで与えた十分条件は,関数論理型言語のプログラムのモデルとして適当な表現力を保証しているといえる.

　本論文では,項書換え系における標準化定理(standardization theorem)の新たな証明方法についても述べている.標準化定理は,与えられた書換え列から「標準的な」書換え列が常に得られることを述べた定理である.この定理は,書換え系における正規化戦略の理論的基礎を与えるとともに,関数型言語における遅延評価の機構の理論的基礎付けを与える.また,標準化定理は,遅延ナローイングと呼ばれるナローイング戦略の理論的基礎を与える.このナローイング戦略は,遅延評価の機構をもつ関数論理型言語の計算メカニズムとして用いられるので,実用的な関数論理型言語処理系を設計する上で特に重要である.標準化定理については,既にいくつかの異なる証明法が提案されているが,ここでは,与えられた書換え列への新たなラベル付けの方法を提案することで,左線形な項書換え系に関する標準化定理を証明する方法を与えた.また,この証明法を条件付き項書換え系の場合に拡張することで,外変数を書換え規則の右辺に含む左線形な条件付き項書換え系に関して,標準化定理が成り立つことを示した.この結果は,遅延ナローイングの条件付きナローイングへの拡張を図る上でとくに有用である.

　本論文は9章より成るが,本研究の成果は,第5章から第8章までに書かれている.本論文は全体として,条件付き項書換え系におけるナローイング計算の完全性を示すものである.第5章では,有向な条件付き項書換え系において,書換えが階層合流性と独立階層正規性を満たせば,ナローイングの求解完全性が保証されることが示されている.第6章では,階層合流性を保証するための構文的な条件が明らかにされる.第7章では,独立階層正規性を保証するための構文的な条件が明らかにされる.第8章では,項書換え系における標準化定理の新たな証明方法が述べられる.標準化定理は,遅延ナローイングと呼ばれるナローイング戦略の完全性を与えるための基礎となる.

　第5章では,有向な条件付き項書換え系においては,階層正規性をより緩めた独立階層正規性と呼ばれる条件を階層合流性とともに用いれば,ナローイングの求解完全性を保証する十分条件を与えることができることが示される.さらに,停止性を仮定しない場合の,書換え規則の右辺に外変数をもつ条件付き項書換え系への拡張が試みられる.その結果,定向性という構文的な条件を付加すれば,このような有向条件付き項書換え系に対してもナローイングの求解完全性を保証できることが明らかになった.

　階層合流性と独立階層正規性は,ともに条件付き項書換え系における書換えに関する性質である.プログラミング言語処理系で,与えられたプログラムがナローイングの求解完全性を保証する条件付き項書換え系に基づいているかどうかを迅速にチェックするためには,これらの性質を保証する構文的な条件を明らかにする必要がある.第6章と第7章では,定向性をもつ条件付き項書換え系が,正交性と右安定性と呼ばれる構文的な性質を満たすならば,階層合流性と独立階層正規性をみたすことを明らかにされる.

　正交な条件付き項書換え系は,関数論理型言語のプログラムのモデルとして適当であることが,多くの研究者によって指摘されている.実際,関数型言語と論理型言語の多くのプログラムは,このクラスに属する.また,定向性と右安定性は,我々がプログラムを記述するときに,しばしば自然に仮定する条件である.したがって,ここで与えた十分条件は,関数論理型言語のプログラムのモデルとして適当な表現力を保証しているといえる.

　第8章では,項書換え系における標準化定理の新たな証明方法についても述べられている.標準化定理は,与えられた書換え列から「標準的な」書換え列が常に得られることを述べた定理である.この定理は,書換え系における正規化戦略の理論的基礎を与えるとともに,関数型言語における遅延評価の機構の理論的基礎付けを与える.また,標準化定理は,遅延ナローイングと呼ばれるナローイング戦略の理論的基礎を与える.このナローイング戦略は,遅延評価の機構をもつ関数論理型言語の計算メカニズムとして用いられるので,実用的な関数論理型言語処理系を設計する上で特に重要である.標準化定理については,既にいくつかの異なる証明法が提案されているが,ここでは,与えられた書換え列への新たなラベル付けの方法が提案されたことで,左線形な項書換え系に関する標準化定理を証明する方法が与えられた.また,この証明法を条件付き項書換え系の場合に拡張することで,外変数を書換え規則の右辺に含む左線形な条件付き項書換え系に関して,標準化定理が成り立つことが示された.この結果は,遅延ナローイングの条件付きナローイングへの拡張を図る上でとくに有用である.

　なお,本論文の第6章は,井田哲雄氏とアート・ミデルドープ氏との共同研究であるが,論文提出者が主体となって分析及び検証を行なったもので,論文提出者の寄与が十分であると判断する.

　したがって,博士(理学)を授与できると認める.