非形式的概要

ウィキペディア小見出し辞書

非形式的概要

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/09 03:08 UTC 版)

「ユニフィケーション」の記事における「非形式的概要」の解説

2つの項 s と t があるとき、（統語論的）ユニフィケーションは s と t を構造的に等価にする置換を求めるプロセスである。そのような置換が存在する場合、それを s と t の単一子と呼ぶ。 理論上、入力された2つの項は無数の単一子を持ちうる。しかし一般的用途では1つの最大汎用単一子を考慮すれば十分である。他の単一子は最大汎用単一子のインスタンスである。 一階のユニフィケーションは、一階の項（変数記号や関数記号で構築される項）の統語論的ユニフィケーションである。一方高階ユニフィケーションは、高階の項（何らかの高階の変数を含む項）のユニフィケーションを指す。 特定のユニフィケーションアルゴリズムの理論的属性は、入力される項の多様性に依存する。たとえば一階のユニフィケーションは決定可能であり、単一化可能な項群は必ず最大汎用単一子を持つ。しかし高階ユニフィケーションは一般に決定不能であり、最大汎用単一子を持たないことが多い。 統語論的ユニフィケーションとは別に、意味論的ユニフィケーションも広く使われている。この2つは、項を「等しい」とみなす方法が異なる。統語論的ユニフィケーションでは、置換によって項が構造的に等価になるようにする。意味論的ユニフィケーションでは、2つの項が何らかの理論において合同であるかで判定する。例えば、交換性と結合性において合同な項を「等しい」とするユニフィケーションをAC-ユニフィケーションと呼ぶ。 ユニフィケーションは計算機科学の重要なツールである。特に一階のユニフィケーションは論理プログラミング、プログラミング言語の型システム設計、自動推論などに用いられている。高階ユニフィケーションは定理証明支援で使われている。高階ユニフィケーションに制約を加えたものを実装に採用したプログラミング言語もある。意味論的ユニフィケーションは、背景理論付きSAT (SMT) を解くアルゴリズムや項書き換えアルゴリズムでよく使われている。