أرقام الكنيسة للإضافة

Question

أنا عالق في الخطوة التالية. سيكون من الرائع أن يساعدني شخص ما:

2 = λfx.f(f x)
3 = λfx.f(f(f x))
ADD = λm n f x. m f (n f x)

خطواتي هي:

   (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> ((λn f x. (λf x.f(f(f x))) f (n f x))) (λf x.f(f x))
-> ((λf x. (λf' x'.f'(f'(f' x'))) f ((λf" x".f"(f" x")) f x)

هل الموظفين بخير؟ أنا حقا خلط نفسي في البدائل والأقواس. هل هناك تقنية رسمية وأسهل لمعالجة مثل هذه المشكلات؟

Answer 1

محاولة البيض التمساح!

إليكم خطواتي ، التي اشتقتها بمساعدة بيض التمساح:

ADD 2 3
-> (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
->   (λn f x. (λf x.f(f(f x))) f (n f x))   (λf x.f(f x))
->     (λf x. (λf x.f(f(f x))) f ((λf x.f(f x)) f x)) 
->     (λf x.   (λx.f(f(f x)))   ((λf x.f(f x)) f x)) 
->     (λf x.       f(f(f(λf x.f(f x)) f x)))))
->     (λf x.       f(f(f  (λx.f(f x)) x)))))
->     (λf x.       f(f(f     (f(f x))  )))))

Answer 2

نصيحتي ، من تجربتي المحدودة ولكن الحديثة:

1. يفعل واحد الشيء في وقت واحد: إجراء تحويل ألفا أو تخفيض بيتا أو تحويل ETA. لاحظ في هامش الصفحة التي تعمل على الخطوة التي اتخذتها للوصول إلى السطر التالي. إذا لم تكن هذه الكلمات مألوفة لك ، فما الذي سيكون عليه - فقط ألق نظرة ويكيبيديا.

ملخص سريع لخطوات التخفيض هذه:

ألفا تعني فقط تغيير أسماء المتغيرات في سياق باستمرار:

λfx. f (f x) => λgx. g (g x)

Beta يعني فقط تطبيق Lambda على واحد جدال

(λf x. f x) b => λx. b x

ETA هي ببساطة "تفكيك" وظيفة ملفوفة غير ضرورية لا تغير معناها.

λx.f x => f

ثم

2. يستخدم الكثير من تحويل ألفا لتغيير أسماء المتغيرات لجعل الأمور أكثر وضوحا. كل هؤلاء fق ، سيكون دائمًا مربكًا. لقد فعلت شيئًا مشابهًا مع " في صفك الثاني

3. أدعي أنك جهاز كمبيوتر! لا تقفز للأمام أو تخطي خطوة عندما تقوم بتقييم التعبير. فقط افعل الشيء التالي (وشيء واحد فقط). تحرك فقط بشكل أسرع بمجرد أن تكون واثقًا من التحرك ببطء.

4. فكر في تسمية بعض التعبيرات واستبدالها فقط بتعبيرات Lambda الخاصة بهم عندما تحتاج إلى تقييمها. ألاحظ عادة الاستبدال في هامش الصفحة كما by def لأنها ليست حقا خطوة تخفيض. شيء مثل:

   add two three 
   (λm n f x. m f (n f x)) two three | by def
   

لذا اتباع القواعد المذكورة أعلاه ، إليك مثال العمل الخاص بي:

two   = λfx. f (f x)
three = λfx. f (f (f x))
add   = λmnfx. m f (n f x)

0  | add two three 
1  | (λm n f x. m f (n f x)) two three           | by def
2  | (λn f x. two f (n f x)) three               | beta
3  | (λf x. two f (three f x))                   | beta
4  | (λf x. two f ((λfx. f (f (f x))) f x))      | by def
5  | (λf x. two f ((λgy. g (g (g y))) f x))      | alpha
6  | (λf x. two f ((λy. f (f (f y))) x))         | beta
7  | (λf x. two f (f (f (f x))))                 | beta
8  | (λf x. (λfx. f (f x)) f (f (f (f x))))      | by def
9  | (λf x. (λgy. g (g y)) f (f (f (f x))))      | alpha
10 | (λf x. (λy. f (f y)) (f (f (f x))))         | beta
11 | (λf x. (λy. f (f (f (f (f x))))))           | beta

Answer 3

هل هناك تقنية رسمية وأسهل لمعالجة مثل هذه المشكلات؟

إنها كثير أسهل في كتابة مخفض وبراعة جميلة لشروط Lambda من القيام بالتخفيضات باليد. ولكن PLT REDEX يمكن أن يعطيك ساقا على التخفيضات. حاول تحديد قواعد لتقليل الطلب الطبيعي ، ثم كل ما عليك فعله هو القلق بشأن طباعة جميلة النتائج مع عدم وجود أقواس زائدة.

من المحتمل أن تتعلم الكثير أيضًا.