関数論理型言語の意味論として，これまでに二つの独立したアプローチが 存在している．一つは項書換え系に基づくもの，もう一つは論理型プログラミング 言語の宣言的意味論に基づくものである． 双方の意味論のアプローチとも対象としている関数論理型言語の構文はほぼ 同一のものであるが，意味論，操作的意味論ともに別々の ものが与えられているため，双方の関係はこれまで明らかにされていなかった． この論文は，関数論理型言語を等式論理の枠組みでとらえ， これら二つの意味論を等式論理に対する二つのモデル として定式化し，その等価性を示したものである．

双方のアプローチを比較するために， 本論文は関数論理型言語の意味論を条件付き等式論理の枠組みで論じる． 条件付き等式論理とは，述語記号が等号記号``=''のみである一階述語論理 であり，論理式として条件付き等式を取るものである．

関数論理型言語の条件付き等式論理による見方は，次の自然な解釈 を導く．すなわち，関数論理型プログラムとは「関数定義として解 釈される条件付き等式」であり，質問とは「存在限量された等式」 である．そして，関数論理型言語の実行である「質問を解く」とは 「前提となる関数論理型プログラムのもとで解を求めることにより， 存在限量された等式の妥当性を証明する」ことである． Kaplan,Goguen,Meseguerらの結果を用い，条件付きナローイングは， 正規解を持つような妥当な質問に対して，完全な証明法であることが示される．

関数論理型言語に対する二つのアプローチは， 条件付き等式の集合としての関数論理型プログラムに対する， 二つの異なったモデルとして定式化される． このモデルとは，商項代数モデルと最小完備エルブランモデルである． 質問の形を厳格等式と呼ばれる 有限確定な値上のみで 成立するように制限された等式の形として与えれば， 双方のモデルでの質問の妥当性は等価であることが示される．

この結果を得るために，まず，質問の等式の形を厳格等式ではなく， 一般の等式として考えてみる． すると，もしその質問の両辺が，最小完備エルブランモデルにおけ る解釈において 未定義値あるいは無限値をとる場合，質問の妥当性が二つのモデルの間では 等価でなくなる反例を見つけることができる． 関数論理型言語においては，質問の形として厳格等式を採用する ことが多いが， この反例はその理由を意味論的に説明する結果となっている．

さらに厳格等式を質問の形として採用すれば， 質問は常に正規解を持つことを示すことができ，これより 「質問の妥当性は二つのモデルの間で等価となる」という本論文の目的である定理を 証明することができる． 等価性の証明は 「商項代数モデルで成立する質問は，最小完備エルブランモデルでも成立する」 という命題と，その逆 「最小完備エルブランモデルで成立する質問は，商項代数モデルでも成立する」 の双方を示すことによる． 前者は商項代数の始モデル性よりただちに得られる． 後者の証明が本論文の主要な部分である．

この証明は領域論的結果を用いて行われる．証明の鍵となる事実は，

• 最小完備エルブラン領域の代数性
• 厳格等式の連続性
• 最小完備エルブランモデルでの有限で全域的(finite and total)な解 は商項代数モデルでの解とみなせるという事実

である．証明の方針は，最小完備エルブランモデルでの質問の解から 商項代数モデルでの質問の解をつくることである． これはまず，１．の 領域の代数性を使い，最小完備エルブランモデルでの質問の解を有限元 の最小上界で表現する．次に２．の厳格等式の連続性を使い， 厳格等式の成立性を，得られた有限元を解とする厳格等式の成立性で 置き換える．これらの有限元の解は未定義値を含んでいるかもしれないが， これを適当な定数で置き換えたものもやはり有限元の解となる ことが示せる．そしてそのような解は有限で全域的な解となる． よって最後に３．を使い，この解が商項代数モデルでの解であることが わかる．

この結果より，関数論理型言語の実行を最小完備エルブラン モデル中での等式の求解と見なすことができる． これはすなわち， 関数記号は部分関数を表し，計算は無限データを扱うという 関数論理型言語の自然な理解が，妥当であるという望ましい結果である． さらに我々はナローイングを妥当な質問を解くための方法として使 うことができる．二つの意味論の等価性は，このような自然な理解 とそれに対する健全かつ完全な解法を提供する結果である，と結論することができる．