تعبير Lambda حساب التفاضل والتكامل

Question

لتعبير Lambda (x (λx y. x y) z h), ، لم أفهم كيف المتغيرات الحرة x (outer x), z و h يمكن تحويلها في رمز C؟

التحيات ، داركي

Answer 1

المتغيرات الحرة هي حالة خاصة في حساب التفاضل والتكامل Lambda - لا يمكن "تحويلها" إلى أي شيء ، لذلك عادةً ما يتم اعتبارها رموزًا فقط. في مثالك ، وبالنظر إلى بعض المنشئين الوهميين لتعبيرات Lambda ، يمكنك ترجمتها إلى التعبير التالي (الذي يتضمن التعامل مع الكاري الضمني) التعبير C-like:

mk_app(mk_app(mk_app(mk_sym("x"),
                     mk_lam("x",
                            mk_lam("y",
                                   mk_app(mk_var("x"),
                                          mk_var("y"))))),
              mk_sym("z")),
       mk_sym("h"));

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

(راجع للشغل ، الجزء ذي الصلة هنا هو افتراض المتغير الحرة لـ BarendRegt.)

Answer 2

تحويل حساب التفاضل والتكامل Lambda إلى رمز C غير تافهة. عادةً ما تكتب مترجمًا ، يقوم بتقييم خطوة بخطوة. وهذا يعني ، حول التعبير إلى شجرة ، وابحث عن العقدة الأقرب إلى الجذر الذي يعد تطبيقًا مع وجود الجانب الأيسر هو lambda. الآن استبدل في الجانب الأيمن. كرر حتى لا تتمكن من تطبيق المزيد ، ولديك النتيجة.

لاحظ أنه لا يوجد ما يعادل مباشرة للمتغيرات الحرة هنا ؛ نحن فقط نستخدمهم لمعرفة مكان استبدال الأشياء.

ضع في اعتبارك أن معادلة تورينج لا تتطلب بالضبط التكافؤ بين أي مفاهيم بلغتين تكتمل. إنه يتطلب ببساطة أن تكون قادرًا على محاكاة واحدة مع الآخر ، والعكس صحيح.