ユニフィケーション
(単一化 から転送)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/09 03:08 UTC 版)
ユニフィケーション（英: unification）は数理論理学や計算機科学の用語であり、充足性問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つの項が同一[1]または同等[2]であることを示す置換を求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。
- ^ 英: identical
- ^ 英: equal
- ^ 英: syntactic unification
- ^ 英: equality
- ^ 英: semantic unification
- ^ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.
- ^ Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Lectures on Jacques Herbrand as a Logician (SEKI Report). arXiv:0902.4682. Here: p.56
- ^ Jacques Herbrand (1930). Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis). A. 1252. Université de Paris. Here: p.96-97
- ^ 英: occurs check
- ^ 英: unifier
- ^ a b 英: most general unifier
- ^ 英: equational-unification。e-unification とも呼ばれる。
- ^ lamdaPrologなど
- ^ Russell, Norvig: Artificial Intelligence, A Modern Approach, p. 277
- ^ Warren Goldfarb: The undecidability of the second-order unification problem
- ^ Gérard Huet: The undecidability of unification in third order logic
- ^ Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)
- ^ Martelli, Montanari: An Efficient Unification Algorithm
- ^ Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []
- ^ Gérard Huet: Higher Order Unification 30 Years Later
- ^ Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009-1062
- ^ 英: Dale Miller
- ^ 英: higher-order pattern unification
- ^ Dale Miller: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, 1991, pp. 497--536
- ^ Claire Gardent, Michael Kohlhase, Karsten Konrad, (1997), A multi-level, Higher-Order Unification approach to ellipsis
- ^ 英: number of non-unique variables
- ^ 英: number of function symbols and constants on the LHS of potential equations
- ^ 英: number of equations
- ^ McBride, Conor (October 2003). “First-Order Unification by Structural Recursion”. Journal of Functional Programming 13 (6): 1061–1076. doi:10.1017/S0956796803004957. ISSN 0956-7968 2012年3月30日閲覧。.
単一化
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/12 02:49 UTC 版)
単一化は1960年代の述語論理理論の発展の鍵となった概念であるが、Prolog が述語論理に導かれて機械による自動証明を実現するためのプログラム言語として成立したことから、必然的にこの言語の必須の最も重要な機構となった。単一化は副目標（質問）と対応する定義節の頭部のパターンが完全に一致するか、調べることで、節の選択を可能にする。さらに、Prolog の実行順序等の制御は単一化のからくりを利用してプログラミングされる。 簡単なからくりでかつ極めて強力な単一化であるが実行コストも大きい、すなわち実行速度が遅くなる原因となる。さらに、パターンとして認識することと引き換えに、引数での関数評価は不可能になった。独立して節の本体で式評価を記述しなくてはならないため、数値計算ではやや冗長になる。これらの点は、単一化の強力さとのトレードオフの関係になっている。
※この「単一化」の解説は、「Prolog」の解説の一部です。
「単一化」を含む「Prolog」の記事については、「Prolog」の概要を参照ください。
「単一化」の例文・使い方・用例・文例
- 単一化のページへのリンク
