الگوریتم یکسان سازی UNIFY در استنتاج مرتبه اول در AI
الگوریتم یکسان سازی UNIFY در استنتاج مرتبه اول در AI
قوانین استنتاج ارتقا یافته مستلزم یافتن جانشینی هایی است که موجب میشوند عبارات منطقی مختلف، یکسان به نظر برسند. این فرایند یکسان سازی نام دارد و عنصر اصلی الگوریتم های استنتاج مرتبه اول است. الگوریتم UNIFY دو جمله را دریافت میکند و یک یکسان ساز را برای آنها برمی گرداند (در صورت وجود):
UNIFY(p,q) = θ where SUBSET (θ,p) = SUBSET (θ,q).
برای بررسی رفتار UNIFY چند مثال زیر را در نظر میگیریم.
فرض کنید پرس وجوهای AskV ars(Knows(John,x)) به معنای این است که John چه کسی را می شناسد؟ برای یافتن بعضی از پاسخ های مربوط به این پرس وجو میتوان تمام جملاتی را در پایگاه دانش یافت که با Knows(John,x) یکسان میشود. نتایج یکسان سازی با چهار جمله مختلف که ممکن است در پایگاه دانش باشند در زیر آمده است:
UNIFY ( Knows (John, x) , Knows(John, Jane) ) = {x/ Jane}
UNIFY ( Knows (John, x) , Knows(y, Bill) ) = {x/ Bill , y/ John}
UNIFY ( Knows (John, x) , Knows(y, Mother(y) ) ) = { y/ John , x/ mother(John)}
UNIFY ( Knows (John, x) , Knows(x, Elizabeth) ) = fail.
یکسان سازی آخری با شکست مواجه میشود، زیرا x نمی تواند همزمان مقادیر Elizabeth و John را بپذیرد. معنای Knows(x, Elizabeth) این است که "همه Elizabeth را میشناسند"، لذا باید بتوانیم استنتاج کنیم که John نیز Elizabeth را میشناسد. مشکل وقتی به وجود می آید که دو جمله بخواهند از یک متغیر به نام x استفاده کنند. این مشکل با جداسازی استاندارد یکی از دو جمله ای که باید یکسان سازی شود، رفع میگردد. معنایش این است که متغیرهای یکی از دو جمله تغییر نام پیدا کنند تا از برخورد اسامی اجتناب شود. بعنوان مثال میتوانیم x را در Knows(x, Elizabeth) به x17 عوض کنیم، بدون اینکه معنایش تغییر کند. اکنون یکسان سازی عمل خواهد کرد:
UNIFY ( Knows (John, x) , Knows(x17, Elizabeth) ) = {x/ Elizabeth, x17/ John}.
یک پیچیدگی دیگر نیز وجود دارد: گفتیم UNIFY باید یک جایگزینی را برگرداند تا دو آرگومان را یکسان کند. اما ممکن است تعداد این یکسان سازها بیش از یکی باشد.
بعنوان مثال UNIFY(Knows(John, x) , Knows(y, z)) میتواند {y / John , x / z} یا {y / John , x / John , z/ John } را برگرداند. یکسان ساز اول، Knows(John, z) را بعنوان نتیجه ی یکسان سازی برمیگرداند، در حالیکه دومی Knows(John, John) را برمیگرداند. نتیجه دوم میتواند زا اوای به دست آید، برای این منظور نیاز به جایگزینی دیگر یعنی { z/ John } است.
میگوییم یکسان ساز اول کلی تر از دومی است، زیرا محدودیت کمتری به متغیرها اعمال میکند. نتیجه میشود که برای هر جفت قابل یکسان سازی از عبارات، یک کلی ترین یکسان ساز، وجود تغییر نام و جایگزینی متغیرهای یکتاست.
الگوریتم محاسبه "کلی ترین یکسان ساز" را در ادامه ذکر خواهیم کرد. در این الگوریتم فرایند محاسبه بسیار ساده است: دو عبارت را همزمان در کنار هم بطور بازگشتی جست وجو کنید تا یکسان ساز ساخته شود، اما اگر دو نقطه متناظر در این ساختار با هم تطبیق نکنند، با شکست مواجه خواهید شد. یک مرحله گران وجود دارد: هنگام تطبیق یک متغیر یا یک ترم پیچیده، باید بررسی شود که آیا خود متغیر در ترم ظاهر میشود یا خیر. اگر ظاهرمی شود، این تطبیق با شکست مواجه میشود زیرا نمیتوان یکسان سساز سازگاری را ساخت.
این بررسی وقوع، پیچیدگی الگوریتم را برحسب اندازه عباراتی که باید یکسان سازی شود، از درجه دوم تعیین میکند. بعضی از سیستمها از جمله تمام سیستم های برنامه سازی منطقی، از بررسی وقوع صرف نظر میکنند و در نتیجه واسط های نامعقولی را به بوجود می آورند. سیستم های دیگر از الگوریتم های پیچیده ای با پیچیدگی زمانی خطی استفاده میکنند.
شبه کد الگوریتم یکسان سازی
function UNIFY (x, y, θ) returns a substitution to make x and y identical
inputs : x , a variable, constant, list, or compound expression
y , a variable, constant, list, or compound expression
θ , the substitution built up so far(optional , defaults to empty)
if θ = failure then return θ
else if x = y then return θ
else if VARIABLE?( x) then return UNIFY-VAR(x, y, θ)
else if VARIABLE?( y) then return UNIFY-VAR(y, x, θ)
else if COMPOUND?(x) and COMPOUND?(y) then return UNIFY(x.ARGS, y.ARGS, UNIFY(x.OP , y.OP , θ) )
else if LIST?(x) and LIST?(y) then return UNIFY(x. REST, y.REST, UNIFY(x.FIRST , y.FIRST, θ) )
else return failure
function UNIFY-VAR(var, x , θ) ) returns a substitution
if {var / val} عضو θ then return UNIFY(var, x, θ)
else if {x / val} عضو θ then return UNIFY(var, val, θ)
else if OCCUR-CHECK?(var, x) then return failure
else return add {var / x} to θ
