論理プログラミングでのユニフィケーション
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/09 03:08 UTC 版)
「ユニフィケーション」の記事における「論理プログラミングでのユニフィケーション」の解説
単一化(ユニフィケーション)の考え方は Prolog に代表される論理プログラミングの根底を支える重要な概念である。それは変数の内容の束縛であり、項の構成要素の全体の形式から細部までその同一性を検査する機構である。他のプログラム言語とは異なり、Prolog では = という記号はこの意味を表す。Prolog は、質問としての副目標と、これによって呼び出される述語定義の頭部の単一化が試みられ、頭部の単一化の成功した節のみ選択され、その本体が次の質問になる導出と呼ばれるダイナミックで再帰的な機構によって実行される。 一般に型推論アルゴリズムは上記単一化に基づいている。 Prolog では、単一化されるとは、 束縛されていない変数 は、原子項、複合項、そして他の束縛されていない変数を、以後同一なものとみなす。この変数の変数名を、変数を含む他の項の一種の別名と解釈することも可能である。全ての形式の項に対して同一のものとみなすことができるのだから、束縛されていない変数の単一化は必ず成功する。(注1) 原子項（アトム）は同じ原子項とだけ単一化可能である。原子項はアルファベット(英文字に限らない)によって構成された文字列なのでこの先頭から最後までの文字とその位置が同一の場合、単一化される。一ヶ所でも異なれば単一化は失敗する。 複合項は関数名(述語名)とアリティ（オペランドの個数）が等しい場合に、対応するオペランド毎に項の単一化が再帰的に試みられる。この単一化が全て成功した場合のみ単一化に成功したことになる。 (注1) 最近の Prolog や一階述語論理では、変数（変項）はそれ自身を含む項と単一化することはできない。それをすると無限の単一化が発生するためである。
※この「論理プログラミングでのユニフィケーション」の解説は、「ユニフィケーション」の解説の一部です。
「論理プログラミングでのユニフィケーション」を含む「ユニフィケーション」の記事については、「ユニフィケーション」の概要を参照ください。
- 論理プログラミングでのユニフィケーションのページへのリンク
