ما هي خوارزمية "الموحد الأكثر عمومية" الأمثل؟

Question

السؤال

ما هي خوارزمية MGU الأكثر كفاءة؟ما هو تعقيدها الزمني؟هل من السهل وصفها بأنها إجابة تجاوز سعة المكدس؟

لقد كنت أحاول العثور على الإجابة على Google ولكني أستمر في العثور على ملفات .PDF الخاصة التي لا يمكنني الوصول إليها إلا من خلال اشتراك ACM.

لقد وجدت مناقشة واحدة في SICP: هنا

شرح ما هي "خوارزمية التوحيد الأكثر عمومية":خذ شجرتي تعبير تحتويان على "المتغيرات الحرة" و"الثوابت"...على سبيل المثال

 e1 = (+ x? (* y? 3) 5)
 e2 = (+ z? q? r?)

ثم تقوم خوارزمية Unifier الأكثر عمومية بإرجاع المجموعة الأكثر عمومية من الارتباطات التي تجعل التعبيرين متساويين.

أي.

mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5

من خلال "الأكثر عمومية"، يمكنك بدلاً من ذلك ربط (x = 1) و(z = 1) وهذا من شأنه أيضًا أن يجعل e1 وe2 متكافئين ولكنه سيكون أكثر تحديدًا.

يبدو أن مقالة SICP تشير ضمنًا إلى أنها باهظة الثمن إلى حد معقول.

للحصول على معلومات، سبب سؤالي هو أنني أعلم أن استنتاج النوع يتضمن أيضًا خوارزمية "التوحيد" هذه وأود أن أفهمها.

Answer 1

الخوارزمية البسيطة المستخدمة في الممارسة العملية (على سبيل المثال.في Prolog) هو الأسي للحالات المرضية.

هناك خوارزمية أكثر كفاءة من الناحية النظرية من قبل مارتيلي ومونتاناري (IIRC وهي خطية)، ولكنها أبطأ بكثير بالنسبة للحالات البسيطة التي تحدث في الممارسة العملية، لذلك لا يتم استخدامها كثيرًا.

Answer 2

بادر وسنايدر نشر العديد من خوارزميات التوحيد، لكل من التوحيد النحوي والتوحيد المعادلة.

يذكرون أن خوارزمية التوحيد النحوي الثالثة (في القسم 2.3) تعمل في O(n alpha(n)) حيث alpha(n) هي دالة أكرمان العكسية - في المواقف العملية تعادل ثابتًا صغيرًا.