حالة غير ضرورية على ما يبدو في خوارزمية التوحيد في SICP

Question

أحاول فهم خوارزمية التوحيد الموضحة في SICP هنا

على وجه الخصوص، في إجراء "التمديد إن أمكن"، هناك علامة اختيار (المكان الأول مميز بعلامة النجمة "*") والذي يتم التحقق لمعرفة ما إذا كان "التعبير" الأيمن هو متغير مرتبط بالفعل بشيء ما في الإطار الحالي:

(define (extend-if-possible var val frame)
  (let ((binding (binding-in-frame var frame)))
    (cond (binding
       (unify-match
        (binding-value binding) val frame))
      ((var? val)                      ; *** why do we need this?
       (let ((binding (binding-in-frame val frame)))
         (if binding
             (unify-match
              var (binding-value binding) frame)
             (extend var val frame))))
      ((depends-on? val var frame)
       'failed)
      (else (extend var val frame)))))

ينص التعليق المرتبط على ما يلي:

"في الحالة الأولى، إذا كان المتغير الذي نحاول مطابقته غير مرتبط، ولكن القيمة التي نحاول مطابقته بها هي في حد ذاتها متغير (مختلف)، فمن الضروري التحقق لمعرفة ما إذا كانت القيمة مرتبطة، و إذا كان الأمر كذلك، لتتناسب مع قيمتها.إذا كان طرفا المباراة غير ملتزمين، يجوز لنا ربط أي منهما بالآخر".

ومع ذلك، لا أستطيع التفكير في حالة يكون فيها هذا ضروريًا بالفعل.

ما الذي يتحدث عنه، أنا يفكر, ، هو المكان الذي قد تكون فيه روابط الإطارات التالية موجودة حاليًا:

{?y = 4}

ثم يُطلب منهم "تمديد IfPossible" رابطًا من ?z إلى ?y.

مع وجود علامة الاختيار "*"، عندما يُطلب منا توسيع "?z" مع "?y"، نرى أن "?y" مرتبط بالفعل بـ 4، ثم نحاول بشكل متكرر توحيد "?z" مع "4"، مما يؤدي إلى تمديد الإطار بـ "?z = 4".

بدون علامة التحديد، سينتهي بنا الأمر إلى توسيع الإطار باستخدام "?z = ?y" فقط.لكن في كلتا الحالتين، طالما أن ?z غير مرتبط بالفعل بشيء آخر، فلا أرى المشكلة.

ملاحظة، إذا ؟ز ملك تم ربطه بالفعل بشيء آخر، وبالتالي فإن الكود لا يصل إلى الجزء الذي يحمل علامة "*" (كنا قد لجأنا بالفعل إلى التوحيد مع ما تمت مطابقة ?z معه بالفعل).

بعد التفكير مليًا، أدركت أنه قد يكون هناك نوع من الحجة لإنشاء MGU "الأبسط" (الموحد الأكثر عمومية).على سبيل المثالقد ترغب في الحصول على وحدة MGU تحتوي على أقل عدد ممكن من المتغيرات التي تشير إلى متغيرات أخرى...أي أننا نفضل إنشاء الاستبدال {?x = 4, ?y = 4} بدلاً من الاستبدال {?x = ?y, ?y = 4}...لكنني لا أعتقد أن هذه الخوارزمية ستضمن هذا السلوك بأي حال من الأحوال، لأنه إذا طلبت منها توحيد "(?x 4)" مع "(?y ?y)" فسينتهي الأمر بـ {?x = ?y, ?y = 4}.وإذا كان السلوك لا يمكن ضمانه، فلماذا التعقيد الإضافي؟

هل تفكيري هنا كله صحيح؟إذا لم يكن الأمر كذلك، فما هو المثال المضاد حيث يكون التحقق "*" ضروريًا لإنشاء ملف صحيح MGU؟

Answer 1

وهذا سؤال جيد!

وأعتقد أن السبب هو أنك لا تريد في نهاية المطاف مع الارتباطات دائرية مثل { ?x = ?y, ?y = ?x }. على وجه الخصوص، فإن (?x ?y) توحيد مع (?y ?x) تعطيك إطار دائري أعلاه إذا كنت حذف الاختيار. مع الاختيار، يمكنك الحصول على إطار {؟ س =؟ ص} كما هو متوقع.

والارتباطات التعميم في إطار سيئة، لأنها قد تسبب ظائف يؤدون بدائل باستخدام الإطار، مثل instantiate، لتشغيل في حلقة لا نهائية.

Answer 2

وبدون ذلك، لن تحصل على الأكثر عمومية الموحد.لا يزال هناك عمل يتعين القيام به:توحيد x و y.