المنطق التوافقي

📅 آخر تحديث: ٢٦ يوليو ٢٠٢٦
✍️ نُشر في: ٢٦ يوليو ٢٠٢٦
📷 يحتوي على 62 صور
الموسوعة الحرة

المنطق التوافقي هو أسلوب ترميز يُستخدم للاستغناء عن المتغيرات الكمية في المنطق الرياضي . وقد طوّره موسى شونفينكل [ 1 ] وهاسكل كاري [ 2 ] ، ويُستخدم مؤخرًا في علوم الحاسوب كنموذج نظري للحوسبة ، وأيضًا كأساس لتصميم لغات البرمجة الوظيفية . وهو قائم على المُركِّبات ، التي قدّمها شونفينكل عام 1920 بهدف توفير طريقة مماثلة لبناء الدوال - والاستغناء عن أي ذكر للمتغيرات - لا سيما في منطق المسندات . المُركِّب هو دالة من الرتبة العليا تستخدم فقط تطبيق الدالة والمُركِّبات المُعرَّفة سابقًا لتحديد نتيجة من مُدخلاتها.

في الرياضيات

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

لم ينشر موسى شونفينكل ، مخترع المنطق التوافقي، أي شيء حول هذا الموضوع بعد بحثه الأصلي عام ١٩٢٤. أعاد هاسكل كاري اكتشاف التوافقيات أثناء عمله كمدرس في جامعة برينستون أواخر عام ١٩٢٧. [ ٣ ] في أواخر ثلاثينيات القرن العشرين، ابتكر ألونسو تشيرش وطلابه في برينستون صيغةً منافسةً للتجريد الوظيفي، وهي حساب لامدا ، الذي أثبت شعبيته الأكبر من المنطق التوافقي. نتيجةً لهذه الظروف التاريخية، وحتى بدأ علم الحاسوب النظري يهتم بالمنطق التوافقي في ستينيات وسبعينيات القرن العشرين، كانت جميع الأعمال تقريبًا في هذا المجال من قِبل هاسكل كاري وطلابه، أو روبرت فيس في بلجيكا . يستعرض كاري وفيس (١٩٥٨)، وكاري وآخرون (١٩٧٢) التاريخ المبكر للمنطق التوافقي. للحصول على معالجة أكثر حداثة للمنطق التوافقي وحساب لامدا معًا، انظر كتاب باريندريخت ، [ 4 ] الذي يستعرض النماذج التي وضعها دانا سكوت للمنطق التوافقي في الستينيات والسبعينيات.

في مجال الحوسبة

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

يمكن النظر إلى المنطق التوافقي على أنه شكل من أشكال حساب لامدا ، حيث تُستبدل تعابير لامدا (التي تُمثل التجريد الوظيفي) بمجموعة محدودة من المُركِّبات ، وهي دوال أولية بدون متغيرات حرة . من السهل تحويل تعابير لامدا إلى تعابير مُركِّبات، كما أن اختزال المُركِّبات أبسط بكثير من اختزال لامدا. لذا، استُخدم المنطق التوافقي لنمذجة بعض لغات البرمجة الوظيفية غير الصارمة وبعض الأجهزة . يُعدّ Unlambda أنقى أشكال هذا المنظور ، إذ تقتصر عناصره الأولية على المُركِّبات S و K المُدعَّمة بمدخلات/مخرجات حرفية. على الرغم من أن Unlambda ليست لغة برمجة عملية، إلا أنها ذات أهمية نظرية.

يمكن تفسير المنطق التوافقي بتفسيرات متعددة. وقد أوضحت العديد من الأبحاث المبكرة لكاري كيفية ترجمة مجموعات البديهيات للمنطق التقليدي إلى معادلات المنطق التوافقي. [ 5 ] كما أوضح دانا سكوت في الستينيات والسبعينيات من القرن الماضي كيفية الجمع بين نظرية النماذج والمنطق التوافقي.

ملخص حساب التفاضل والتكامل لامدا

يهتم حساب لامدا بالكائنات التي تسمى مصطلحات لامدا ، والتي يمكن تمثيلها بالأشكال الثلاثة التالية من السلاسل النصية:

  • v{\displaystyle v}
  • λv.هـ1{\displaystyle \lambda v.E_{1}}
  • (هـ1هـ2){\displaystyle (E_{1}E_{2})}

أينv{\displaystyle v}هو اسم متغير مُستمد من مجموعة لا نهائية مُحددة مسبقًا من أسماء المتغيرات، وهـ1{\displaystyle E_{1}}وهـ2{\displaystyle E_{2}}هي مصطلحات لامدا.

شروط النموذجλv.هـ1{\displaystyle \lambda v.E_{1}}تُسمى هذه المفاهيم بالتجريدات . المتغيرv{\displaystyle v}يُطلق عليه اسم المعامل الرسمي للتجريد، وهـ1{\displaystyle E_{1}}هو جوهر التجريد. المصطلحλv.هـ1{\displaystyle \lambda v.E_{1}}تمثل الدالة التي، عند تطبيقها على وسيط، تربط المعامل الرسميv{\displaystyle v}إلى الوسيط ثم يحسب القيمة الناتجة لـهـ1{\displaystyle E_{1}}أي أنها تعودهـ1{\displaystyle E_{1}}مع كل حدوث لـv{\displaystyle v}تم استبدالها بالوسيط.

شروط النموذجهـ1هـ2{\displaystyle E_{1}E_{2}}تُسمى هذه التطبيقات . تُمثل التطبيقات استدعاء أو تنفيذ الدالة: الدالة التي تُمثلهاهـ1{\displaystyle E_{1}}يتم استدعاؤه، معهـ2{\displaystyle E_{2}}كمعامل لها، ويتم حساب النتيجة. إذاهـ1{\displaystyle E_{1}}(يُطلق عليه أحيانًا اسم مقدم الطلب ) هو مفهوم مجرد، ويمكن اختصار المصطلح :هـ2{\displaystyle E_{2}}، يمكن استبدال الحجة في صلب الموضوعهـ1{\displaystyle E_{1}}بدلاً من المعامل الرسمي لـهـ1{\displaystyle E_{1}}والنتيجة هي مصطلح لامدا جديد مكافئ للمصطلح القديم. إذا لم يحتوي مصطلح لامدا على أي مصطلحات فرعية من الشكل((λv.هـ1)هـ2){\displaystyle ((\lambda v.E_{1})E_{2})}عندئذٍ لا يمكن اختزاله، ويقال إنه في شكله الطبيعي .

التعبيرهـ[v:=أ]{\displaystyle E[v:=a]}يمثل نتيجة أخذ المصطلحهـ{\displaystyle E}واستبدال جميع حالات الظهور المجانية لـv{\displaystyle v}فيه معأ{\displaystyle a}وهكذا نكتب

((λv.هـ)أ)⇒هـ[v:=أ]{\displaystyle ((\lambda vE)a)\Rightarrow E[v:=a]}

بحسب العرف، نأخذ(أبج){\displaystyle (abc)}كاختصار لـ((أب)ج){\displaystyle ((ab)c)}(أي أن التطبيق ترابطي من اليسار ).

يكمن الدافع وراء هذا التعريف للاختزال في أنه يجسد السلوك الأساسي لجميع الدوال الرياضية. على سبيل المثال، لنأخذ الدالة التي تحسب مربع عدد ما. يمكننا كتابة

مربعx{\displaystyle x}يكونx*x{\displaystyle x*x}

(استخدام "*{\displaystyle *}"للدلالة على الضرب.") x{\displaystyle x}هذا هو المعامل الرسمي للدالة. لحساب مربع القيمة لقيمة معينة، ولتكن 3، نقوم بإدخالها في تعريف الدالة بدلاً من المعامل الرسمي:

مربع3{\displaystyle 3}يكون3*3{\displaystyle 3*3}

لتقييم التعبير الناتج3*3{\displaystyle 3*3}، سيتعين علينا اللجوء إلى معرفتنا بالضرب والعدد 3. بما أن أي عملية حسابية هي ببساطة تركيب لتقييم دوال مناسبة على وسائط أولية مناسبة، فإن مبدأ الاستبدال البسيط هذا يكفي لفهم الآلية الأساسية للحساب. علاوة على ذلك، في حساب لامدا، مفاهيم مثل '3' و'*{\displaystyle *}يمكن تمثيل ' دون الحاجة إلى عوامل أو ثوابت أولية مُعرَّفة خارجيًا. من الممكن تحديد مصطلحات في حساب لامدا، والتي، عند تفسيرها بشكل مناسب، تتصرف مثل الرقم 3 ومثل عامل الضرب ، انظر ترميز تشيرش .

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

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

الحسابات التوافقية

بما أن التجريد هو السبيل الوحيد لإنشاء الدوال في حساب لامدا، فلا بد من وجود بديل له في حساب التوافيق. فبدلاً من التجريد، يوفر حساب التوافيق مجموعة محدودة من الدوال الأولية التي يمكن من خلالها بناء دوال أخرى.

المصطلحات التركيبية

يأخذ المصطلح التجميعي أحد الأشكال التالية:

بناء الجملةاسموصف
x{\displaystyle x}عاملحرف أو سلسلة تمثل مصطلحًا تركيبيًا.
P{\displaystyle P}الدالة الأوليةأحد رموز التجميعأنا{\displaystyle I}،ك{\displaystyle K}،S{\displaystyle S}.
(مشمال){\displaystyle (MN)}طلبتطبيق دالة على وسيط.م{\displaystyle M}وشمال{\displaystyle N}هي مصطلحات تركيبية.

الدوال الأولية هي دوال مركبة ، أو دوال لا تحتوي على متغيرات حرة عند النظر إليها كحدود لامدا .

ولتبسيط الرموز، فإن الاصطلاح العام هو أن(هـ1هـ2هـ3...هـن){\displaystyle (E_{1}E_{2}E_{3}...E_{n})}أو حتىهـ1هـ2هـ3...هـن{\displaystyle E_{1}E_{2}E_{3}...E_{n}}يشير إلى المصطلح(...((هـ1هـ2)هـ3)...هـن){\displaystyle (...((E_{1}E_{2})E_{3})...E_{n})}هذا هو نفس الاصطلاح العام (التجميع من اليسار) كما هو الحال بالنسبة للتطبيق المتعدد في حساب التفاضل والتكامل لامدا.

انخفاض في المنطق التوافقي

في المنطق التوافقي، يأتي كل مُركِّب أولي مع قاعدة اختزال على النحو التالي:

(P x1...xن)=هـ{\displaystyle (P\ x_{1}\dots x_{n})=E}

أينهـ{\displaystyle E}هو مصطلح يشير فقط إلى المتغيرات من المجموعة{x1...xن}{\displaystyle \{x_{1}\dots x_{n}\}}وبهذه الطريقة تتصرف المجموعات الأولية كدوال.

أمثلة على المجموعات

أبسط مثال على المُركِّب هوأنا{\displaystyle I}، مُركِّب الهوية، المُعرَّف بواسطة

(أنا x)=x{\displaystyle (I\ x)=x}

لجميع الشروطx{\displaystyle x}. مُركِّب بسيط آخر هوك{\displaystyle K}، والتي تُنتج وظائف ثابتة:(كx){\displaystyle (Kx)}هي الدالة التي تُرجع قيمةً لأي وسيط.x{\displaystyle x}لذلك نقول

((ك x) y)=x{\displaystyle ((K\ x)\ y)=x}

لجميع الشروطx{\displaystyle x}وy{\displaystyle y}أو، باتباع الاصطلاح المتبع في التطبيقات المتعددة،

(ك x y)=x{\displaystyle (K\ x\ y)=x}

المُركِّب الثالث هوS{\displaystyle S}، وهو نسخة معممة من التطبيق:

(S x y z)=(x z (y z)){\displaystyle (S\ x\ y\ z)=(x\ z\ (y\ z))}

S{\displaystyle S}ينطبقx{\displaystyle x}لy{\displaystyle y}بعد الاستبدال أولاًz{\displaystyle z}في كل واحد منهم. أو بعبارة أخرى،x{\displaystyle x}ينطبق علىy{\displaystyle y}داخل البيئةz{\displaystyle z}.

منحS{\displaystyle S}وك{\displaystyle K}،أنا{\displaystyle I}هي نفسها غير ضرورية، إذ يمكن بناؤها من الاثنين الآخرين:

((Sكك)x){\displaystyle ((S\,K\,K)\,x)}
=(Sكك)x{\displaystyle =(S\,K\,K)\,x}
=كx(كx){\displaystyle =K\,x\,(K\,x)}
=x{\displaystyle =x}

لأي مدةx{\displaystyle x}لاحظ أنه على الرغم من((Sكك)x)=(أناx){\displaystyle ((S\,K\,K)\,x)=(Ix)}لأيx{\displaystyle x}،(Sكك){\displaystyle (S\,K\,K)} لا يساوي نفسهأنا{\displaystyle I}نقول إن الحدود متساوية امتدادياً . تجسد المساواة الامتدادية المفهوم الرياضي لمساواة الدوال: أي أن دالتين تُعتبران متساويتين إذا أنتجتا دائماً نفس النتائج لنفس الوسائط. في المقابل، فإن الحدود نفسها، إلى جانب اختزال المُركِّبات الأولية، تُجسد مفهوم المساواة القصدية للدوال: أي أن دالتين تُعتبران متساويتين فقط إذا كان لهما تطبيقات متطابقة حتى توسيع المُركِّبات الأولية. هناك طرق عديدة لتطبيق دالة التطابق .(Sكك){\displaystyle (S\,K\,K)}وأنا{\displaystyle I}وتُعد هذه من بين هذه الطرق.(SكS){\displaystyle (S\,K\,S)}وهذا مثال آخر. سنستخدم كلمة "مكافئ" بمعنى المساواة الامتدادية.

المُركِّب الأكثر إثارة للاهتمام هو مُركِّب النقطة الثابتة أوY{\displaystyle Y}المُركِّب، الذي يمكن استخدامه لتنفيذ الاستدعاء الذاتي .

اكتمال قاعدة بيانات SK

يمكن تركيب S و K لإنتاج مُركِّبات تُساوي، من حيث الامتداد، أي حد لامدا، وبالتالي، وفقًا لأطروحة تشرش، أي دالة قابلة للحساب . ويتمثل البرهان في تقديم تحويل، T [  ] ، يُحوِّل أي حد لامدا إلى مُركِّب مُكافئ.

 يمكن تعريف T [ ] على النحو التالي:

  1. T [ x ] ⇒ x
  2. T [( E 1 E 2 )] ⇒ ( T [ E 1 ] T [ E 2 ])
  3. T [ λx . E ] ⇒ ( K T [ E ]) (إذالم يظهر x بشكل حر في E )
  4. T [ λx . x ] ⇒ I
  5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (إذا كان x يظهر حراً في E )
  6. T [ λx .( E 1 E 2 )] ⇒ ( S T [ λx . E 1 ] T [ λx . E 2 ]) (إذا كان x يظهر بشكل حر في E 1 أو E 2 )

لاحظ أن T [  ] كما هو معطى ليس دالة رياضية جيدة النوع، بل هو بالأحرى إعادة كتابة المصطلح: على الرغم من أنه ينتج في النهاية مُركبًا، إلا أن التحويل قد يولد تعبيرات وسيطة ليست مصطلحات لامدا ولا مُركبات، عبر القاعدة (5).

تُعرف هذه العملية أيضًا باسم إزالة التجريد . هذا التعريف شامل: أي تعبير لامدا سيخضع لواحدة فقط من هذه القواعد (انظر ملخص حساب لامدا أعلاه).

يرتبط هذا بعملية تجريد الأقواس ، التي تأخذ تعبيرًا E مبنيًا من متغيرات وتطبيق، وتُنتج تعبيرًا تركيبيًا [x]E حيث يكون المتغير x غير حر، بحيث يتحقق الشرط [ x ] E x = E. تُعرَّف خوارزمية بسيطة جدًا لتجريد الأقواس بالاستقراء على بنية التعبيرات كما يلي: [ 6 ]

  1. [ x ] y  := K y
  2. [ x ] x  := I
  3. [ س ]( E 1 E 2 )  := S ([ x ] E 1 )([ x ] E 2 )

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

تحويل مصطلح لامدا إلى مصطلح توافقي مكافئ

على سبيل المثال، سنقوم بتحويل الحد لامدا λx . λy .( y x ) إلى حد توافقي:

T [ λx . λy .( y x )]
= T [ λx . T [ λy .( y x ) ]] (بضرب 5)
= T [ λx .( S T [ λy . y ] T [ λy . x ])] (بواسطة 6)
= T [ λx .( SI T [ λy . x ])] (بضرب 4)
= T [ λx .( SI ( K T [ x ]))] (بمضاعفة 3)
= T [ λx .( SI ( K x ))] (بمقدار 1)
= ( S T [ λx .( SI )] T [ λx .( K x )]) (بواسطة 6)
= ( S ( K ( SI )) T [ λx .( K x )]) (بواسطة 3)
= ( S ( K ( SI )) ( S T [ λx . K ] T [ λx . x ])) (بواسطة 6)
= ( S ( K ( SI )) ( S ( KK ) T [ λx . x ])) (بواسطة 3)
= ( S ( K ( SI )) ( S ( KK ) I )) (بواسطة 4)

إذا طبقنا هذا الحد التوافقي على أي حدين x و y (عن طريق إدخالهما بطريقة تشبه قائمة الانتظار في المُركِّب "من اليمين")، فإنه يختزل على النحو التالي:

( S ( K ( S I )) ( S ( K K ) I ) xy)
= ( K ( S I ) x ( S ( K K ) I x) y)
= ( S I ( S ( K K ) I x) y)
= ( I y ( S ( K K ) I xy))
= (y ( S ( K K ) I xy))
= (y ( K K x ( I x) y))
= (y ( K ( I x) y))
= (y ( I x))
= (yx)

التمثيل التوافقي، ( S ( K ( SI ))( S ( KK ) I )) ، أطول بكثير من التمثيل كمصطلح لامدا، λx.λy. ( yx). وهذا أمر شائع. بشكل عام، يمكن لبنية T [ ] توسيع مصطلح لامدا بطول n إلى مصطلح توافقي بطول Θ ( n³ ). [ 7 ] 

شرح تحويل T [  ]

إن تحويل T [  ] مدفوع برغبة في إزالة التجريد. هناك حالتان خاصتان، وهما القاعدتان 3 و4، بديهيتان: λx.x مكافئ بوضوح لـ I ، و λx.E مكافئ بوضوح لـ ( KT [ E ] ) إذا لم يظهر x حراً في E.

القاعدتان الأوليان بسيطتان أيضًا: المتغيرات تتحول إلى نفسها، والتطبيقات، المسموح بها من الناحية التوافقية، يتم تحويلها إلى مُركِّبات ببساطة عن طريق تحويل المُطبَّق والوسيط إلى مُركِّبات.

القاعدتان 5 و6 هما المهمتان. تنص القاعدة 5 ببساطة على أنه لتحويل تجريد معقد إلى مُركِّب، يجب أولاً تحويل جسمه إلى مُركِّب، ثم حذف التجريد. أما القاعدة 6 فتحذف التجريد فعلياً.

الدالة λx .( E 1 E 2 ) تأخذ وسيطًا، ولنقل a ، وتستبدله في الحد لامدا ( E 1 E 2 ) بدلًا من x ، مما ينتج عنه ( E 1 E 2 )[ x  : = a ]. لكن استبدال a في ( E 1 E 2 ) بدلًا من x هو نفسه استبداله في كل من E 1 و E 2 ، لذا

( ه 1 ه 2 )[ س  := أ ] = ( ه 1 [ س  := أ ] ه 2 [ س  := أ ])
( lectx .( E 1 E 2 ) a ) = (( lectx . E 1 a ) ( lectx . E 2 a ))
= ( S λx . E 1 λx . E 2 a )
= (( S λx . E 1 λx . E 2 ) a )

بالمساواة الامتدادية،

lectx .( E 1 E 2 ) = ( S lectx . E 1 lectr . E 2 )

لذلك، لإيجاد مُركِّب مُكافئ لـ λx .( E 1 E 2 )، يكفي إيجاد مُركِّب مُكافئ لـ ( S λx . E 1 λx . E 2 )، و

( ST [ λx . E 1 ] T [ λx . E 2 ] )

من الواضح أن هذا يفي بالغرض. يحتوي كل من E1 وE2 على عدد أقل من التطبيقات مقارنةً بـ (E1 E2 ) ، لذا يجب أن ينتهي الاستدعاء الذاتي بحد لامدا بدون أي تطبيقات على الإطلاق - إما متغير، أو حد من الشكل λx.E.

تبسيطات التحويل

اختزال إيتا

يمكن تصغير المجموعات الناتجة عن تحويل T [ ] إذا أخذنا في الاعتبار قاعدة الاختزال η : 

T [ λx .( E x )] = T [ E ] (إذا لم يكن x حراً في E )

الدالة λx .( E x) هي الدالة التي تأخذ وسيطًا، x ، وتطبق عليه الدالة E ؛ وهي تساوي الدالة E نفسها من حيث الامتداد. لذلك، يكفي تحويل E إلى صيغة توافقية.

مع الأخذ في الاعتبار هذا التبسيط، يصبح المثال أعلاه كالتالي:

  T [ λx . λy .( y x )]
= ...
= ( S ( K ( SI )) T [ λx .( K x )])
= ( S ( K ( SI )) K ) (عن طريق اختزال η)

هذا المركب مكافئ للمركب السابق الأطول:

  ( S ( K ( SI )) K x y )
= ( K ( SI ) x ( K x ) y )
= ( SI ( K x ) y )
= ( I y ( K x y ))
= ( y ( K x y ))
= ( yx )

وبالمثل، حوّلت النسخة الأصلية من تحويل T [  ] دالة التطابق λf . λx .( f x ) إلى ( S ( S ( KS ) ( S ( KK ) I )) ( KI )). وباستخدام قاعدة اختزال η، يتم تحويل λf . λx .( f x ) إلى I .

أساس نقطة واحدة

توجد قواعد أحادية النقطة يمكن من خلالها تكوين أي مُركِّب بشكل ممتد يُساوي أي حد لامدا. مثال بسيط على هذه القاعدة هو { X } حيث:

X ≡ λx .((x S ) K )

ليس من الصعب التحقق من ذلك:

X ( X ( X X )) = β K و
X ( X ( X ( X X ))) = β S .

بما أن { K , S } أساس، فإن { X } أساس أيضًا. تستخدم لغة برمجة Iota العنصر X كعنصرها التجميعي الوحيد.

مثال بسيط آخر على أساس النقطة الواحدة هو:

X' ≡ λx .(x K S K ) مع
( X' X' ) X' = β K و
X' ( X' X' ) = β S

أبسط أساس معروف بنقطة واحدة هو تعديل طفيف لـ S :

S' ≡ λxλyλz . (xz) (y (λw. z))) مع
S' ( S' S' ) ( S' ( S' S' ) S' S' S' S' S' ) = β K و
S' ( S' ( S' S ' ( S' S' ( S' S' ))( S' ( S' ( S' S' ( S' S' )))))) S' S' = β S .

في الواقع، توجد قواعد لا حصر لها من هذا القبيل. [ 8 ]

المُركِّبات B، C

بالإضافة إلى S و K ، قام شونفينكل (1924) بتضمين اثنين من المجموعات التي تسمى الآن B و C ، مع الاختزالات التالية:

( C f g x ) = (( f x ) g )
( B f g x ) = ( f ( g x ))

ويشرح أيضاً كيف يمكن التعبير عنهما باستخدام S و K فقط :

ب = ( س ( ك س ) ك )
C = ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

تُعدّ هذه المُركِّبات مفيدة للغاية عند ترجمة منطق المسندات أو حساب لامدا إلى تعابير مُركِّبة. وقد استخدمها كاري أيضًا ، ولاحقًا ديفيد تيرنر ، الذي ارتبط اسمه باستخدامها الحسابي. وباستخدامها، يُمكننا توسيع قواعد التحويل على النحو التالي:

  1. T [ x ] ⇒ x
  2. T [( E 1 E 2 )] ⇒ ( T [ E 1 ] T [ E 2 ])
  3. T [ λx . E ] ⇒ ( K T [ E ]) (إذالم يكن x حراً في E )
  4. T [ λx . x ] ⇒ I
  5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (إذا كان x حرًا في E )
  6. T [ λx .( E 1 E 2 )] ⇒ ( S T [ λx . E 1 ] T [ λx . E 2 ]) (إذا كان x حراً في كل من E 1 و E 2 )
  7. T [ λx .( E 1 E 2 )] ⇒ ( C T [ λx . E 1 ] T [ E 2 ]) (إذا كان x حرًا في E 1 ولكن ليس في E 2 )
  8. T [ λx .( E 1 E 2 )] ⇒ ( B T [ E 1 ] T [ λx . E 2 ]) (إذا كان x حرًا في E 2 ولكن ليس في E 1 )

باستخدام مُركِّبات B و C ، يبدو تحويل λx . λy .( y x ) على النحو التالي:

  T [ λx . λy .( y x )]
= T [ λx . T [ λy .( y x )]]
= T [ λx .( C T [ λy . y ] x )] (بحسب القاعدة 7)
= T [ λx .( C I x )]
= ( C I ) (اختزال إيتا)
=ج*{\displaystyle ={\mathsf {C}}_{*}}(التدوين الكنسي التقليدي:X*=Xأنا{\displaystyle {\mathsf {X}}_{*}={\mathsf {XI}}})
=أنا′{\displaystyle ={\mathsf {I}}'}(التدوين الكنسي التقليدي:X′=جX{\displaystyle {\mathsf {X}}'={\mathsf {CX}}})

وبالفعل، فإن ( C I x y ) يختزل إلى ( y x ):

  ( C I x y )
= ( I y x )
= ( y x )

يكمن الدافع هنا في أن B و C هما نسختان محدودتان من S ، حيث B x y = S ( K x ) y و C x y = S x ( K y ). بينما تأخذ S x yz = ( xz ) ( yz ) قيمة ( z ) وتستبدلها في كل من المُطبَّق ( x ) ووسيطه ( y ) قبل تنفيذ التطبيق، فإن C تُجري الاستبدال فقط في المُطبَّق (( xz ) y )، و B فقط في الوسيط ( x ( yz )).

تعود الأسماء الحديثة للمُركِّبات إلى أطروحة الدكتوراه التي قدمها هاسكل كاري عام 1930 (انظر نظام B، C، K، W ). في ورقة شونفينكل الأصلية، ما نسميه الآن S و K و I و B و C كان يُسمى S و C و I و Z و T على التوالي.

ويمكن أيضًا تحقيق تقليل حجم التجميع الناتج عن قواعد التحويل الجديدة دون إدخال B و C ، كما هو موضح في القسم 3.2 من Tromp (2008) .

حساب الفرق بين CL K و CL I

يجب التمييز بين حساب التفاضل والتكامل CL K كما هو موضح في هذه المقالة وحساب التفاضل والتكامل CL I. ويتطابق هذا التمييز مع التمييز بين حساب التفاضل والتكامل λ K وحساب التفاضل والتكامل λ I. فعلى عكس حساب التفاضل والتكامل λ K ، يقتصر حساب التفاضل والتكامل λ I على التجريدات التالية:

λx . E حيث x له ظهور حر واحد على الأقل في E .

نتيجةً لذلك، لا يوجد المُركِّب K في حساب λ I ولا في حساب CL I. ثوابت CL I هي: I و B و C و S ، والتي تُشكِّل أساسًا يُمكن من خلاله تكوين جميع حدود CL I (مع مراعاة المساواة). يُمكن تحويل كل حد من حدود λ I إلى مُركِّب CL I مُساوٍ له في الامتداد، وذلك وفقًا لقواعد مُشابهة لتلك المُوضَّحة أعلاه لتحويل حدود λ K إلى مُركِّبات CL K. انظر الفصل 9 في كتاب باريندريخت (1984).

يُعرّف تشرش (1941) (الفقرة 12) مُركّبين أدنى لحساب λ I : I = λ a . a و J = λ abcd . ab ( adc ). كما يقترح مجموعات أولية بديلة من المُركّبات، B و C و W و I (حيث W = λ ab . abb هو نفسه المستخدم اليوم)، أو B و T و U و I (حيث T = JII = λ ab . ba = CI و U = λ a . aa = WI والذي يُسمّيه D ).

التحويل العكسي

إن تحويل L [  ] من الحدود التوافقية إلى حدود لامدا أمر تافه:

L [ I ] = λx . x
L [ K ] = λx . λy . x
L [ C ] = λx . λy . λz .( x z y )
L [ B ] = λx . λy . λz .( x ( y z ))
L [ S ] = λx . λy . λz .( x z ( y z ))
ل [( ه 1 ه 2 )] = ( ل [ ه 1 ] ل [ ه 2 ])

لاحظ مع ذلك أن هذا التحويل ليس التحويل العكسي لأي من إصدارات T [  ] التي رأيناها.

عدم قابلية الحسم في حساب التفاضل والتكامل التوافقي

الصيغة الطبيعية هي أي حد تركيبي لا تُطبَّق فيه المُركِّبات الأولية، إن وُجدت، على عدد كافٍ من الوسائط لتبسيطها. من غير الممكن تحديد ما إذا كان للحد التركيبي العام صيغة طبيعية، أو ما إذا كان حدان تركيبيان متكافئين، وما إلى ذلك. ويمكن إثبات ذلك بطريقة مشابهة للمسائل المقابلة لحدود لامدا.

عدم إمكانية التعريف بواسطة المسندات

تأخذ المسائل غير القابلة للحسم المذكورة أعلاه (التكافؤ، وجود الصيغة الطبيعية، إلخ) تمثيلات نحوية للمصطلحات كمدخلات ضمن ترميز مناسب (مثل ترميز تشيرش ). يمكن أيضًا النظر في نموذج حسابي بسيط حيث "نحسب" خصائص المصطلحات باستخدام مُركِّبات تُطبَّق مباشرةً على المصطلحات نفسها كوسائط، بدلاً من تمثيلاتها النحوية. بتعبير أدق، ليكن المسند مُركِّبًا ، عند تطبيقه، يُعيد إما T أو F ( حيث يُمثل T و F ترميزات تشيرش التقليدية للصواب والخطأ ، λx.λy.x و λx.λy.y ، مُحوَّلة إلى منطق توافقي؛ النسخ التوافقية لها T = K و F = ( K I ) ) . يكون المسند N غير تافه إذا كان هناك وسيطان A و B بحيث يكون NA = T و NB = F. يكون المُركِّب N كاملاً إذا كان لـ NA صيغة طبيعية لكل وسيط M. ينص نظير نظرية رايس لهذا النموذج البسيط على أن كل محمول كامل هو تافه. وبرهان هذه النظرية بسيط للغاية. [ 9 ]

دليل

بالبرهان بالخلف. لنفترض وجود محمول كامل غير تافه، ولنسمه N. ولأن N يفترض أن يكون غير تافه، فهناك مُركِّبان A و B بحيث

( NA ) = T و
( NB ) = F.​
عرّف النفي على النحو التالي: ≡ λx .(if ( N x ) then B else A ) ≡ λx .(( N x ) B A )
تعريف السخافة ≡ ( Y NEGATION)

تنص نظرية النقطة الثابتة على أن: العبث = (العبث النفي)، لـ

السبيل ≡ ( نفي Y ) = ( النفي ( نفي Y )) ≡ ( نفي السخافة).

لأن N يفترض أن تكون كاملة إما:

  1. ( مغالطة منطقية) = خطأ أو
  2. ( مغالطة N ) = T
  • الحالة 1: F = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N A ) = T ، تناقض.
  • الحالة 2: T = ( N عبثية) = N ( عبثية النفي) = ( N B ) = F ، وهو تناقض مرة أخرى.

وبالتالي، فإن ( N عبثية) ليست صحيحة ولا خاطئة ، مما يناقض الافتراض المسبق بأن N ستكون محمولًا كاملًا غير تافه. وهو المطلوب إثباته.

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

(تساوي AB ) = T إذا كان A = B و
(EQUAL AB ) = F إذا كان A ≠ B .

إذا كان EQUAL موجودًا، فإنه بالنسبة لجميع A ، λx. (EQUAL x A ) يجب أن يكون مسندًا كاملاً غير تافه.

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

التطبيقات

تجميع اللغات الوظيفية

استخدم ديفيد تيرنر أجهزة التجميع الخاصة به لتنفيذ لغة برمجة SASL .

استخدم كينيث إي. إيفرسون عناصر أساسية مبنية على مُركِّبات كاري في لغة البرمجة J ، التي خلفت لغة APL . وقد مكّن هذا من ما أسماه إيفرسون البرمجة الضمنية ، أي البرمجة باستخدام تعابير وظيفية لا تحتوي على متغيرات، إلى جانب أدوات قوية للتعامل مع هذه البرامج. واتضح أن البرمجة الضمنية ممكنة في أي لغة شبيهة بلغة APL تحتوي على عوامل تشغيل مُعرَّفة من قِبل المستخدم. [ 10 ]

منطق

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

تتوافق المجموعات K و S مع البديهيات

AK : A → ( B → A ),
AS : ( A → ( B → C )) → (( A → B ) → ( A → C )),

ويتوافق تطبيق الوظيفة مع قاعدة الفصل ( modus ponens ).

MP : من A و A → B استنتج B .

تُعتبر الحسابات المكونة من AK و AS و MP كاملةً بالنسبة للجزء الاستلزامي من المنطق الحدسي، والذي يمكن توضيحه على النحو التالي. لنفترض المجموعة W التي تضم جميع مجموعات الصيغ المغلقة استنتاجياً، مرتبةً حسب الاحتواء . عندئذٍ⟨دبليو،⊆⟩{\displaystyle \langle W,\subseteq \rangle }هو إطار كريپكي حدسي ، ونحن نُعرّف نموذجًا⊩{\displaystyle \Vdash }في هذا الإطار بواسطة

X⊩أ⟺أ∈X.{\displaystyle X\Vdash A\iff A\in X.}

هذا التعريف يفي بشروط تحقيق →: من جهة، إذاX⊩أ→ب{\displaystyle X\Vdash A\to B}، وY∈دبليو{\displaystyle Y\in W}بحيثY⊇X{\displaystyle Y\supseteq X}وY⊩أ{\displaystyle Y\Vdash A}، ثمY⊩ب{\displaystyle Y\Vdash B}عن طريق الاستدلال الاستدلالي. من ناحية أخرى، إذاX⊮أ→ب{\displaystyle X\not \Vdash A\to B}، ثمX،أ⊬ب{\displaystyle X,A\not \vdash B}وبناءً على نظرية الاستنتاج ، فإن الإغلاق الاستنتاجي لـX∪{أ}{\displaystyle X\cup \{A\}}هو عنصرY∈دبليو{\displaystyle Y\in W}بحيثY⊇X{\displaystyle Y\supseteq X}،Y⊩أ{\displaystyle Y\Vdash A}، وY⊮ب{\displaystyle Y\not \Vdash B}.

لتكن A أي صيغة غير قابلة للإثبات في حساب التفاضل والتكامل. عندئذٍ، لا تنتمي A إلى الإغلاق الاستنتاجي X للمجموعة الفارغة ، وبالتاليX⊮أ{\displaystyle X\not \Vdash A}، و A ليس صحيحًا من الناحية الحدسية.

انظر أيضاً

مراجع

الأدب