一階の項の統語論的ユニフィケーションの例
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/09 03:08 UTC 版)
「ユニフィケーション」の記事における「一階の項の統語論的ユニフィケーションの例」の解説
Prolog では、大文字で始まるシンボルは変数名、小文字で始まるシンボルは関数名を表し、カンマは論理積として使われる。数学の慣習では小文字だけを使い、アルファベットの最後の方（たとえば x,y,z）は変数名、f,g,h といった文字は関数記号、a,b,c といった文字は定数を意味し、定数は引数を持たない関数とみなされる。論理積は & または ∧ {\displaystyle \land } で表される。 Prolog の記法数学の記法ユニフィケーションに必要な置換備考a = a a = a {\displaystyle a=a} { } {\displaystyle \{\,\}} 成功（恒真式） a = b a = b {\displaystyle a=b} 失敗 a と b は一致しない。 X = X x = x {\displaystyle x=x} { } {\displaystyle \{\,\}} 成功（恒真式） a = X a = x {\displaystyle a=x} { x ↦ a } {\displaystyle \{x\mapsto a\}} x は定数 a に単一化される。 X = Y x = y {\displaystyle x=y} { x ↦ y } {\displaystyle \{x\mapsto y\}} x と y は別名である。 f(a,X) = f(a,b) f ( a , x ) = f ( a , b ) {\displaystyle f(a,x)=f(a,b)} { x ↦ b } {\displaystyle \{x\mapsto b\}} 関数記号と定数記号が一致しているので、x を 定数 b に単一化する。 f(a) = g(a) f ( a ) = g ( a ) {\displaystyle f(a)=g(a)} 失敗 f と g は一致しない。 f(X) = f(Y) f ( x ) = f ( y ) {\displaystyle f(x)=f(y)} { x ↦ y } {\displaystyle \{x\mapsto y\}} x と y は別名である。 f(X) = g(Y) f ( x ) = g ( y ) {\displaystyle f(x)=g(y)} 失敗 f と g は一致しない。 f(X) = f(Y,Z) f ( x ) = f ( y , z ) {\displaystyle f(x)=f(y,z)} 失敗 アリティが異なる。 f(g(X)) = f(Y) f ( g ( x ) ) = f ( y ) {\displaystyle f(g(x))=f(y)} { y ↦ g ( x ) } {\displaystyle \{y\mapsto g(x)\}} y を項 g(x) に単一化する。 f(g(X),X) = f(Y,a) f ( g ( x ) , x ) = f ( y , a ) {\displaystyle f(g(x),x)=f(y,a)} { x ↦ a , y ↦ g ( a ) } {\displaystyle \{x\mapsto a,y\mapsto g(a)\}} x を定数 a に、y を項 g(a) に単一化する。 X = f(X) x = f ( x ) {\displaystyle x=f(x)} 失敗とすべき （出現検査（英語版）により）厳密な一階述語論理では失敗となり、最近のPrologでも失敗する。古い実装のPrologでは x が x=f(f(f(f(...)))) という無限の式に単一化されるが、これは厳密には項ではない。 X = Y, Y = a x = y ∧ y = a {\displaystyle x=y\land y=a} { x ↦ a , y ↦ a } {\displaystyle \{x\mapsto a,y\mapsto a\}} x と y が共に定数 a に単一化される。 a = Y, X = Y a = y ∧ x = y {\displaystyle a=y\land x=y} { x ↦ a , y ↦ a } {\displaystyle \{x\mapsto a,y\mapsto a\}} 同上（ユニフィケーションは対称的で推移的である） X = a, b = X x = a ∧ b = x {\displaystyle x=a\land b=x} 失敗 a と b は一致しないので、x はどちらとも単一化できない。
※この「一階の項の統語論的ユニフィケーションの例」の解説は、「ユニフィケーション」の解説の一部です。
「一階の項の統語論的ユニフィケーションの例」を含む「ユニフィケーション」の記事については、「ユニフィケーション」の概要を参照ください。
- 一階の項の統語論的ユニフィケーションの例のページへのリンク
