ユニフィケーション（単一化）とは？ゆにふぃけーしょん
ユニフィケーション（単一化）とは、論理型言語の推論エンジンが行う基本操作で、二つの項を照合し、含まれる変数へ値を割り当てて両者を同じ形にすること。この照合が成功するかどうかで、その規則（節）を適用できるかが決まり、割り当てられた束縛の集合がそのまま問合せの答えになる。
最終更新：2026-10-06
この語が出る過去問を解く →背景
手続き型言語の代入は左辺へ値を入れる一方向の操作だが、論理型言語では問合せ側にも事実側にも変数が現れうる。どちらの変数にも束縛を入れて形を揃える操作を用意することで、「どの規則が使えるか」の判定と「答えの値を得ること」を一つの仕組みで同時に行える。Prologの動作原理として問われる。
具体例
Prologで事実 親(太郎, 花子). が登録されている状態で 親(太郎, X) と問い合わせると、両者が単一化されてXに花子が束縛され、これが答えとして返る。該当する事実が複数あれば、順に照合されて解が列挙される。
試験での引っ掛け
代入や一方向のパターンマッチとの取り違えが定番。単一化は両辺の変数に束縛が入りうる双方向の照合で、左辺へ値を入れるだけの操作ではない。照合そのものを指すため、失敗したときに別の節を試すバックトラックとは別の操作である点も区別する。
関連用語
出た過去問
出典：令和6年度 春期 システムアーキテクト試験 午前Ⅱ 問9（IPA）
論理型プログラミングにおいて、命題の証明を行うための基本的な機能はどれか。
正解：ユニフィケーション
要点：項を一致させるユニフィケーションが論理型言語の推論の基礎
論理型プログラミングでは、事実と規則の集合に対して問合せを与え、変数に適切な値を割り当てて項どうしを一致させながら証明を進める。この、変数への代入を求めて二つの項を同一の形にする操作がユニフィケーション（単一化）であり、導出（規則を当てはめて結論を導く推論）による推論の基礎となる。
出典・参考
解説は資格暗記が独自に作成しています。過去問の出典は各問題に記載のとおりです。