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

Question

أنا أعمل على أسئلة التمرين في الكتاب حساب حساب Lambda. أحد الأسئلة التي أتعثر فيها هو إثبات ما يلي: أظهر أن التطبيق غير مرتبط ؛ في الواقع ، X (YZ) لا يساوي (xy) z

هذا ما عملت عليه حتى الآن:

Let x = λa.λb. ab
Let y = λb.λc. bc
Let z = λa.λc. ac

(xy)z => ((λa.λb. ab) (λb.λc. bc)) (λa.λc. ac)    
=> (λb. (λb.λc. bc) b) (λa.λc. ac)    
=> (λb.λc. bc) (λa.λc. ac)    
=> (λc. (λa.λc. ac) c)

x(yz) => (λa.λb. ab) ((λb.λc. bc) (λa.λc. ac))    
=> (λb. ((λb.λc. bc) (λa.λc. ac)) b)    
=> (λb. (λc. (λa.λc. ac) c) b)

هل هذا صحيح؟ الرجاء مساعدتي في الفهم.

Answer 1

الاشتقاقات تبدو جيدة ، في لمحة.

من الناحية المفاهيمية ، فقط أعتقد أن X و Y و Z يمكن أن تمثل أي وظائف قابلة للحساب ، ومن الواضح أن بعض هذه الوظائف ليست مرتبطة. قل ، x هو "اطرح 2" ، y هو "Divide by 2" ، و Z هو "مزدوج". على سبيل المثال ، x (yz) = 'اطرح 2' و (xy) z = 'substract 1'.

Answer 2

أعتقد أيضًا أن مثالك المضاد صحيح.
ربما يمكنك الحصول على مثال مضاد أبسط مثل هذا:

يترك x = λa.n و ذ, ض المتغيرات ثم:

(xy) z => ((λa.n) y) z => nz
x (yz) => (λa.n) (yz) => n

Answer 3

يبدو الأمر جيدًا ، ولكن من أجل البساطة ، ماذا عن إثبات التناقض؟

افترض (xy) z = x (yz) ، ودع

x = λa.λb. a     # x = const
y = λa. -a       # y = negate
z = 1            # z = 1

وأظهر أن ((xy) z) 0 ≠ (x (yz)) 0.

Answer 4

الكتاب الذي ذكرته بواسطة BarendRegt رسمي للغاية ودقيق (كتاب رائع) ، لذلك سيكون من الجيد أن يكون لديك البيان الدقيق للتمرين.

أعتقد أن الهدف الفعلي هو العثور على مثيلات لـ x و y و z بحيث يقلل x (yz) إلى true boolean = xy.x و (xy) z يقلل إلى boolean false = xy.y

بعد ذلك ، يمكنك أن تأخذ على سبيل المثال x = z.true و z = i = zz (y تعسفي).

ولكن كيف يمكننا إثبات أن هذا صحيح غير قابل للتحويل مع خطأ؟ ليس لديك طريقة لإثبات ذلك داخل حساب التفاضل والتكامل ، نظرًا لأنه ليس لديك نفي: لا يمكنك إثبات سوى المساواة وليس عدم المساواة. ومع ذلك ، دعونا نلاحظ أنه إذا كان صحيحًا = خطأ ، فكل المصطلحات متساوية.

في الواقع ، لأي m و n ، إذا كان صحيحًا = خطأ إذن

                         true M N = false M N

لكن MN True يقلل إلى M ، بينما يقلل MN الخاطئ إلى N ، لذلك ،

                              M = N

وبالتالي ، إذا كان صحيحًا = خطأ فكل الشروط ستكون متساوية ، وستكون حساب التفاضل والتكامل تافهة. نظرًا لأننا لا نستطيع العثور على نماذج تافهة لحساب Lambda ، فإن أي نموذج قد يساوي هذا صحيحًا وكاذبًا (قد يعادل بشكل عام مصطلحات مع أشكال طبيعية مختلفة ، وهذا يتطلب منا التحدث عن تقنية Bohm-Out).