一階の項における統語論的ユニフィケーション問題
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/02/22 09:08 UTC 版)
「ユニフィケーション」の記事における「一階の項における統語論的ユニフィケーション問題」の解説
一階の項における統語論的ユニフィケーション問題は、同等である可能性のある有限個の式の連言 t 1 = ? u 1 & , … , & t n = ? u n {\displaystyle t_{1}{\stackrel {?}{=}}u_{1}\And ,\ldots ,\And t_{n}{\stackrel {?}{=}}u_{n}} で表される。この問題を解くには、それぞれの潜在的等式の左辺と右辺が統語論的に等価となるような置換 θ {\displaystyle \theta } を求める必要があり、 t 1 θ = u 1 θ & , … , & t n θ = u n θ {\displaystyle t_{1}\theta =u_{1}\theta \And ,\ldots ,\And t_{n}\theta =u_{n}\theta } となるようにしなければならない。そのような置換 θ {\displaystyle \theta } を「単一子」（ユニフィケーション作用素）と呼ぶ。ユニフィケーション問題には解がない場合もある。例えば、 x = ? z & y = ? f ( x ) {\displaystyle x{\stackrel {?}{=}}z\And y{\stackrel {?}{=}}f(x)} の単一子は { x ↦ z , y ↦ f ( z ) } {\displaystyle \{x\mapsto z,y\mapsto f(z)\}} である。この場合、 x { x ↦ z , y ↦ f ( z ) } = z = z { x ↦ z , y ↦ f ( z ) } = z {\displaystyle x\{x\mapsto z,y\mapsto f(z)\}=z=z\{x\mapsto z,y\mapsto f(z)\}=z} y { x ↦ z , y ↦ f ( z ) } = f ( z ) = f ( x ) { x ↦ z , y ↦ f ( z ) } = f ( z ) {\displaystyle y\{x\mapsto z,y\mapsto f(z)\}=f(z)=f(x)\{x\mapsto z,y\mapsto f(z)\}=f(z)} となる。
※この「一階の項における統語論的ユニフィケーション問題」の解説は、「ユニフィケーション」の解説の一部です。
「一階の項における統語論的ユニフィケーション問題」を含む「ユニフィケーション」の記事については、「ユニフィケーション」の概要を参照ください。
- 一階の項における統語論的ユニフィケーション問題のページへのリンク
