高階ユニフィケーション
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/09 03:08 UTC 版)
「ユニフィケーション」の記事における「高階ユニフィケーション」の解説
多くの用途で、一階の項ではなく型付きラムダ項のユニフィケーションを考慮する必要がある。そのようなユニフィケーションを「高階ユニフィケーション」と呼ぶことが多い。高階ユニフィケーションで特に研究が進んでいる領域は、αβη変換により単純な型付きラムダ項の等価性を判定する問題である。そのようなユニフィケーション問題は最大汎用単一子を持たない。高階ユニフィケーションは決定不能だが、Gérard Huet は単一子空間の体系的探索を可能にする半決定可能なユニフィケーションアルゴリズム（Martelli-Montanari のユニフィケーションアルゴリズムに高階の変数を含む項についての規則を加えて一般化したもの）を示した。Huet と Gilles Dowek はこれに関する論文を書いている。 デール・ミラーは高階パターン・ユニフィケーションと呼ばれるものを提案した。この高階ユニフィケーションのサブセットは決定可能であり、これで解けるユニフィケーション問題には最大汎用単一子が存在する。λProlog（英語版）やTwelf（英語版）といった高階の論理プログラミング言語は、完全な高階ユニフィケーションではなくパターン・ユニフィケーションを実装しているものが多い。 計算言語学では、省略法について最も有力な理論として、省略された要素を自由変数で表し高階ユニフィケーション (HOU) を使ってその値を決定するというものがある。例えば、ジョンはメアリーが好きで、ピーターも同様であるという文を like(j; m)R(p) のように意味論表現したとき、R（省略の意味論的表現）の値は like(j; m) = R(j) という等式で決定される。このような式を解くプロセスを高階ユニフィケーションと呼ぶ。
※この「高階ユニフィケーション」の解説は、「ユニフィケーション」の解説の一部です。
「高階ユニフィケーション」を含む「ユニフィケーション」の記事については、「ユニフィケーション」の概要を参照ください。
- 高階ユニフィケーションのページへのリンク
