combinator المنطق البديهيات

Question

أنا أجري بعض التجارب في النظرية التي تثبت مع Combinator Logic ، والتي تبدو واعدة ، ولكن هناك كتلة عثرة واحدة: لقد تمت الإشارة إلى أنه في منطق combinator ، صحيح أن على سبيل المثال i = skk ولكن هذه ليست نظرية ، إنها يجب إضافة بديسيوم. هل يعرف أي شخص قائمة كاملة من البديهيات التي تحتاج إلى إضافتها؟

تحرير: يمكنك بالطبع أن تثبت باليد أنني = skk ، ولكن ما لم أفتقد شيئًا ، فهي ليست نظرية في نظام منطق combinator مع المساواة. بعد قول ذلك ، يمكنك فقط التوسع في الماكرو إلى التزحلق ... لكنني ما زلت أفتقد شيئًا مهمًا. أخذ مجموعة من الجمل P (x) و ~ p (x) ، والتي تحل بسهولة إلى تناقض في منطق الترتيب الأول العادي ، وتحويلها إلى SK ، وإجراء الاستبدال وتقييم جميع مكالمات S و K ، يولد برنامجي فيما يلي (حيث أستخدم 'for Unlambda's Backtick):

'eq' 's' s 's' ks '' s 's' ks 's' kk 'k eq' 's' ks 'kk' kk 's' kk 'k false "K True" K True

يبدو أن ما أحتاجه هو مجموعة مناسبة من القواعد للتعامل مع المكالمات الجزئية "K و" S ، أنا فقط لا أرى ما ينبغي أن تكون عليه هذه القواعد ، وجميع الأدبيات التي يمكنني العثور عليها في هذا المجال مكتوب من أجلها جمهور مستهدف من علماء الرياضيات وليس المبرمجين. أظن أن الإجابة ربما تكون بسيطة جدًا بمجرد فهمها.

Answer 1

بعض الكتب المدرسية تعريف أنا كما مجرد اسم مستعار ل ((SK) K). في هذه الحالة فهي متطابقة (كشروط) لكل تعريف. لإثبات المساواة (كوظائف) ، نحتاج فقط لإثبات أن المساواة انعكاس ، والتي يمكن تحقيقها من خلال مخطط axiox الانعكاسية:

• الاقتراح ``ه = ه"" قابلة للاستفادة (الانعكاسية مخطط Axiom ، تم إنشاء مثيله لكل مصطلحات محتملة يدل عليها Metavariable ه)

وهكذا ، أفترض في ما يلي ، أن أسئلتك تحقق نهجًا آخر: عندما تكون combinator أنا لم يتم تعريفه على أنه أ مجرد الاسم المستعار لمركز مركب ((SK) K), ، ولكن تم تقديمه ك combinator الأساسي المستقل ثابت من تلقاء نفسه ، والتي يتم الإعلان عن دلالاتها التشغيلية صراحة بواسطة axiom مخطط

• ``(أنا ه) = ه"" قابلة للاستفادة (i-axiom مخطط)

أفترض أن سؤالك يسأل

سواء كان بإمكاننا أن نستنتج رسميًا (تبقى داخل النظام) ، فهذا محدد محدد أنا يتصرف بالضبط كما ((SK) K), ، عند استخدامها كوظائف في التخفيضات؟

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

أعتقد أنه يتعين علينا تبني مثل هذا النهج لبناء المنطق التوافقي ، بحيث يتعين علينا أيضًا السماح باستخدام المتغيرات في الكائن langauge. بالطبع ، أعني "فقط" مجانا الأشياء الثمينة. استخدام المتغيرات المربوطة سيكون الغش ، يجب أن نبقى داخل عالم المنطق المشترك. إن استخدام Varaibles المجاني ليس غشًا ، إنه أداة صادقة. وبالتالي ، يمكننا أن نفعل الدليل الرسمي الذي تحتاجه.

إلى جانب البديهيات المساواة المباشرة وقواعد الاستدلال (النقل ، الانعكاسية ، التماثل ، قواعد Leibniz) ، يجب علينا إضافة ملف التوسيع قاعدة الاستدلال للمساواة. هذه هي النقطة التي تهم المتغيرات الحرة.

في Csörnyei 2007: 157-158 ، لقد وجدت النهج التالي. أعتقد بهذه الطريقة يمكن القيام بالدليل.

بعض الملاحظات:

معظم البديهيات في الواقع مخططات البديهية, ، التي تتكون من العديد من مثيلات البديهية. يجب إنشاء مثيل للحالات لكل ممكن ه, F, ز مصلحات. هنا ، أستخدم مائل للميتافاريات.

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

الآن دعونا نظهر إطار عملنا:

لغة

الأبجدية

الثوابت: الثلاثة التالية تسمى الثوابت: ك, س, أنا.

أضفت الثابت أنا فقط لأن سؤالك يفترض أننا لم نحدد المشابك أنا كما مجرد الاسم المستعار/الماكرو لمركز مركب س ك ك, ، لكنه ثابت مستقل من تلقاء نفسه.

سأشير إلى الثوابت من قبل العواصم الرومانية Boldface.

علامة التطبيق: علامة @ من "التطبيق" كافية (تدوين البادئة مع arity 2). بصفتي سكر النحوي ، أستخدم هنا جنودًا بدلاً من علامة التطبيق الصريحة: سأستخدم علامات الفتح (والإغلاق) الصريحة.

المتغيرات: على الرغم من أن منطق Combinator لا يستفيد من المتغيرات المرتبطة ، والنطاق وما إلى ذلك ، ولكن يمكننا تقديم متغيرات مجانية. أظن أنهم ليسوا فقط السكر النحوي ، بل يمكنهم تعزيز نظام الخصم أيضًا. أنا أخطط ، أن سؤالك سيتطلب استخدامهم. أي مجموعة لا حصر لها من اللانهائي (تفكيك الثوابت وعلامات الأقواس) ستعمل كأبجدية للمتغيرات ، سأشير إليها هنا بأحرف صغيرة رومانية غير مفيدة X ، Y ، Z ...

مصلحات

يتم تعريف الشروط بشكل استقرائي:

• أي ثابت هو مصطلح
• أي متغير مصطلح
• لو ه هو مصطلح ، و F هو مصطلح أيضا ، ثم (أيضا (ه F) هو مصطلح

أستخدم أحيانًا اتفاقيات عملية كسكر نحوي ، على سبيل المثال الكتابة

ه F ز ح

بدلاً من

(((ه F) ز) ح).

المستقطع

مخططات التحويل:

• ``ك ه F = ه"" قابلة للاستفادة (K-axiom مخطط)
• ``س F ز ح = F ح (ز ح) "" قابلة للاستفادة (S-Axiom مخطط)
• ``أنا ه = ه"" قابلة للاستفادة (i-axiom مخطط)

أضفت Axiom التحويل الثالث (أنا القاعدة) فقط لأن سؤالك يفترض أنه لم نقم بذلك يعرف المشابك أنا كمستعار/ماكرو ل س ك ك.

مخططات البديهية المساواة وقواعد الاستدلال

• ``ه = ه"" قابلة للاستفادة (الانعكاسية بديهية)
• لو "ه = F"قابلة للاستفادة ، ثم"F = ه"كما أنه قابل للاستفادة (تناظر قاعدة الاستدلال)
• لو "ه = F"استنتاجي ، و"F = ز"هو استنتاج أيضًا ، ثم"ه = ز"يمكن اختزاله (عبورية القاعدة)
• لو "ه = F"قابلة للاستفادة ، ثم"ه ز = F ز"كما أنه قابل للاستفادة (القاعدة ليبنيز أنا)
• لو "ه = F"قابلة للاستفادة ، ثم"ز ه = ز F"كما أنه قابل للاستفادة (القاعدة ليبنيز الثاني)

سؤال

الآن دعونا نتحقق من سؤالك. أتخمين أن نظام الخصم الذي تم تعريفه حتى الآن ليس قويًا بما يكفي لإثبات سؤالك.

هو اقتراح "أنا = س ك ك"استنتاج؟

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

لو ه F = ز F قابلية للاستفادة ، ثم أيضًا ه = ز قابلية للاستفادة

سيفشل في القيام بهذه المهمة: يمكننا أن نرى أن هذا لا ينتج ما نريد. باستخدامه ، يمكننا إثبات ذلك

``أنا ه = س ك ك ه"" قابلة للاستفادة

لكل ه مثيل المصطلح ، ولكن هذه النتائج مفصولة فقط حالات ، ولا يمكن استخدامها ككل لمزيد من الخصومات. لدينا نتائج ملموسة فقط (بلا حدود كثيرة) ، وليس قادرين على تلخيصها:

• انها تحمل ل ه := ك
• يحمل ل ه := س
• انها تحمل ل ه := ك ك
• .
• .
• .

...

لا يمكننا تلخيص هذه الحالات الناتجة المجزأة إلى نتيجة رائعة واحدة ، مع توضيح توسيع! لا يمكننا صب هذه الشظية ذات القيمة المنخفضة في القمع قاعدة من الاستدلال من شأنها أن تذوبها معًا في نتيجة واحدة أكثر قيمة.

علينا أن نزيد من قوة نظام الخصم لدينا. علينا أن نجد أداة رسمية يمكنها فهم المشكلة. تؤدي أسئلتك إلى توسيع ، وأعتقد أن احتياجات التوسيع التي يمكننا طرحها مقترحات تحمل مثيلات ***** *****. لهذا السبب أعتقد أننا يجب أن نسمح للمتغيرات الحرة داخل لغة كائننا. أنا أخطط أن قاعدة الاستدلال الإضافية التالية ستقوم بالعمل:

• إذا لم يكن المتغير x جزءًا من المصطلحات لا ه ولا F, وبيان (ه x) = (F س) قابلية للاستفادة ، ثم ه = F كما أنه قابل للاستفادة (التوسيع قاعدة الاستدلال)

الشيء الصعب في هذا البديهية ، مما يؤدي بسهولة إلى الارتباك: X هو هدف المتغيرات ، تحرر بالكامل وتحترم أجزاء من لغة الكائن لدينا ، بينما ه و ز نكون ميتاالمتغيرات ، وليس أجزاء من لغة الكائن ، ولكن تستخدم فقط لتدوين موجز لمخططات البديهية.

(ملاحظة: بشكل أدق ، يجب إضفاء الطابع الرسمي على قاعدة الامتداد ميتاعامل x أكثر من ذلك ممكن هدف المتغيرات X ، Y ، Z ... ، وكذلك نوع آخر من ميتاعامل ه أكثر من ذلك ممكن مثيلات مصطلح. لكن هذا التمييز بين النوعين من metavariables بالإضافة إلى أن متغيرات الكائن ليست تعليمية هنا ، فهو لا يؤثر على سؤالك كثيرًا.)

دليل - إثبات

دعونا نثبت الآن الاقتراح بأن ""أنا = س ك ك''.

خطوات الجانب الأيسر:

• الاقتراح ``أنا x = x '' هو مثيل i-axiom مخطط مع Instatiation [ه : = x

خطوات للجانب الأيمن:

• اقتراح "س ك ك x = ك x (ك س) "هو مثال S-Axiom مخطط مع إنشاءات [ه := ك, F := ك, ز : = x] ، وبالتالي فهي قابلة للاستفادة
• اقتراح "ك x (ك x) = x "هو مثيل K-axiom مخطط مع إنشاءات [ه : = x ، F := ك س] ، وبالتالي فهي قابلة للاستفادة

انتقال المساواة:

• إفادة "س ك ك x = ك x (ك س) "تطابق الفرضية الأولى من عبورية قاعدة الاستدلال ، والبيان "ك x (ك x) = x "يطابق الفرضية الثانية لقاعدة الاستدلال هذه.ه := س ك ك x ، F := ك x (ك س) ، ز = x]. وبالتالي فإن الاستنتاج ينطبق أيضًا على: ه = ز. إعادة كتابة الاستنتاج مع نفس الخصائص ، نحصل على بيان "س ك ك x = x "، وبالتالي ، هذا أمر قابل للاستفادة.

تناظر المساواة:

• استخدام "س ك ك x = x "، يمكننا أن نستنتج" x = س ك ك x "

انتقال المساواة:

• استخدام "أنا x = x "و" x = س ك ك x "، يمكننا أن نستنتج"أنا x = س ك ك x "

الآن لقد مهد الطريق للنقطة الحاسمة:

• اقتراح "أنا x = س ك ك X "تطابق مع الفرضية الأولى من تمديد قاعدة الاستدلال: (ه x) = (F س) ، مع إنشاءات [ه := أنا, F := س ك ك]. وبالتالي ، يجب أن يكون الاستنتاج أيضًا ، أي "،"ه = F"مع نفس الخصائص ([[ه := أنا, F := س ك ك]) ، الاقتراح العائد "أنا = س ك ك"، Quod erat perfectandum.

---

Csörnyei ، Zoltán (2007): Lambda-Kalkulus. A funkcionális programozás alapjai. بودابست: Typotex. ISBN-978-963-9664-46-3.

Answer 2

لا تحتاج إلى تعريف أنا كطبيب. ابدأ بما يلي:

I.x = x
K.x y = x
S.x y z = x z (y z)

حيث SKاى شى = اى شى, ، من ثم SKاى شى هي وظيفة الهوية ، تماما مثل I.

لذا، I = SKK و I = SKS. لا حاجة لتعريف I على أنها بديهية ، يمكنك تعريفه على أنه سكر بناء الجملة الذي يمتلك الأسماء المستعارة.

تعريفات S و K هل أنت فقط البديهيات.

Answer 3

البديهيات المعتادة كاملة للمساواة بين بيتا ، ولكن لا تعطي ETA المساواة. وجد كاري مجموعة من حوالي ثلاثين بديهية للمعتاد للحصول على اكتمال المساواة بين بيتا-إيتا. لقد تم إدراجهم في Hindley & Seldin's مقدمة للمجموعات و Lambda-Calculus.

روجر هيندلي ، مشكلة كاري الأخيرة, ، يسرد بعض desiderata الإضافية التي قد نريدها من التعيينات بين حساب التفاضل والتكامل Lambda وتلاحظ أنه ليس لدينا تعيينات ترضيها جميعًا. من المحتمل ألا تهتم كثيرًا بجميع المعايير.