رفع لامدا

رفع لامدا هو عملية شاملة تُعيد هيكلة برنامج حاسوبي بحيث تُعرَّف الدوال بشكل مستقل عن بعضها البعض في نطاق عام. يحوّل الرفع الفردي دالة محلية (روتين فرعي) إلى دالة عامة. وهي عملية من خطوتين، تتكون من:

إزالة المتغيرات الحرة في الدالة عن طريق إضافة المعاملات .
نقل الوظائف من نطاق محدود إلى نطاق أوسع أو عالمي.

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

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

يمكن استخدام هذه التقنية على الدوال الفردية، في إعادة هيكلة الشيفرة ، لجعل الدالة قابلة للاستخدام خارج نطاقها الأصلي. كما يمكن تكرار عمليات رفع لامدا لتحويل البرنامج. ويمكن استخدام عمليات الرفع المتكررة لتحويل برنامج مكتوب بلغة لامدا إلى مجموعة من الدوال التكرارية ، دون استخدام لامدا. وهذا يُظهر تكافؤ البرامج المكتوبة بلغة لامدا والبرامج المكتوبة كدوال. ^{[ 1 ]} ومع ذلك، لا يُظهر هذا سلامة استخدام لامدا للاستدلال، لأن اختزال إيتا المستخدم في رفع لامدا هو الخطوة التي تُدخل مشاكل في عدد عناصر لامدا، لأنه يُزيل القيمة من المتغير، دون التحقق أولاً من وجود قيمة واحدة فقط تُحقق شروط المتغير (انظر مفارقة كاري ).

يُعدّ رفع تعبيرات لامدا مكلفًا من حيث وقت المعالجة بالنسبة للمترجم. ويتمثل التنفيذ الفعال لرفع تعبيرات لامدا فيما يلي: $O(n^{2})$ ^[²^] وقت المعالجة للمترجم.

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

العملية العكسية لرفع لامدا هي خفض لامدا . ^{[ 3 ]}

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

الخوارزمية

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

أعد تسمية الدوال بحيث يكون لكل دالة اسم فريد.
استبدل كل متغير حر بوسيطة إضافية للدالة المحيطة، وقم بتمرير تلك الوسيطة إلى كل استخدام للدالة.
استبدل كل تعريف دالة محلية لا تحتوي على متغيرات حرة بدالة عامة مطابقة.
كرر الخطوتين 2 و 3 حتى يتم التخلص من جميع المتغيرات الحرة والوظائف المحلية.

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

مثال

يقوم برنامج OCaml التالي بحساب مجموع الأعداد الصحيحة من 1 إلى 100:

ليكن مجموع n = إذا كان n = 1 فإن 1 وإلا فليكن f x = n + x في f ( مجموع ( n - 1 ) ) المجموع 100

( let recيُعرّف هذا sumكدالة يمكنها استدعاء نفسها). الدالة f، التي تجمع وسيط الدالة sum مع مجموع الأعداد الأقل من الوسيط، هي دالة محلية. ضمن تعريف f، n متغير حر. ابدأ بتحويل المتغير الحر إلى مُعامل:

ليكن مجموع n = إذا كان n = 1 فإن 1 وإلا فليكن f w x = w + x في f n ( مجموع ( n - 1 ) ) المجموع 100

بعد ذلك، قم بتحويل f إلى دالة عامة:

ليكن rec f w x = w + x و sum n = إذا كان n = 1 فإن 1 وإلا f n ( sum ( n - 1 )) in sum 100

فيما يلي نفس المثال، ولكن هذه المرة مكتوب بلغة جافا سكريبت :

// النسخة الأوليةدالة الجمع ( ن ) { دالة د ( س ) { إرجاع ن + س ؛ }إذا كان ( n == 1 ) فأرجع 1 ؛ وإلا فأرجع f ( sum ( n - 1 )); }// بعد تحويل المتغير الحر n إلى معامل رسمي wدالة الجمع ( ن ) { دالة f ( و ، س ) { إرجاع و + س ؛ }إذا كان ( n == 1 ) فأرجع 1 ؛ وإلا فأرجع f ( n , sum ( n - 1 )); }// بعد رفع الدالة f إلى النطاق العامدالة f ( w , x ) { إرجاع w + x ; }دالة المجموع ( ن ) { إذا كان ( ن == 1 ) أرجع 1 ؛ وإلا أرجع f ( ن ، مجموع ( ن - 1 )); }

رفع لامدا مقابل إغلاقها

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

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

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

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

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

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

إن تعبير let المستخدم هنا هو نسخة متبادلة التكرار بالكامل من let rec ، كما هو مطبق في العديد من اللغات الوظيفية.

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

ترد قواعد التحويل التي تصف الترجمة بدون رفع في مقالة تعبير Let .

توضح القواعد التالية تكافؤ تعبيرات لامدا وليت،

اسم	قانون
تكافؤ اختزال إيتا	$f\ x=y\equiv f=\lambda x.y$
تكافؤ ليت-لامدا	$f\notin FV(E)\to (\operatorname {let} f:f=E\operatorname {in} L\equiv (\lambda f.L)\ E)\ {\text{(where }}f{\text{ is a variable name.)}}$
مجموعة لي	$x\notin FV(E)\to (\operatorname {let} v,\dots ,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,\dots ,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)$

سيتم تقديم دوال وصفية تصف رفع وخفض قيم لامدا. الدالة الوصفية هي دالة تأخذ برنامجًا كمعامل. يمثل البرنامج بيانات للبرنامج الوصفي. يقع البرنامج والبرنامج الوصفي على مستويين وصفيين مختلفين.

سيتم استخدام الاصطلاحات التالية للتمييز بين البرنامج والبرنامج الفوقي،

سيتم استخدام الأقواس المربعة [] لتمثيل تطبيق الدالة في البرنامج الفوقي.
سيتم استخدام الأحرف الكبيرة للمتغيرات في البرنامج الوصفي. أما الأحرف الصغيرة فتمثل المتغيرات في البرنامج.
$\equiv$ سيتم استخدامها للمساواة في البرنامج الوصفي.
$\_$ يمثل متغيرًا وهميًا، أو قيمة غير معروفة.

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

يُستخدم عامل الاستبدال على نطاق واسع. التعبير $L[G:=S]$ يعني ذلك استبدال كل ظهور للحرف G في L بالحرف S وإرجاع التعبير. تم توسيع التعريف المستخدم ليشمل استبدال التعبيرات، انطلاقًا من التعريف الوارد في صفحة حساب لامدا . يجب أن تقارن عملية مطابقة التعبيرات التعبيرات للتأكد من تكافؤها (إعادة تسمية المتغيرات).

رفع لامدا في حساب لامدا

تستبدل كل عملية رفع لدالة لامدا تجريدًا لدالة لامدا، وهو تعبير فرعي من تعبير لامدا، باستدعاء دالة (تطبيق) لدالة تقوم بإنشائها. المتغيرات الحرة في التعبير الفرعي هي معاملات استدعاء الدالة.

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

مصعد لامدا

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

\operatorname {lambda-lift-op} [S,L,P]=P[L:=\operatorname {lambda-lift} [S,L]]

قد يكون التعبير الفرعي إما تجريدًا لـ lambda، أو تجريدًا لـ lambda مطبقًا على معلمة.

يوجد نوعان من المصاعد.

مصعد مجهول الهوية
مصعد يحمل اسمًا

يحتوي الرفع المجهول على تعبير رفع يمثل تجريدًا لدالة لامدا فقط. ويُعتبر بمثابة تعريف لدالة مجهولة . يجب تحديد اسم لهذه الدالة.

يُطبَّق تجريد لامدا على تعبير الرفع المُسمّى. ويُعتبر هذا الرفع تعريفًا مُسمّى لدالة.

مصعد مجهول الهوية

يستمد المصعد المجهول تجريدًا لامدا (يسمى S ). لـ S ؛

أنشئ اسمًا للدالة التي ستحل محل S (وتسمى V ). تأكد من عدم استخدام الاسم المحدد بواسطة V.
أضف معلمات إلى V ، لجميع المتغيرات الحرة في S ، لإنشاء تعبير G (انظر make-call ).

إن رفع لامدا هو استبدال تجريد لامدا S بتطبيق دالة، بالإضافة إلى إضافة تعريف للدالة.

\operatorname {lambda-lift} [S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[S:=G]

يحتوي التعبير الجديد لـ lambda على استبدال S بـ G: L [ S := G ] يعني استبدال S بـ G في L. تمت إضافة تعريف الدالة G = S إلى تعريفات الدوال .

في القاعدة المذكورة أعلاه ، G هي دالة التطبيق التي تحل محل التعبير S. ويتم تعريفها على النحو التالي:

G=\operatorname {make-call} [V,\operatorname {FV} [S]]

حيث V هو اسم الدالة. يجب أن يكون متغيرًا جديدًا، أي اسمًا لم يُستخدم من قبل في تعبير لامدا.

V\not \in \operatorname {vars} [\operatorname {let} F\operatorname {in} L]

أين $\operatorname {vars} [E]$ هي دالة وصفية تُرجع مجموعة المتغيرات المستخدمة في E.

مثال على المصعد المجهول.
على سبيل المثال، ${\begin{aligned}F&=\operatorname {true} \\L&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\S&=\lambda x.f\ (x\ x)\\G&=p\ f\end{aligned}}$ $\operatorname {de-lambda} [p\ f=\lambda x.f\ (x\ x)]\equiv p\ f\ x=f\ (x\ x)$ انظر إلى de-lambda في قسم التحويل من تعبيرات lambda إلى تعبيرات let . والنتيجة هي: $\operatorname {lambda-lift} [\lambda x.f\ (x\ x),\operatorname {let} \operatorname {true} \operatorname {in} \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\equiv \operatorname {let} p\ f\ x=f\ (x\ x)\operatorname {in} \lambda f.(p\ f)\ (p\ f)$

إنشاء المكالمة

يتم إنشاء استدعاء الدالة G عن طريق إضافة معلمات لكل متغير في مجموعة المتغيرات الحرة (الممثلة بـ V ) إلى الدالة H.

$X\in V\to \operatorname {make-call} [H,V]\equiv \operatorname {make-call} [H,V\cap \neg \{X\}]\ X$
$\operatorname {make-call} [H,\{\}]\equiv H$

مثال على بناء الاستدعاء.
$S=\lambda x.f\ (x\ x)$ $\operatorname {FV} (S)=\{f\}$ $G\equiv \operatorname {make-call} [p,\operatorname {FV} [S]]\equiv \operatorname {make-call} [p,\{f\}]\equiv \operatorname {make-call} [p,\{\}]\ f\equiv p\ f$

مصعد يحمل اسمًا

المصعد المسمى يشبه المصعد المجهول باستثناء أنه يتم توفير اسم الوظيفة V.

\operatorname {lambda-lift} [(\lambda V.E)\ S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[(\lambda V.E)\ S:=E[V:=G]]

أما بالنسبة للرفع المجهول، فإن التعبير G يُشتق من V بتطبيق المتغيرات الحرة لـ S. ويُعرَّف على النحو التالي:

G=\operatorname {make-call} [V,\operatorname {FV} [S]]

مثال على مصعد مُسمى.
على سبيل المثال، ${\begin{aligned}V&=x\\E&=f\ (x\ x)\\S&=(\lambda x.f\ (x\ x))\\L&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\G&=x\ f\end{aligned}}$ $E[V:=G]=f\ (x\ x)[x:=x\ f]=f\ ((x\ f)\ (x\ f))$ $L[(\lambda V.E)\ F:=E[V:=G]]=L[(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)):=f\ ((x\ f)\ (x\ f))]=\lambda f.f\ ((x\ f)\ (x\ f))$ $\operatorname {de-lambda} [x\ f=\lambda y.f\ (y\ y)]\equiv x\ f\ y=f\ (y\ y)$ انظر إلى de-lambda في قسم التحويل من تعبيرات lambda إلى تعبيرات let . والنتيجة هي: يعطي، $\operatorname {lambda-lift} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)),\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\equiv \operatorname {let} x\ f\ y=f\ (y\ y)\operatorname {in} \lambda f.(x\ f)\ (x\ f)$

تحويل لامدا-ليفت

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

$\operatorname {let} M\operatorname {in} N$

حيث M عبارة عن سلسلة من تعريفات الدوال، و N هو التعبير الذي يمثل القيمة التي يتم إرجاعها.

على سبيل المثال،

\operatorname {lambda-lift-tran} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\equiv \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p

يمكن بعد ذلك استخدام دالة de-let meta لتحويل النتيجة مرة أخرى إلى حساب لامدا.

\operatorname {de-let} [\operatorname {lambda-lift-tran} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]]\equiv (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)

تتضمن عملية تحويل تعبير لامدا سلسلة من عمليات الرفع. كل عملية رفع تتضمن،

يتم اختيار تعبير فرعي بواسطة الدالة lift-choice . يجب اختيار التعبير الفرعي بحيث يمكن تحويله إلى معادلة بدون تعابير لامدا.
يتم تنفيذ عملية الرفع عن طريق استدعاء الدالة الوصفية lambda-lift ، الموضحة في القسم التالي.

{\begin{cases}\operatorname {lambda-lift-tran} [L]=\operatorname {drop-params-tran} [\operatorname {merge-let} [\operatorname {lambda-apply} [L]]]\\\operatorname {lambda-apply} [L]=\operatorname {lambda-process} [\operatorname {lift-choice} [L],L]\\\operatorname {lambda-process} [\operatorname {none} ,L]=L\\\operatorname {lambda-process} [S,L]=\operatorname {lambda-apply} [\operatorname {lambda-lift} [S,L]]\end{cases}}

بعد تركيب المصاعد، يتم دمج الأجزاء معًا في جزء واحد.

{\begin{cases}\operatorname {merge-let} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]=\operatorname {merge-let} [\operatorname {let} V,W:E\land F\operatorname {in} G]\\\operatorname {merge-let} [E]=E\end{cases}}

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

اختيار التعبير المناسب للرفع

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

هذان المسندان ضروريان لكلا التعريفين.

خالٍ من تعبيرات لامدا - تعبير لا يحتوي على أي تجريدات لامدا.

{\begin{cases}\operatorname {lambda-free} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-free} [V]=\operatorname {true} \\\operatorname {lambda-free} [M\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-free} [N]\end{cases}}

lambda-anon - دالة مجهولة. تعبير مثل $\lambda x_{1}.\ ...\ \lambda x_{n}.X$ حيث X خالية من لامدا.

{\begin{cases}\operatorname {lambda-anon} [\lambda F.X]=\operatorname {lambda-free} [X]\lor \operatorname {lambda-anon} [X]\\\operatorname {lambda-anon} [V]=\operatorname {false} \\\operatorname {lambda-anon} [M\ N]=\operatorname {false} \end{cases}}

اختيار الوظائف المجهولة فقط لأغراض الرفع

ابحث عن أعمق تجريد مجهول، بحيث يصبح عند تطبيق الرفع، الدالة المرفوعة معادلة بسيطة. لا يعتبر هذا التعريف تجريدات لامدا ذات المعامل تعريفًا لدالة. تُعتبر جميع تجريدات لامدا تعريفًا لدوال مجهولة.

lift-choice - أول مجهول يتم العثور عليه أثناء اجتياز التعبير أو لا شيء إذا لم تكن هناك دالة.

$\operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X$
$\operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]$
$\operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]$
$\operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]$
$\operatorname {lift-choice} [V]=\operatorname {none}$

على سبيل المثال،

اختيار لامدا $\lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))$ يكون $\lambda x.f\ (x\ x)$
قاعدة	نوع الوظيفة	خيار
2		$\operatorname {lift-choice} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))]$
3		$\operatorname {lift-choice} [(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))]$
1	حالا	$\operatorname {lift-choice} [\lambda x.f\ (x\ x)]$
		$\lambda x.f\ (x\ x)$

اختيار لامدا $\lambda f.(p\ f)\ (p\ f)$ يكون $\lambda f.(p\ f)\ (p\ f)$
قاعدة	نوع الوظيفة	خيار
2	حالا	$\operatorname {lift-choice} [\lambda f.(p\ f)\ (p\ f)]$
2		$\lambda f.(p\ f)\ (p\ f)$

اختيار الدوال المسماة والمجهولة لرفع البيانات

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

لامدا-الاسم

دالة مُسماة. تعبير مثل

(\lambda F.M)\ N

حيث M خالية من تعبيرات لامدا و N خالية من تعبيرات لامدا أو دالة مجهولة.

{\begin{array}{l}\operatorname {lambda-named} [(\lambda F.M)\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-anon} [N]\\\operatorname {lambda-named} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-named} [V]=\operatorname {false} \end{array}}

اختيار المصعد

أول دالة مجهولة أو مسماة يتم العثور عليها أثناء اجتياز التعبير، أو لا شيء إذا لم تكن هناك دالة.

$\operatorname {lambda-named} [X]\lor \operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X$
$\operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]$
$\operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]$
$\operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]$
$\operatorname {lift-choice} [V]=\operatorname {none}$

على سبيل المثال،

اختيار لامدا $\lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))$ يكون $(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))$
قاعدة	نوع الوظيفة	خيار
2		$\operatorname {lift-choice} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))]$
1	اسم	$\operatorname {lift-choice} [(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))]$
		$(\lambda x.f\ (x\ x))\ (\lambda y.f\ (y\ y))$

اختيار لامدا $\lambda f.f\ ((x\ f)\ (x\ f))$ يكون $\lambda f.f\ ((x\ f)\ (x\ f))$
قاعدة	نوع الوظيفة	خيار
1	حالا	$\operatorname {lift-choice} [\lambda f.f\ ((x\ f)\ (x\ f))]$
		$\lambda f.f\ ((x\ f)\ (x\ f))$

أمثلة

على سبيل المثال، مُركِّب Y ،

\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))

تم رفعه على النحو التالي:

\operatorname {let} x\ f\ y=f\ (y\ y)\land q\ x\ f=f\ ((x\ f)\ (x\ f))\operatorname {in} q\ x

وبعد حذف المعلمة ،

\operatorname {let} x\ f\ y=f\ (y\ y)\land q\ f=f\ ((x\ f)\ (x\ f))\operatorname {in} q

كتعبير لامدا (انظر التحويل من تعبيرات let إلى تعبيرات لامدا )،

(\lambda x.(\lambda q.q)\ \lambda f.f\ (x\ f)\ (x\ f))\ \lambda f.\lambda y.f\ (y\ y)

رفع الوظائف المسماة والمجهولة
	تعبير لامدا	وظيفة	من	ل	المتغيرات
1	$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$	حقيقي	$(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$	$x\ f$	$\{x,f\}$
2	$(\lambda f.(\lambda x.f\ (x\ x))(\lambda x.f\ (x\ x)))$ $[(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)):=f\ ((x\ f)\ (x\ f))]$	$x\ f=\lambda y.f\ (y\ y)$			$\{x,f,p\}$
3	$\lambda f.f\ ((x\ f)\ (x\ f))$	$x\ f\ y=f\ (y\ y)$	$\lambda f.f\ ((x\ f)\ (x\ f))$	$q\ x$	$\{x,f,p\}$
4	$\lambda f.f\ ((x\ f)\ (x\ f))[\lambda f.f\ ((x\ f)\ (x\ f)):=q\ x]$	$x\ f\ y=f\ (y\ y)\land q\ x=\lambda f.f\ ((x\ f)\ (x\ f))$			$\{x,f,p,q\}$
5	$q\ x$	$x\ f\ y=f\ (y\ y)\land q\ x\ f=f\ ((x\ f)\ (x\ f))$			$\{x,f,p,q\}$

إذا اقتصر الأمر على رفع الدوال المجهولة فقط، فإن مُركِّب Y هو،

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p

وبعد حذف المعلمة ،

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ f=(p\ f)\ (p\ f)\operatorname {in} q

كتعبير لامدا،

(\lambda p.(\lambda q.q)\ \lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)

رفع الوظائف المجهولة فقط
	تعبير لامدا	وظيفة	من	ل	المتغيرات
1	$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))$	حقيقي	$\lambda x.f\ (x\ x)$	$p\ f$	$\{x,f\}$
2	$(\lambda f.(\lambda x.f\ (x\ x))(\lambda x.f\ (x\ x)))[\lambda x.f\ (x\ x):=p\ f]$	$p\ f=\lambda x.f\ (x\ x)$			$\{x,f,p\}$
3	$\lambda f.(p\ f)\ (p\ f)$	$p\ f\ x=f\ (x\ x)$	$\lambda f.(p\ f)\ (p\ f)$	$q\ p$	$\{x,f,p\}$
4	$\lambda f.(p\ f)\ (p\ f)[\lambda f.(p\ f)\ (p\ f):=q\ p]$	$p\ f\ x=f\ (x\ x)\land q\ p=\lambda f.(p\ f)\ (p\ f)$			$\{x,f,p,q\}$
5	$q\ p$	$p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)$			$\{x,f,p,q\}$

أول تعبير فرعي يتم اختياره للرفع هو $\lambda x.f\ (x\ x)$ وهذا يحول تعبير لامدا إلى $\lambda f.(p\ f)\ (p\ f)$ وينشئ المعادلة $p\ f\ x=f(x\ x)$ .

التعبير الفرعي الثاني الذي سيتم اختياره للرفع هو $\lambda f.(p\ f)\ (p\ f)$ وهذا يحول تعبير لامدا إلى $q\ p$ وينشئ المعادلة $q\ p\ f=(p\ f)\ (p\ f)$ .

والنتيجة هي،

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\

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

تنفيذ

تطبيق الدالة على $K$ ،

{\begin{cases}\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\ K&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} \ q\ p\ K\\(\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} \ p\ K\ (p\ K)\\K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x)))&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=p\ f\ (p\ f)\ \operatorname {in} \ K\ (p\ K\ (p\ K))\\\end{cases}}

لذا،

(\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))=K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))))\

أو

p\ K\ (p\ K)=K\ (p\ K\ (p\ K))

يستدعي مُركِّب Y مُعامله (الدالة) بشكل متكرر على نفسه. تُحدَّد القيمة إذا كانت للدالة نقطة ثابتة . لكن الدالة لن تنتهي أبدًا.

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

يُقلل حذف تعبيرات لامدا ^{[ 4 ]} نطاق الدوال، ويستخدم السياق الناتج من النطاق المُصغّر لتقليل عدد المعاملات. ويُسهّل تقليل عدد المعاملات فهم الدوال.

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

يتم تنفيذ عملية إسقاط لامدا على مرحلتين،

غرق
إسقاط المعلمات

انخفاض لامدا

يتم تطبيق دالة حذف لامدا على تعبير ضمن برنامج. ويتم التحكم في عملية الحذف بواسطة مجموعة من التعبيرات التي سيتم استبعادها من عملية الحذف.

\operatorname {lambda-drop-op} [L,P,X]=P[L:=\operatorname {drop-params-tran} [\operatorname {sink-test} [L,X]]]

أين،

L هو التجريد اللامدا الذي سيتم حذفه.

P هو البرنامج

X عبارة عن مجموعة من التعبيرات التي يجب استبعادها من عملية الحذف.

تحول قطرة لامدا

يُخفي تحويل لامدا دروب جميع التجريدات في التعبير. ويُستثنى من ذلك التعبيرات الموجودة ضمن مجموعة من التعبيرات.

\operatorname {lambda-drop-tran} [L,X]=\operatorname {drop-params-tran} [\operatorname {sink-tran} [\operatorname {de-let} [L,X]]]

أين،

L هو التعبير المراد تحويله.

X عبارة عن مجموعة من التعبيرات الفرعية التي سيتم استبعادها من عملية الحذف.

يُغرق نظام sink-tran كل تجريد، بدءًا من الأعمق.

{\begin{cases}\operatorname {sink-tran} [(\lambda N.B)\ Y,X]=\operatorname {sink-test} [(\lambda N.\operatorname {sink-tran} [B])\ \operatorname {sink-tran} [Y],X]\\\operatorname {sink-tran} [\lambda N.B,X]=\lambda N.\operatorname {sink-tran} [B,X]\\\operatorname {sink-tran} [M\ N,X]=\operatorname {sink-tran} [M,X]\ \operatorname {sink-tran} [M,X]\\\operatorname {sink-tran} [V,X]=V\end{cases}}

غرق التجريد

الغرق هو نقل تجريد لامدا إلى الداخل قدر الإمكان بحيث يظل خارج جميع المراجع إلى المتغير.

التطبيق - 4 حالات.

{\begin{cases}E\not \in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=G\ H\\E\not \in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=\operatorname {sink-test} [G\ \operatorname {sink-test} [(\lambda E.H)\ Y,X]]\\E\in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\operatorname {sink-test} [(\lambda E.G)\ Y,X])\ H\\E\in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\lambda E.G\ H)\ Y\end{cases}}

التجريد . استخدم إعادة التسمية لضمان أن تكون أسماء المتغيرات جميعها مميزة.

V\neq W\to \operatorname {sink} [(\lambda V.\lambda W.E)\ Y,X]=\lambda W.\operatorname {sink-test} [(\lambda V.E)\ Y,X]

المتغير - حالتان.

E\neq V\to \operatorname {sink} [(\lambda E.V)\ Y,X]=V

E=V\to \operatorname {sink} [(\lambda E.V)\ Y,X]=Y

اختبار الاستبعاد يمنع إسقاط التعبيرات،

L\in X\to \operatorname {sink-test} [L,X]=L

L\not \in X\to \operatorname {sink-test} [L,X]=\operatorname {sink} [L,X]

مثال

مثال على الغرق

على سبيل المثال،

قاعدة

تعبير

إلغاء التأجير

\operatorname {sink-tran} [\operatorname {de-let} [\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p]]

غرق-نقل

\operatorname {sink-tran} [(\lambda p.(\lambda q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f)))\ (\lambda f.\lambda x.f\ (x\ x))]

طلب

$\operatorname {sink} [(\lambda p.\operatorname {sink} [(\lambda q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))])\ (\lambda f.\lambda x.f\ (x\ x))]$
$\operatorname {sink} [(\lambda q.q\ p)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))]$
$E\in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]$
$E=q,G=q,H=p,Y=(\lambda p.\lambda f.(p\ f)\ (p\ f)),X=\{\}$
$(\operatorname {sink} [(\lambda E.G)\ Y,X])\ H$
$(\operatorname {sink} [(\lambda q.q)\ (\lambda p.\lambda f.(p\ f)\ (p\ f)),X])\ p$

عامل

$\operatorname {sink} [(\lambda p.\operatorname {sink} [(\lambda q.q)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))]\ p)\ (\lambda f.\lambda x.f\ (x\ x))]$
$\operatorname {sink} [(\lambda q.q)\ (\lambda p.\lambda f.(p\ f)\ (p\ f))]$
$E=V\to \operatorname {sink} [(\lambda E.V)\ Y,X]$
$E=q,V=q,Y=(\lambda p.\lambda f.(p\ f)\ (p\ f)),X=\{\}$
$Y$
$(\lambda p.\lambda f.(p\ f)\ (p\ f))$

طلب

$\operatorname {sink} [(\lambda p.(\lambda p.\lambda f.(p\ f)\ (p\ f))\ p)\ (\lambda f.\lambda x.f\ (x\ x))]$
$E\not \in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]$
$E=p,G=(\lambda p.\lambda f.(p\ f)\ (p\ f)),H=p,Y=(\lambda f.\lambda x.f\ (x\ x))$
$\operatorname {sink} [G\ \operatorname {sink} [(\lambda E.H)\ Y,X]]$

عامل

$\operatorname {sink} [(\lambda p.\lambda f.(p\ f)\ (p\ f))\ \operatorname {sink-test} [(\lambda p.p)\ (\lambda f.\lambda x.f\ (x\ x)),X]]$
$\operatorname {sink} [(\lambda p.p)\ (\lambda f.\lambda x.f\ (x\ x)),X]$
$E=V\to \operatorname {sink} [(\lambda E.V)\ Y,X]$
$E=p,V=p,Y=(\lambda f.\lambda x.f\ (x\ x)),X=\{\}$
$Y$
$(\lambda f.\lambda x.f\ (x\ x))$

التجريد

$\operatorname {sink} [(\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]$
$V\neq W\to \operatorname {sink} [(\lambda V.\lambda W.E)\ Y,X]$
$V=p,W=f,E=(p\ f)\ (p\ f),Y=(\lambda f.\lambda x.f\ (x\ x))$
$\lambda W.\operatorname {sink} [(\lambda V.E)\ Y,X]$

طلب

$\lambda f.\operatorname {sink} [(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x)),X]$
$\operatorname {sink} [(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x)),X]$
$E\in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]$
$E=p,G=(p\ f),H=(p\ f),Y=(\lambda f.\lambda x.f\ (x\ x))$
$(\lambda E.G\ H)\ Y$
$(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))$

\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))

إسقاط المعلمات

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

حذف مُعامل يعني إزالة مُعامل غير ضروري من دالة، حيث يكون المُعامل الفعلي المُمرر هو نفس التعبير دائمًا. يجب أن تكون المتغيرات الحرة للتعبير حرة أيضًا في موضع تعريف الدالة. في هذه الحالة، يُستبدل المُعامل المحذوف بالتعبير الموجود في متن تعريف الدالة، مما يجعله غير ضروري.

على سبيل المثال، لنفترض،

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y

في هذا المثال، يكون المعامل الفعلي للمعامل الرسمي o هو p دائمًا . وبما أن p متغير حر في التعبير بأكمله، يمكن حذف هذا المعامل. أما المعامل الفعلي للمعامل الرسمي y فهو n دائمًا . ومع ذلك، فإن n مرتبط في تجريد لامدا، لذا لا يمكن حذف هذا المعامل.

نتيجة حذف المعامل هي،

\operatorname {drop-params-tran} [\lambda m,p,q.(\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n))\ \lambda x.\lambda o.\lambda y.o\ x\ y

\equiv \lambda m,p,q.(\lambda g.\lambda n.n\ (g\ m\ n)\ (g\ q\ n))\ \lambda x.\lambda y.p\ x\ y

على سبيل المثال الرئيسي،

\operatorname {drop-params-tran} [\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]

\equiv \lambda f.(\lambda p.p\ p)\ (\lambda x.f\ (x\ x))

تعريف drop-params-tran هو،

\operatorname {drop-params-tran} [L]\equiv (\operatorname {drop-params} [L,D,FV[L],[]])

أين،

\operatorname {build-param-list} [L,D,V,\_]

إنشاء قوائم المعلمات

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

على سبيل المثال، في

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y

معاملات الدالة g هي:

المعامل الرسمي	جميعها لها نفس القيمة	التعبير الفعلي للمعامل
x	خطأ شنيع	_
o	حقيقي	ص
y	حقيقي	ن

يُعاد تسمية كل تجريد باسم فريد، وتُربط قائمة المعاملات باسم التجريد. على سبيل المثال، g لها قائمة معاملات.

D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]

تقوم الدالة build-param-lists بإنشاء جميع القوائم الخاصة بتعبير معين، وذلك من خلال المرور على التعبير. ولها أربعة معلمات؛

التعبير اللامدا قيد التحليل.
قائمة معلمات الجدول للأسماء.
جدول قيم المعلمات.
قائمة المعلمات المُعادة، والتي تُستخدم داخليًا بواسطة

التجريد - تعبير لامدا من الشكل $(\lambda N.S)\ L$ يتم تحليلها لاستخراج أسماء معلمات الدالة.

{\begin{cases}\operatorname {build-param-lists} [(\lambda N.S)\ L,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\land \operatorname {build-list} [L,D,V,D[N]]\\\operatorname {build-param-lists} [\lambda N.S,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\end{cases}}

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

{\begin{cases}\operatorname {build-list} [\lambda P.B,D,V,[X,\_,\_]::L]\equiv \operatorname {build-list} [B,D,V,L]\\\operatorname {build-list} [B,D,V,[]]\equiv \operatorname {build-param-lists} [B,D,V,\_]\end{cases}}

المتغير - استدعاء لدالة.

\operatorname {build-param-lists} [N,D,V,D[N]]

بالنسبة لاسم دالة أو معلمة، ابدأ بتعبئة قائمة المعلمات الفعلية عن طريق إخراج قائمة المعلمات لهذا الاسم.

التطبيق - تتم معالجة التطبيق (استدعاء الدالة) لاستخراج تفاصيل المعلمات الفعلية.

\operatorname {build-param-lists} [E\ P,D,V,R]\equiv \operatorname {build-param-lists} [E,D,V,T]\land \operatorname {build-param-lists} [P,D,V,K]

\land T=[F,S,A]::R\land (S\implies (\operatorname {equate} [A,P]\land V[F]=A))\land D[F]=K

استرجع قوائم المعاملات الخاصة بالتعبير، والمعامل نفسه. استرجع سجل المعامل من قائمة المعاملات الخاصة بالتعبير، وتحقق من تطابق قيمة المعامل الحالية مع هذا المعامل. سجّل قيمة اسم المعامل لاستخدامها لاحقًا في عملية التحقق.

{\begin{cases}\operatorname {equate} [A,N]\equiv A=N\lor (\operatorname {def} [V[N]]\land A=V[N])&{\text{if }}N{\text{ is a variable.}}\\\operatorname {equate} [A,E]\equiv A=E&{\text{otherwise.}}\end{cases}}

المنطق المذكور أعلاه دقيقٌ للغاية في طريقة عمله. لا يتم تعيين مؤشر القيمة نفسه إلى "صحيح" مطلقًا، وإنما إلى "خطأ" فقط في حال تعذّر مطابقة جميع القيم. تُسترجع القيمة باستخدام S لإنشاء مجموعة من القيم المنطقية المسموح بها لـ S. إذا كانت القيمة "صحيح" ضمن هذه المجموعة، فإن جميع قيم هذا المعامل متساوية، ويمكن حذف المعامل.

\operatorname {ask} [S]\equiv S\in \{X:X=S\}

وبالمثل، تستخدم الدالة def نظرية المجموعات للاستعلام عما إذا تم إعطاء قيمة لمتغير ما؛

\operatorname {def} [F]\equiv |\{X:X=F\}|

ليكن - تعبير ليكن.

\operatorname {build-param-list} [\operatorname {let} V:E\operatorname {in} L,D,V,\_]\equiv \operatorname {build-param-list} [E,D,V,\_]\land \operatorname {build-param-list} [L,D,V,\_]

و - للاستخدام في "let".

\operatorname {build-param-lists} [E\land F,D,V,\_]\equiv \operatorname {build-param-lists} [E,D,V,\_]\land \operatorname {build-param-lists} [F,D,V,\_]

أمثلة

على سبيل المثال، بناء قوائم المعلمات لـ،

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y

يعطي،

D[g]=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]

ويتم حذف المعامل o للحصول على،

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ n)\ (g\ q\ n)))\ \lambda x.\lambda y.p\ x\ y

إنشاء قائمة المعلمات لـ

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y

مثال على قائمة معلمات البناء

$\operatorname {build-param-list} [\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y,D,V,\_]$
قاعدة	تعبير
التجريد	$\operatorname {build-param-list} [\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y,D,V,\_]$
التجريد	$\operatorname {build-param-list} [(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y,D,V,\_]$
	$\operatorname {build-param-lists} [n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,V,R]\land \operatorname {build-list} [\lambda x.\lambda o.\lambda y.o\ x\ y,D,V,D[g]]$

$\operatorname {build-list} [\lambda x.\lambda o.\lambda y.o\ x\ y,D,V,D[g]]$
قاعدة	تعبير
أضف معلمة	$\operatorname {build-list} [\lambda x.\lambda o.\lambda y.o\ x\ y,D,V,D[g]]\land D[g]=L_{1}$
أضف معلمة	$\operatorname {build-list} [\lambda o.\lambda y.o\ x\ y,D,V,L_{1}]\land D[g]=[x,\_,\_]::L_{1}$
أضف معلمة	$\operatorname {build-list} [\lambda y.o\ x\ y,D,V,L_{2}]\land D[g]=[x,\_,\_]::[o,\_,\_]::L_{2}$
إندري	$\operatorname {build-list} [o\ x\ y,D,V,L_{3}]\land D[g]=[x,\_,\_]::[o,\_,\_]::[y,\_,\_]::L_{3}$
	$\operatorname {build-param-lists} [o\ x\ y,D,V,[]]\land D[g]=[x,\_,\_]::[o,\_,\_]::[y,\_,\_]::[]$

$\operatorname {build-param-lists} [n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,V,R]$
قاعدة	تعبير
طلب	$\operatorname {build-param-lists} [n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,V,R]$
طلب	$\operatorname {build-param-lists} [n\ (g\ m\ p\ n),D,V,T_{1}]\land \operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ $\land ((T_{1}=[F_{1},S_{1},A_{1}]::R$ $\land (S_{1}\implies (\operatorname {equate} [A_{1},g\ q\ p\ n]\land V[F_{1}]=g\ q\ p\ n))\land D[F_{1}]=K_{1})$
عامل	$\operatorname {build-param-lists} [n,D,V,T_{2}]\land \operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]\land \operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ $\land ((T_{2}=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::R$ $\land (S_{1}\implies (\operatorname {equate} [A_{1},g\ q\ p\ n]\land V[F_{1}]=g\ q\ p\ n))\land D[F_{1}]=K_{1})$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},g\ m\ p\ n]\land V[F_{2}]=g\ m\ p\ n))\land D[F_{2}]=K_{2})$
عامل	$\operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]\land \operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$ $\land ((D[n]=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::R$ $\land (S_{1}\implies (\operatorname {equate} [A_{1},g\ q\ p\ n]\land V[F_{1}]=g\ q\ p\ n))\land D[F_{1}]=K_{1})$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},g\ m\ p\ n]\land V[F_{2}]=g\ m\ p\ n))\land D[F_{2}]=K_{2})$

يعطي،

D[n]=[\_,\_,g\ m\ p\ n]::[\_,\_,g\ q\ p\ n]::R

$\operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]$
قاعدة	تعبير
طلب	$\operatorname {build-param-lists} [g\ m\ p\ n,D,V,K_{2}]$
	$\operatorname {build-param-lists} [g\ m\ p,D,V,T_{3}]\land \operatorname {build-param-lists} [n,D,V,K_{3}]$ $\land ((T_{3}=[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[F_{3}]=n))\land D[F_{3}]=D[n])$
التطبيق، متغير	$\operatorname {build-param-lists} [g\ m,D,V,T_{4}]\land \operatorname {build-param-lists} [p,D,V,K_{4}]$ $\land T_{4}=[\_,S_{4},A_{4}]::[\_,S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[F_{3}]=n))\land D[F_{3}]=D[n])$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=p))\land D[F_{4}]=D[p]$
التطبيق، متغير	$\operatorname {build-param-lists} [g,D,V,T_{5}]\land \operatorname {build-param-lists} [m,D,V,K_{5}]$ $\land T_{5}=[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[F_{3}]=n))\land D[F_{3}]=D[n])$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=p))\land D[F_{4}]=D[p]$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},m]\land V[F_{5}]=m))\land D[F_{5}]=D[m]$
عامل	$D[g]=[x,S_{5},A_{5}]::[o,S_{4},A_{4}]::[y,S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},n]\land V[y]=n))\land D[y]=D[n])$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[o]=p))\land D[o]=D[p]$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},m]\land V[x]=m))\land D[x]=D[m]$

$\operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$
قاعدة	تعبير
طلب	$\operatorname {build-param-lists} [g\ q\ p\ n,D,V,K_{1}]$
	$\operatorname {build-param-lists} [g\ q\ p,D,V,T_{6}]\land \operatorname {build-param-lists} [n,D,V,K_{6}]$ $\land ((T_{6}=[F_{6},S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[F_{6}]=n))\land D[F_{6}]=D[n])$
التطبيق، متغير	$\operatorname {build-param-lists} [g\ q,D,V,T_{7}]\land \operatorname {build-param-lists} [p,D,V,K_{7}]$ $\land T_{7}=[\_,S_{7},A_{7}]::[\_,S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[F_{6}]=n))\land D[F_{6}]=D[n])$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},p]\land V[F_{7}]=p))\land D[F_{7}]=D[p]$
التطبيق، متغير	$\operatorname {build-param-lists} [g,D,V,T_{8}]\land \operatorname {build-param-lists} [m,D,V,K_{8}]$ $\land T_{8}=[F_{8},S_{8},A_{8}]::[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[F_{6}]=n))\land D[F_{6}]=D[n])$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},p]\land V[F_{7}]=p))\land D[F_{7}]=D[p]$ $\land (S_{8}\implies (\operatorname {equate} [A_{8},q]\land V[F_{8}]=q))\land D[F_{8}]=D[q]$
عامل	$D[g]=[x,S_{8},A_{8}]::[o,S_{6},A_{7}]::[y,S_{6},A_{6}]::K_{1}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},n]\land V[y]=n))\land D[y]=D[n])$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},p]\land V[o]=p))\land D[o]=D[p]$ $\land (S_{8}\implies (\operatorname {equate} [A_{8},q]\land V[x]=q))\land D[x]=D[q]$

بما أنه لا توجد تعريفات لـ، $V[n],V[p],V[q],V[m]$ ويمكن تبسيط المعادلة إلى:

\operatorname {equate} [A,N]\equiv A=N\lor (\operatorname {def} [V[N]]\land A=V[N])\equiv A=N

بإزالة التعبيرات غير الضرورية، $D[g]=[x,S_{5},A_{5}]::[o,S_{4},A_{4}]::[y,S_{3},A_{3}]::K_{2}$

\land S_{3}\implies A_{3}=n

\land S_{4}\implies A_{4}=p

\land S_{5}\implies A_{5}=m

$D[g]=[x,S_{8},A_{8}]::[o,S_{6},A_{7}]::[y,S_{6},A_{6}]::K_{1}$

\land S_{6}\implies A_{6}=n

\land S_{7}\implies A_{7}=p

\land S_{8}\implies A_{8}=q

بمقارنة التعبيرين لـ $D[g]$ ، يحصل،

S_{5}=S_{8},A_{5}=A_{8},S_{4}=S_{7},A_{4}=A_{7},S_{3}=S_{6},A_{3}=A_{6}

لو $S_{3}$ صحيح؛

n=A_{3}=A_{6}=n

لو $S_{3}$ إذا كان هذا غير صحيح، فلا يوجد أي دلالة. $S_{3}=\_$ وهذا يعني أنه قد يكون صحيحاً أو خاطئاً.

لو $S_{4}$ صحيح؛

p=A_{4}=A_{7}=p

لو $S_{5}$ صحيح؛

m=A_{5}=A_{8}=q

لذا $S_{5}$ هذا غير صحيح.

والنتيجة هي، $D[g]=[x,\operatorname {false} ,\_]::[o,\_,p]::[y,\_,n]::\_$

$\operatorname {build-param-lists} [o\ x\ y,D,V,L]$
قاعدة	تعبير
طلب	$\operatorname {build-param-lists} [o\ x\ y,D,V,L]$
طلب	$\operatorname {build-param-lists} [o\ x,D,V,T_{9}]\land \operatorname {build-param-lists} [y,D,V,K_{9}]$ $\land T_{9}=[F_{9},S_{9},A_{9}]::L$ $\land (S_{9}\implies (\operatorname {equate} [A_{9},y]\land V[F_{9}]=A_{9})\land K_{9}=D[F_{9}]$
عامل	$\operatorname {build-param-lists} [o,D,V,T_{10}]\land \operatorname {build-param-lists} [x,D,V,K_{10}]\land \operatorname {build-param-lists} [y,D,V,K_{10}]$ $\land T_{10}=[F_{10},S_{10},A_{10}]::[F_{9},S_{9},A_{9}]::L$ $\land (S_{9}\implies (\operatorname {equate} [A_{9},y]\land V[F_{9}]=A_{9})\land K_{9}=D[F_{9}]$ $\land (S_{10}\implies (\operatorname {equate} [A_{10},y]\land V[F_{10}]=A_{10})\land K_{10}=D[F_{10}]$
	$\land D[o]=[F_{10},S_{10},A_{10}]::[F_{9},S_{9},A_{9}]::L$ $\land (S_{9}\implies (\operatorname {equate} [A_{9},y]\land V[F_{9}]=A_{9})\land K_{9}=D[F_{9}]$ $\land (S_{10}\implies (\operatorname {equate} [A_{10},y]\land V[F_{10}]=A_{10})\land K_{10}=D[F_{10}]$

وباستخدام حجج مماثلة لتلك المستخدمة أعلاه، نحصل على:

D[o]=[\_,\_,x]::[\_,\_,y]::\_

ومن السابق،

D[g]=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]

D[n]=[[\_,\_,(g\ m\ p\ n)],[\_,\_,(g\ q\ p\ n)]]

D[m]=\_

D[p]=\_

D[q]=\_

مثال آخر هو،

\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x))

هنا، x تساوي f. ويكون تعيين قائمة المعاملات كما يلي:

D[p]=[[q,\_,p],[x,\_,f]]

ويتم حذف المعامل x للحصول على،

\lambda f.((\lambda q.f\ (q\ q))\ (\lambda q.f\ (q\ q))

إنشاء قائمة المعلمات لـ

\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x))

يتم استخدام المنطق الموجود في برنامج equate في هذا المثال الأكثر صعوبة.

$\operatorname {build-param-list} [\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$
قاعدة	تعبير
التجريد	$\operatorname {build-param-list} [\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$
التجريد	$\operatorname {build-param-list} [(\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$
	$\operatorname {build-param-lists} [f\ (p\ p\ f),D,\_]\land \operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]$
	$\operatorname {build-param-lists} [f\ (p\ p\ f),D,\_]\land \operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]$

$\operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]$
قاعدة	تعبير
أضف معلمة	$\operatorname {build-list} [\lambda q.\lambda x.x\ (q\ q\ x),D,D[p]]\land D[p]=L_{1}$
أضف معلمة	$\operatorname {build-list} [\lambda x.x\ (q\ q\ x),D,L_{2}]\land D[p]=[q,\_,\_]::L_{2}$
إندري	$\operatorname {build-list} [x\ (q\ q\ x),D,L_{3}]\land D[p]=[q,\_,\_]::[x,\_,\_]::L_{3}$
	$\operatorname {build-param-lists} [x\ (q\ q\ x),D,[]]\land D[p]=[q,\_,\_]::[x,\_,\_]::[]$

$\operatorname {build-param-lists} [\lambda p.f\ (p\ p\ f),D,V,T_{1}]$
قاعدة	تعبير
التجريد	$\operatorname {build-param-lists} [\lambda p.f\ (p\ p\ f),D,V,T_{1}]$
طلب	$\operatorname {build-param-lists} [f\ (p\ p\ f),D,V,T_{1}]$
اسم	$\operatorname {build-param-lists} [f,D,V,T_{2}]\land \operatorname {build-param-lists} [p\ p\ f,D,V,K_{2}]$ $\land T_{2}=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},p\ p\ f]\land V[F_{2}]=A_{2}))\land D[F_{2}]=K_{2}$
اسم	$\operatorname {build-param-lists} [p\ p\ f,D,V,K_{2}]$ $\land D[f]=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},p\ p\ f]\land V[F_{2}]=A_{2}))\land D[F_{2}]=K_{2}$
اسم	$\operatorname {build-param-lists} [p\ p,D,V,T_{3}]\land \operatorname {build-param-lists} [f,D,V,K_{3}]$ $\land T_{3}=[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=K_{3}$
طلب	$\operatorname {build-param-lists} [p\ p,D,V,T_{3}]$ $\land T_{3}=[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{2}\implies (\operatorname {equate} [A_{2},p\ p\ f]\land V[F_{2}]=A_{2}))\land D[F_{2}]=K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]$
اسم	$\operatorname {build-param-lists} [p,D,V,T_{4}]\land \operatorname {build-param-lists} [p,D,V,K_{4}]$ $\land T_{4}=[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=A_{4}))\land D[F_{4}]=K_{4}$
	$D[p]=[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}$ $\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]$ $\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=A_{4}))\land D[F_{4}]=D[p]$

$\operatorname {build-param-lists} [x\ (q\ q\ x)),D,V,\_]$
قاعدة	تعبير
التجريد	$\operatorname {build-param-lists} [\lambda q.\lambda x.x\ (q\ q\ x)),D,V,\_]$
طلب	$\operatorname {build-param-lists} [x\ (q\ q\ x)),D,V,K_{1}]$
اسم	$\operatorname {build-param-lists} [x,D,V,T_{5}]\land \operatorname {build-param-lists} [q\ q\ x,D,V,K_{5}]$ $\land T_{5}=[F_{5},S_{5},A_{5}]::\_$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},q\ q\ x]\land V[F_{5}]=A_{5}))\land D[F_{5}]=K_{5}$
اسم	$\operatorname {build-param-lists} [q\ q\ x,D,V,K_{5}]$ $\land D[x]=[F_{5},S_{5},A_{5}]::\_$ $\land (S_{5}\implies (\operatorname {equate} [A_{5},q\ q\ x]\land V[F_{5}]=A_{5}))\land D[F_{5}]=K_{5}$
اسم	$\operatorname {build-param-lists} [q\ q,D,V,T_{6}]\land \operatorname {build-param-lists} [x,D,V,K_{6}]$ $\land T_{6}=[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=K_{6}$
طلب	$\operatorname {build-param-lists} [q\ q,D,V,T_{6}]$ $\land T_{6}=[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$
اسم	$\operatorname {build-param-lists} [q,D,V,T_{7}]\land \operatorname {build-param-lists} [q,D,V,K_{7}]$ $\land T_{7}=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=K_{7}$
اسم	$\operatorname {build-param-lists} [q,D,V,K_{7}]$ $\land D[q]=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}$ $\land (S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]$ $\land (S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=D[q]$

بعد جمع النتائج معًا،

D[p]=[q,\_,\_]::[x,\_,\_]::L_{3}

D[p]=[F_{4},S_{4},A_{4}]::[F_{3},S_{3},A_{3}]::K_{2}

\land (S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[F_{3}]=A_{3}))\land D[F_{3}]=D[f]

\land (S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[F_{4}]=A_{4}))\land D[F_{4}]=D[p]

D[q]=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}

(S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]

(S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=D[q]

من التعريفين لـ $D[p]$ ؛

F_{4}=q

F_{3}=x

لذا

D[p]=[q,S_{4},A_{4}]::[x,S_{3},A_{3}]::K_{2}

(S_{3}\implies (\operatorname {equate} [A_{3},f]\land V[x]=A_{3}))\land D[x]=D[f]

(S_{4}\implies (\operatorname {equate} [A_{4},p]\land V[q]=A_{4}))\land D[q]=D[p]

استخدام $D[q]=D[p]$ و

D[p]=[F_{7},S_{7},A_{7}]::[F_{6},S_{6},A_{6}]::K_{5}

(S_{6}\implies (\operatorname {equate} [A_{6},x]\land V[F_{6}]=A_{6}))\land D[F_{6}]=D[x]

(S_{7}\implies (\operatorname {equate} [A_{7},q]\land V[F_{7}]=A_{7}))\land D[F_{7}]=D[q]

بالمقارنة مع ما سبق،

F_{7}=q,F_{6}=x,A_{3}=A_{6},A_{4}=A_{7},S_{3}=S_{6},S_{4}=S_{7}

لذا،

V[x]=A_{3}

V[q]=A_{4}

في،

S_{3}\implies A_{3}=f

S_{3}\implies (A_{3}=x\lor A_{3}=v[x])

يختزل إلى،

S_{3}\implies A_{3}=f

أيضًا،

S_{4}\implies A_{4}=p

S_{4}\implies (A_{4}=q\lor A_{4}=v[q])

يختزل إلى،

S_{4}\implies A_{4}=p

لذا فإن قائمة المعاملات لـ p هي فعلياً؛

D[p]=[q,\_,p]::[x,\_,f]::\_

معلمات الإسقاط

استخدم المعلومات التي تم الحصول عليها من خلال إنشاء قوائم المعلمات لحذف المعلمات الفعلية التي لم تعد مطلوبة. تحتوي قائمة المعلمات على drop-params .

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

التجريد

\operatorname {drop-params} [(\lambda N.S)\ L,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])\ \operatorname {drop-formal} [D[N],L,F]

أين،

F=FV[(\lambda N.S)\ L]

\operatorname {drop-params} [\lambda N.S,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])

أين،

F=FV[\lambda N.S]

عامل

\operatorname {drop-params} [N,D,V,D[N]]\equiv N

بالنسبة لاسم دالة أو معلمة، ابدأ بتعبئة قائمة المعلمات الفعلية عن طريق إخراج قائمة المعلمات لهذا الاسم.

التطبيق - تتم معالجة تطبيق (استدعاء دالة) لاستخراج

(\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]

\neg (\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]\ \operatorname {drop-params} [P,D,V,\_]

ليكن - تعبير ليكن.

\operatorname {drop-params} [\operatorname {let} V:E\operatorname {in} L]\equiv \operatorname {let} V:\operatorname {drop-params} [E,D,FV[E],[]]\operatorname {in} \operatorname {drop-params} [L,D,FV[L],[]]

و - للاستخدام في "let".

\operatorname {drop-params} [E\land F,D,V,\_]\equiv \operatorname {drop-params} [E,D,V,\_]\land \operatorname {drop-params} [F,D,V,\_]

حذف المعلمات من التطبيقات

$\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n)$
حالة	تعبير
	$\operatorname {drop-param} [\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,\{p,q,m\},\_]$
	$\lambda g.\operatorname {drop-param} [\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n),D,\{p,q,m\},\_]$
$\neg (\operatorname {def} [F_{1}]\land ...)$	$\lambda g.\lambda n.\operatorname {drop-param} [n\ (g\ m\ p\ n),D,\{p,q,m\},[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$
$\neg (\operatorname {def} [F_{2}]\land ...)$	$\lambda g.\lambda n.\operatorname {drop-param} [n\ ,D,\{p,q,m\},[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-param} [(g\ m\ p\ n),D,\{p,q,m\},\_]\ \operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$
$D[n]=[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]$	$\lambda g.\lambda n.n\ \operatorname {drop-param} [(g\ m\ p\ n),D,\{p,q,m\},\_]\ \operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$

من نتائج بناء قوائم المعلمات؛

D[n]=[[\_,\_,(g\ m\ p\ n)],[\_,\_,(g\ q\ p\ n)]]

لذا،

F_{1}=\_

F_{2}=\_

لذا،

\operatorname {def} [F_{1}]=\operatorname {false}

\operatorname {def} [F_{2}]=\operatorname {false}

$\operatorname {drop-param} [(g\ m\ p\ n),D,\{p,q,m\},\_]$
حالة	موسع	تعبير
$V=\{p,q,m\}$		$\operatorname {drop-param} [(g\ m\ p\ n),D,V,\_]$
$FV(A_{1})\not \subset \{p,q,m\}$	$n\not \subset \{p,q,m\}$	$\operatorname {drop-params} [g\ m\ p,D,V,[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$
$\operatorname {def} [F_{2}]\land \operatorname {ask} [S_{2}]\land FV[A_{2}]\subset V$	$\operatorname {def} [y]\land \operatorname {ask} [\_]\land FV[p]\subset \{p,q,m\}$	$\operatorname {drop-params} [g\ m,D,V,[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$
$\neg \operatorname {ask} [S_{3}]$	$\neg \operatorname {ask} [\operatorname {false} ]$	$\operatorname {drop-params} [g,D,V,[F_{3},S_{3},A_{3}]::[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]\ \operatorname {drop-params} [m,D,V,\_]\ \operatorname {drop-params} [n,D,V,\_]$
$D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]$ $=[F_{3},S_{3},A_{3}]::[F_{2},S_{2},A_{2}]::[F_{1},S_{1},A_{1}]::\_]$	$F_{3}=x,S_{3}=\operatorname {false} ,A_{3}=\_$ $F_{2}=o,S_{2}=\_,A_{2}=p$ $F_{1}=y,S_{1}=\_,A_{1}=n$	$g\ m\ n$

$\operatorname {drop-param} [(g\ q\ p\ n),D,\{p,q,m\},\_]$
حالة	موسع	تعبير
V = {p, q, m}		$\operatorname {drop-param} [(g\ q\ p\ n),D,V,\_]$
$FV(A_{4})\not \subset V$	$n\not \subset \{p,q,m\}$	$\operatorname {drop-params} [g\ q\ p,D,V,[F_{4},S_{4},A_{4}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$
$\operatorname {def} [F_{5}]\land \operatorname {ask} [S_{5}]\land FV[A_{5}]\subset V$	$\operatorname {def} [o]\land \operatorname {ask} [\_]\land p\subset \{p,q,m\})$	$\operatorname {drop-params} [g\ q,D,V,[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::\_]\ \operatorname {drop-params} [n,D,V,\_]$
$\neg \operatorname {ask} [S-6]$	$\neg \operatorname {ask} [\operatorname {false} ]$	$\operatorname {drop-params} [g,D,V,[F_{6},S_{6},A_{6}]::[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::\_]\ \operatorname {drop-params} [m,D,V,\_]\ \operatorname {drop-params} [n,D,V,\_]$
$D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]$ $=[F_{6},S_{6},A_{6}]::[F_{5},S_{5},A_{5}]::[F_{4},S_{4},A_{4}]::\_]$	$F_{6}=x,S_{6}=\operatorname {false} ,A_{6}=\_$ $F_{5}=o,S_{5}=\_,A_{5}=p$ $F_{4}=y,S_{4}=\_,A_{4}=n$	$g\ q\ n$

حذف المعاملات الرسمية

تقوم الدالة drop-formal بإزالة المعاملات الرسمية، بناءً على محتويات القوائم المنسدلة. معاملاتها هي:

قائمة الحذف،
تعريف الدالة (تجريد لامدا).
المتغيرات الحرة من تعريف الدالة.

يُعرَّف حذف الصيغة الرسمية على النحو التالي:

$(\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \operatorname {drop-formal} [[F,S,A]::Z,Y[F:=A],L]$
$\neg (\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \lambda F.\operatorname {drop-formal} [[F,S,A]::Z,Y,V]$
$\operatorname {drop-formal} [Z,Y,V]\equiv Y$

ويمكن تفسير ذلك على النحو التالي:

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

حالة	تعبير
$\operatorname {false}$	$\operatorname {drop-formal} [D,\lambda x.\lambda o.\lambda y.o\ x\ y,F]$
$\operatorname {true} \land \{p\}\subset F$	$\lambda x.\operatorname {drop-formal} [D,\lambda o.\lambda y.o\ x\ y,F]$
$\neg (\operatorname {true} \land \{n\}\subset F$ )	$\lambda x.\operatorname {drop-formal} [D,(\lambda y.o\ x\ y)[o:=p],F]$
	$\lambda x.\lambda y.\operatorname {drop-formal} [D,p\ x\ y,F]$
	$\lambda x.\lambda y.p\ x\ y$

مثال

بدءًا من تعريف دالة مُركِّب Y،

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\

تحويل	تعبير
	$\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p$
ملخص * 4	$\operatorname {let} p=\lambda f.\lambda x.f\ (x\ x)\land q=\lambda p.\lambda f.(p\ f)\ (p\ f)\operatorname {in} q\ p$
لامدا-مجرد-ترجمة	$(\lambda q.(\lambda p.q\ p)\ (\lambda f.\lambda x.f\ (x\ x)))\ (\lambda p.\lambda f.(p\ f)\ (p\ f))$
غرق-نقل	$(\lambda p.\lambda f.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))$
غرق-نقل	$\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))$
حذف المعامل	$\lambda f.(\lambda p.p\ p)\ (\lambda x.f\ (x\ x))$
بيتا ريدكس	$\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\$

مما يعيد مُركِّب Y ،

\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))

انظر أيضاً

مراجع

↑ جونسون، توماس (1985). "رفع لامدا: تحويل البرامج إلى معادلات تكرارية". في: جوانو، جيه بي (محرر). لغات البرمجة الوظيفية وهندسة الحاسوب. FPCA 1985. سلسلة محاضرات في علوم الحاسوب. المجلد 201. سبرينغر. CiteSeerX 10.1.1.48.4346 . doi : 10.1007/3-540-15975-4_37 . ISBN 3-540-15975-4.
↑ مورازان، ماركو ت.؛ شولتز، أولريك ب. (2008). "الرفع الأمثل لدالة لامدا في زمن تربيعي". تنفيذ وتطبيق اللغات الوظيفية - أوراق مختارة منقحة . ص 37-56 . doi : 10.1007/978-3-540-85373-2_3 . ISBN 978-3-540-85372-5.
↑ دانفي، أو.؛ شولتز، يو بي (1997). "إسقاط لامدا" . إشعارات ACM SIGPLAN . 32 (12): 90-106 . doi : 10.1145/258994.259007 .
↑ دانفي، أوليفييه؛ شولتز، أولريك ب. (أكتوبر 2000). "حذف لامدا: تحويل المعادلات التكرارية إلى برامج ذات بنية كتلية" (ملف PDF) . علوم الحاسوب النظرية . 248 ( 1-2 ): 243-287 . CiteSeerX 10.1.1.16.3943 . doi : 10.1016/S0304-3975(00)00054-2 . BRICS-RS-99-27.

روابط خارجية

شرح على موقع Stack Overflow، مع مثال بلغة JavaScript
سلونيجر، كين؛ كورتز، باري. "5. بعض المناقشات حول تعابير let" (ملف PDF) . أسس لغات البرمجة . جامعة أيوا.

[1] جونسون، توماس (1985). "رفع لامدا: تحويل البرامج إلى معادلات تكرارية". في: جوانو، جيه بي (محرر). لغات البرمجة الوظيفية وهندسة الحاسوب. FPCA 1985. سلسلة محاضرات في علوم الحاسوب. المجلد 201. سبرينغر. CiteSeerX 10.1.1.48.4346 . doi : 10.1007/3-540-15975-4_37 . ISBN 3-540-15975-4.

[Quadratic-2] مورازان، ماركو ت.؛ شولتز، أولريك ب. (2008). "الرفع الأمثل لدالة لامدا في زمن تربيعي". تنفيذ وتطبيق اللغات الوظيفية - أوراق مختارة منقحة . ص 37-56 . doi : 10.1007/978-3-540-85373-2_3 . ISBN 978-3-540-85372-5.

[3] دانفي، أو.؛ شولتز، يو بي (1997). "إسقاط لامدا" . إشعارات ACM SIGPLAN . 32 (12): 90-106 . doi : 10.1145/258994.259007 .

[4] دانفي، أوليفييه؛ شولتز، أولريك ب. (أكتوبر 2000). "حذف لامدا: تحويل المعادلات التكرارية إلى برامج ذات بنية كتلية" (ملف PDF) . علوم الحاسوب النظرية . 248 ( 1-2 ): 243-287 . CiteSeerX 10.1.1.16.3943 . doi : 10.1016/S0304-3975(00)00054-2 . BRICS-RS-99-27.

[ 1 ]

[

[ 3 ]

[ 4 ]

اللغة	العربية (RTL)
روابط موسوعية	30 رابطاً
المصدر الأصلي	ويكيبيديا ↗