نظرية سكوت-كاري

في المنطق الرياضي ، تُعد نظرية سكوت-كاري نتيجة في حساب لامدا تنص على أنه إذا كانت مجموعتان غير فارغتين من حدود لامدا A و B مغلقة تحت التحويل بيتا، فإنهما غير قابلتين للفصل بشكل متكرر . ^{[ 1 ]}

تكون المجموعة A من حدود لامدا مغلقة تحت قابلية التحويل بيتا إذا كان لأي حدي لامدا X و Y، إذا${\displaystyle X\in A}$وإذا كان X مكافئًا لـ Y من النوع β،${\displaystyle Y\in A}$يمكن فصل مجموعتين A و B من الأعداد الطبيعية بشكل متكرر إذا وُجدت دالة قابلة للحساب${\displaystyle f:\mathbb {N} \rightarrow \{0,1\}}$بحيث${\displaystyle f(a)=0}$لو${\displaystyle a\in A}$و${\displaystyle f(b)=1}$لو${\displaystyle b\in B}$. يمكن فصل مجموعتين من مصطلحات لامدا بشكل متكرر إذا كانت مجموعاتهما المقابلة تحت ترقيم غودل قابلة للفصل بشكل متكرر، وغير قابلة للفصل بشكل متكرر خلاف ذلك.

تنطبق نظرية سكوت-كاري بالتساوي على مجموعات المصطلحات في المنطق التوافقي مع المساواة الضعيفة. وهي تُشابه نظرية رايس في نظرية الحوسبة، التي تنص على أن جميع الخصائص الدلالية غير التافهة للبرامج غير قابلة للتقرير.

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

تم اقتباس البرهان من باريندريخت في كتابه "حساب لامدا" . ^{[ 2 ]}

لتكن A و B مجموعتين مغلقتين تحت تحويل بيتا، ولتكن a و b تمثيلات حد لامدا لعناصر من A و B على التوالي. لنفترض جدلاً أن f حد لامدا يمثل دالة قابلة للحساب بحيث${\displaystyle fx=0}$لو${\displaystyle x\in A}$و${\displaystyle fx=1}$لو${\displaystyle x\in B}$(حيث المساواة هي مساواة من النوع β). ثم عرّف${\displaystyle G\equiv \lambda x.{\text{if}}\ ({\text{zero?}}\ (fx))ab}$. هنا،${\displaystyle {\text{صفر؟}}}$تكون صحيحة إذا كانت قيمة وسيطها صفرًا، وخاطئة فيما عدا ذلك، و${\displaystyle {\text{if}}}$هي الهوية بحيث${\displaystyle {\text{if}}\ bxy}$يساوي x إذا كانت b صحيحة، و y إذا كانت b خاطئة.

ثم${\displaystyle x\in C\implies Gx=a}$وبالمثل،${\displaystyle x\notin C\implies Gx=b}$بحسب نظرية الاستدعاء الذاتي الثانية، يوجد حد X يساوي f مطبقًا على رقم الكنيسة لترقيم غودل الخاص به، X ' . عندئذٍ${\displaystyle X\in C}$يشير ذلك إلى أن${\displaystyle X=G(X')=b}$في الواقع${\displaystyle X\notin C}$الافتراض العكسي${\displaystyle X\notin C}$أعطِ${\displaystyle X=G(X')=a}$لذا${\displaystyle X\in C}$في كلتا الحالتين، نصل إلى تناقض، وبالتالي لا يمكن أن تكون f دالة تفصل بين A و B. ومن ثم فإن A و B غير قابلتين للفصل بشكل متكرر.

أثبت دانا سكوت النظرية لأول مرة عام 1963. وقد أثبت هاسكل كاري النظرية، بصيغة أقل عمومية، بشكل مستقل . ^{[ 3 ]} ونُشرت في ورقة كاري البحثية عام 1969 بعنوان "عدم قابلية الحسم في تحويل λK". ^{[ 4 ]}