دع التعبير

تحتاج هذه المقالة إلى مصادر إضافية للتحقق . يُرجى المساعدة في تحسين هذه المقالة بإضافة مصادر موثوقة . قد يتم الطعن في المواد غير الموثقة وإزالتها. البحث عن المصادر:  "Let expression" – news  · journalist  · books  · scholar  · JSTOR ( March 2017 ) ( Learn how and when to remove this message )

في علوم الكمبيوتر، يربط تعبير "let" تعريف الدالة بنطاق مقيد .

يمكن أيضًا تعريف تعبير "let" في الرياضيات، حيث يربط شرطًا منطقيًا بنطاق مقيد.

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

توجد عبارة let في العديد من اللغات الوظيفية للسماح بالتعريف المحلي للتعبير، لاستخدامه في تعريف تعبير آخر. توجد عبارة let في بعض اللغات الوظيفية في شكلين؛ let أو "let rec". Let rec هو امتداد لتعبير let البسيط الذي يستخدم مجموعة النقطة الثابتة لتنفيذ التكرار .

كانت لغة LCF الخاصة بدانا سكوت ^[1] مرحلة في تطور حساب لامدا إلى لغات وظيفية حديثة. قدمت هذه اللغة تعبير let، الذي ظهر في معظم اللغات الوظيفية منذ ذلك الوقت.

لقد ورثت اللغات Scheme و ^[2] ML ومؤخرًا Haskell ^{[3] تعبيرات let من LCF.}

تطبق اللغات الأمرية ذات الحالة مثل ALGOL و Pascal بشكل أساسي تعبير let، لتنفيذ نطاق محدود من الوظائف، في هياكل الكتل. ^{[ بحاجة لمصدر ]}

ظهرت بالفعل جملة " where " وثيقة الصلة ، إلى جانب متغيرها المتكرر " where rec "، في كتاب بيتر لاندين "التقييم الميكانيكي للتعبيرات" . ^[4]

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

دع التعبير	بند أين
يترك ${\displaystyle أ=3}$ و ${\displaystyle b=4}$ في ${\displaystyle {\sqrt {a^{2}+b^{2}}}}$	${\displaystyle {\sqrt {a^{2}+b^{2}}}}$ أين ${\displaystyle أ=3}$ و ${\displaystyle b=4}$

في كلتا الحالتين، يكون البناء بأكمله عبارة عن تعبير قيمته 5. وكما هو الحال مع if-then-else، فإن النوع الذي يتم إرجاعه بواسطة التعبير ليس بالضرورة منطقيًا.

يأتي تعبير let في أربعة أشكال رئيسية،

استمارة	و	متكرر	التعريف / القيد	وصف
بسيط	لا	لا	تعريف	تعريف وظيفة بسيطة غير متكررة.
متكرر	لا	نعم	تعريف	تعريف الدالة المتكررة (تم تنفيذها باستخدام مجموعة Y ).
مشترك	نعم	نعم	تعريف	تعريف الدالة التكرارية المتبادلة.
رياضيات	نعم	نعم	القيد	تعريف رياضي يدعم شرطًا منطقيًا عامًا.

في اللغات الوظيفية، يحدد تعبير let الوظائف التي يمكن استدعاؤها في التعبير. يقتصر نطاق اسم الوظيفة على بنية تعبير let.

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

تختلف المصطلحات والنحو والدلالات من لغة إلى أخرى. في Scheme ، يتم استخدام let للشكل البسيط و let rec للشكل المتكرر. في ML، يشير let فقط إلى بداية كتلة من الإعلانات بينما يشير fun إلى بداية تعريف الوظيفة. في Haskell، قد يكون let متكررًا بشكل متبادل، حيث يكتشف المترجم ما هو مطلوب.

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

${\displaystyle (\lambda fz)\ (\lambda xy)}$

يعادل تعريف الدالة بواسطة في التعبير ، والذي يمكن كتابته على هيئة تعبير let ؛ ${\displaystyle f}$${\displaystyle f\x=y}$${\displaystyle z}$

${\displaystyle \operatorname {دع} f\ x=y\operatorname {في} z}$

يمكن فهم تعبير let باعتباره تعبيرًا بلغة طبيعية. يمثل تعبير let استبدال متغير بقيمة. تصف قاعدة الاستبدال آثار المساواة باعتبارها استبدالًا.

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

${\displaystyle (\exists xE\land F)\iff \operatorname {دع} x:E\operatorname {في} F}$

حيث أن E و F من النوع المنطقي.

يسمح تعبير let بتطبيق الاستبدال على تعبير آخر. يمكن تطبيق هذا الاستبدال ضمن نطاق مقيد، على تعبير فرعي. الاستخدام الطبيعي لتعبير let هو في التطبيق على نطاق مقيد (يسمى إسقاط lambda ). تحدد هذه القواعد كيفية تقييد النطاق؛

${\displaystyle {\begin{cases}x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)\\x\in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=(\operatorname {let} x:G\operatorname {in} E)\ F\\x\not \in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ F\end{cases}}}$

حيث F ليس من النوع المنطقي. ومن هذا التعريف، يمكن استخلاص التعريف القياسي التالي لتعبير let، كما هو مستخدم في لغة وظيفية.

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {دع} x:x=y\operatorname {in} z)=z[x:=y]=(\lambda xz)\y}$

من أجل التبسيط، سيتم حذف العلامة التي تحدد المتغير الوجودي، من التعبيرات عندما يكون ذلك واضحًا من السياق. ${\displaystyle x:}$

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {دع} x=y\operatorname {in} z)=z[x:=y]=(\lambda xz)\y}$

وللتوصل إلى هذه النتيجة، افترض أولاً،

${\displaystyle x\not \in \operatorname {FV} (L)}$

ثم

${\displaystyle {\begin{aligned}L\ (\operatorname {let} x:x=y\operatorname {in} z)&\iff (\operatorname {let} x:x=y\operatorname {in} L\ z)\\&\iff x=y\land L\ z\end{aligned}}}$

باستخدام قاعدة الاستبدال،

${\displaystyle {\begin{aligned}&\iff x=y\land (L\z)[x:=y]\\&\iff x=y\land (L[x:=y]\z[x:=y])\\&\iff x=y\land L\z[x:=y]\\&\implies L\z[x:=y]\end{aligned}}}$

لذلك بالنسبة لجميع L ،

${\displaystyle L\operatorname {دع} x:x=y\operatorname {في} z\يعني L\z[x:=y]}$

ليكن حيث K هو متغير جديد. إذن، ${\displaystyle L\ X=(X=K)}$

${\displaystyle (\operatorname {دع} x:x=y\operatorname {في} z)=K\يعني z[x:=y]=K}$

لذا،

${\displaystyle \operatorname {let} x:x=y\operatorname {in} z=z[x:=y]}$

ولكن من التفسير الرياضي لتخفيض بيتا،

${\displaystyle (\lambda x.z)\ y=z[x:=y]}$

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

${\displaystyle x\not \in \operatorname {FV} (y)}$

لذا،

${\displaystyle x\not \in \operatorname {FV} (y)\implies \operatorname {let} x:x=y\operatorname {in} z=(\lambda x.z)\ y}$

ويتم تمثيل هذه النتيجة بلغة وظيفية في شكل مختصر، حيث يكون المعنى لا لبس فيه؛

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y}$

هنا يتم التعرف ضمناً على المتغير x باعتباره جزءًا من المعادلة التي تحدد x، والمتغير في الكم الوجودي.

ينشأ التناقض إذا تم تعريف E بواسطة . في هذه الحالة، ${\displaystyle E=\neg }$

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)}$

يصبح،

${\displaystyle \operatorname {let} x:G\operatorname {in} \neg F=\neg \ (\operatorname {let} x:G\operatorname {in} F)}$

واستخدامها،

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

${\displaystyle (\exists xG\land \neg F)=\neg \ (\exists xG\land F)}$

${\displaystyle =(\exists x\neg G\lor \neg F)}$

هذا غير صحيح إذا كانت G خاطئة. لتجنب هذا التناقض، لا يُسمح لـ F بأن تكون من النوع المنطقي. بالنسبة لـ F المنطقي، يستخدم البيان الصحيح لقاعدة الإسقاط التضمين بدلاً من المساواة،

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies (\operatorname {let} x:G\operatorname {in} E\ F\to E\ (\operatorname {let} x:G\operatorname {in} F))}$

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

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

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

دع التعبيرات يمكن تعريفها بمتغيرات متعددة،

${\displaystyle (\exists v\cdots \exists w\exists xE\land F)\iff \operatorname {let} v,\ldots ,w,x:E\operatorname {in} F}$

ومن ثم يمكن اشتقاقه،

${\displaystyle x\not \in FV(E)\implies (\exists v\cdots \exists w\exists xE\land F)\iff (\exists v\cdots \exists w(E\land \exists xF))}$

لذا،

${\displaystyle x\not \in FV(E)\implies (\operatorname {let} v,\ldots ,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,\ldots ,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)}$

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

اسم	قانون
تكافؤ تخفيض إيتا	${\displaystyle f\ x=y\equiv f=\lambda x.y}$
تكافؤ لامدا-ليت	${\displaystyle f\notin FV(E)\implies (\operatorname {let} f:f=E\operatorname {in} L\equiv (\lambda f.L)\ E)}$(أين اسم المتغير.) ${\displaystyle f}$
دعونا نجمع	${\displaystyle x\notin FV(E)\implies (\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)}$

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

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

${\displaystyle (\operatorname {let} _{s}x=y\operatorname {in} z)\equiv (\lambda x.z)\ y}$

تم بعد ذلك توسيع تعريف تعبير let البسيط للسماح بالتكرار باستخدام مجموعة النقطة الثابتة .

يمكن تمثيل مركب النقطة الثابتة بالتعبير،

${\displaystyle \lambda f.\operatorname {let} x=f\ x\operatorname {in} x}$

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

${\displaystyle \lambda f.\operatorname {let} x\ x=f\ (x\ x)\operatorname {in} x\ x}$

باستخدام قاعدة تخفيض إيتا،

${\displaystyle f\ x=y\equiv f=\lambda x.y}$

يعطي،

${\displaystyle \lambda f.\operatorname {let} x=\lambda x.f\ (x\ x)\operatorname {in} x\ x}$

يمكن التعبير عن تعبير let باعتباره تجريدًا لامدا باستخدام،

${\displaystyle n\not \in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda n.L)\ E)}$

يعطي،

${\displaystyle \lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

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

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

يتم تعريف تعبير let المتكرر المسمى "let rec" باستخدام مجموعة Y لتعبيرات let المتكررة.

${\displaystyle (\operatorname {let\ rec} x=y\operatorname {in} z)\equiv (\lambda x.z)\ (Y\ (\lambda x.y))}$

يتم تعميم هذا النهج بعد ذلك لدعم التكرار المتبادل. يمكن تكوين تعبير let متبادل التكرار عن طريق إعادة ترتيب التعبير لإزالة أي شروط و. يتم تحقيق ذلك عن طريق استبدال تعريفات الوظائف المتعددة بتعريف وظيفة واحد، والذي يحدد قائمة من المتغيرات تساوي قائمة من التعبيرات. ثم يتم استخدام نسخة من مركب Y، تسمى مركب نقطة التثبيت متعدد المتغيرات Y* ^[5] لحساب النقطة الثابتة لجميع الوظائف في نفس الوقت. والنتيجة هي تنفيذ متبادل التكرار لتعبير let .

يمكن استخدام تعبير let لتمثيل قيمة هي عضو في مجموعة،

${\displaystyle \operatorname {let} x\in X\operatorname {in} x}$

في تطبيق الوظيفة، من تعبير let إلى تعبير آخر،

${\displaystyle {\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)\\&=\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y\\&=\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y\end{aligned}}}$

ولكن هناك قاعدة مختلفة تنطبق على تطبيق تعبير let على نفسه.

${\displaystyle {\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)\\&=\operatorname {let} x\in X\operatorname {in} x\ x\end{aligned}}}$

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

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

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

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

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

• سيتم استخدام الأقواس المربعة [] لتمثيل تطبيق الوظيفة في البرنامج التعريفي.
• سيتم استخدام الأحرف الكبيرة للمتغيرات في البرنامج الوصفي. تمثل الأحرف الصغيرة المتغيرات في البرنامج.
• ${\displaystyle \equiv }$سيتم استخدامها للمساواة في برنامج meta.

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

كما يتم استخدام عامل الاستبدال. ويعني التعبير استبدال كل تكرار لـ G في L بـ S وإرجاع التعبير. ويمتد التعريف المستخدم لتغطية استبدال التعبيرات، من التعريف الوارد في صفحة حساب لامدا . يجب أن تقارن مطابقة التعبيرات التعبيرات من أجل تكافؤ ألفا (إعادة تسمية المتغيرات). ${\displaystyle L[G:=S]}$

تصف القواعد التالية كيفية التحويل من تعبير lambda إلى تعبير let ، دون تغيير البنية.

1. ${\displaystyle \operatorname {de-lambda} [V]\equiv V}$
2. ${\displaystyle \operatorname {de-lambda} [M\ N]\equiv \operatorname {de-lambda} [M]\ \operatorname {de-lambda} [N]}$
3. ${\displaystyle \operatorname {de-lambda} [F=\lambda P.E]\equiv \operatorname {de-lambda} [F\ P=E]}$
4. ${\displaystyle \operatorname {de-lambda} [E=F]\equiv \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$
5. ${\displaystyle \operatorname {de-lambda} [(\lambda F.E)L]\equiv \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]}$
6. ${\displaystyle V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]\equiv \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]}$
7. ${\displaystyle V\neq W\to \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]\equiv \operatorname {let} V,W:E\land F\operatorname {in} G}$
8. ${\displaystyle \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} F]\equiv \operatorname {let} V:E\operatorname {in} F}$

القاعدة 6 تنشئ متغيرًا فريدًا V، كاسم للوظيفة.

على سبيل المثال، مجموعة Y ،

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

يتم تحويله إلى،

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p}$

قاعدة	تعبير لامدا
6	${\displaystyle \operatorname {de-lambda} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]}$ ${\displaystyle V=p,F=f,E=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]}$
4	${\displaystyle \operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p]}$ ${\displaystyle \operatorname {de-lambda} [p\ f=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle \operatorname {de-lambda} [E=F]}$ ${\displaystyle E=p\ f,F=(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$ ${\displaystyle \operatorname {de-lambda} [p\ f]=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p]}$
5	${\displaystyle \operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\operatorname {in} p]}$ ${\displaystyle \operatorname {de-lambda} [(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]}$ ${\displaystyle \operatorname {de-lambda} [(\lambda F.E)L]}$ ${\displaystyle F=x,E=f\ (x\ x),L=(\lambda x.f\ (x\ x))}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]\operatorname {in} f\ (x\ x)]}$
3	${\displaystyle \operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]\operatorname {in} f\ (x\ x)]\operatorname {in} p]}$ ${\displaystyle \operatorname {de-lambda} [x=\lambda x.f\ (x\ x)]}$ ${\displaystyle \operatorname {de-lambda} [F=\lambda P.E]}$ ${\displaystyle F=x,P=x,E=f\ (x\ x)}$ ${\displaystyle \operatorname {de-lambda} [F\ P=E]}$ ${\displaystyle \operatorname {de-lambda} [x\ x=f\ (x\ x)]}$
8	${\displaystyle \operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)]\operatorname {in} p]}$ ${\displaystyle \operatorname {let-combine} [\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)]}$ ${\displaystyle \operatorname {let-combine} [Y]}$ ${\displaystyle Y=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)}$ ${\displaystyle Y}$ ${\displaystyle \operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)}$
8	${\displaystyle \operatorname {let-combine} [\operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p]}$ ${\displaystyle \operatorname {let-combine} [Y]}$ ${\displaystyle Y=\operatorname {let} p:\operatorname {de-lambda} [p\ f=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)]\operatorname {in} p}$ ${\displaystyle Y}$ ${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p}$
4	${\displaystyle \operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let} x:\operatorname {de-lambda} [x\ x=f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p}$ ${\displaystyle \operatorname {de-lambda} [x\ x=f\ (x\ x)]}$ ${\displaystyle \operatorname {de-lambda} [E=F]}$ ${\displaystyle E=x\ x,F=f\ (x\ x)}$ ${\displaystyle \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$ ${\displaystyle \operatorname {de-lambda} [x\ x]=\operatorname {de-lambda} [f\ (x\ x)]}$
2	${\displaystyle \operatorname {let} p:\operatorname {de-lambda} [p\ f]=\operatorname {let} x:\operatorname {de-lambda} [x\ x]=\operatorname {de-lambda} [f\ (x\ x)]\operatorname {in} f\ (x\ x)\operatorname {in} p}$ ${\displaystyle \operatorname {de-lambda} [x\ x],\operatorname {de-lambda} [f\ (x\ x)]}$ ${\displaystyle \operatorname {de-lambda} [p\ f],\operatorname {de-lambda} [M_{1}\ N_{1}],\operatorname {de-lambda} [M_{2}\ N_{2}],}$ ${\displaystyle M_{1}=p,N_{1}=f,M_{2}=x,N_{2}=x,M_{3}=f,N_{3}=x\ x}$ ${\displaystyle \operatorname {de-lambda} [M_{1}]\ \operatorname {de-lambda} [N_{1}],\operatorname {de-lambda} [M_{2}]\ \operatorname {de-lambda} [N_{2}],\operatorname {de-lambda} [M_{3}]\ \operatorname {de-lambda} [N_{3}]}$ ${\displaystyle \operatorname {de-lambda} [p]\ \operatorname {de-lambda} [f],\operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x],\operatorname {de-lambda} [f]\ \operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x]}$
1	${\displaystyle \operatorname {let} p:\operatorname {de-lambda} [p]\ \operatorname {de-lambda} [f]=\operatorname {let} x:\operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x]=\operatorname {de-lambda} [f]\ (\operatorname {de-lambda} [x]\ \operatorname {de-lambda} [x])\operatorname {in} f\ (x\ x)]\operatorname {in} p}$ ${\displaystyle \operatorname {de-lambda} [V]}$ ${\displaystyle V}$
	${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ x=f\ (x\ x)\operatorname {in} f\ (x\ x)]\operatorname {in} p}$

تعكس هذه القواعد التحويل الموصوف أعلاه. فهي تحول من تعبير let إلى تعبير lambda، دون تغيير البنية. لا يمكن تحويل جميع تعبيرات let باستخدام هذه القواعد. تفترض القواعد أن التعبيرات مرتبة بالفعل كما لو كانت قد تم إنشاؤها بواسطة de-lambda .

1. ${\displaystyle \operatorname {get-lambda} [F,G\ V=E]=\operatorname {get-lambda} [F,G=\lambda V.E]}$
2. ${\displaystyle \operatorname {get-lambda} [F,F=E]=\operatorname {de-let} [E]}$
3. ${\displaystyle \operatorname {de-let} [\lambda V.E]\equiv \lambda V.\operatorname {de-let} [E]}$
4. ${\displaystyle \operatorname {de-let} [M\ N]\equiv \operatorname {de-let} [M]\ \operatorname {de-let} [N]}$
5. ${\displaystyle \operatorname {de-let} [V]\equiv V}$
6. ${\displaystyle V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} V]\equiv \operatorname {get-lambda} [V,E]}$
7. ${\displaystyle V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv (\lambda V.\operatorname {de-let} [L])\ \operatorname {get-lambda} [V,E]}$
8. ${\displaystyle W\not \in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} G]\equiv \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} \operatorname {let} W:F\ \operatorname {in} G]}$
9. ${\displaystyle V\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ V=\operatorname {get-lambda} [V,E][V:=V\ V]\ \operatorname {in} L[V:=V\ V]]}$
10. ${\displaystyle W\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ W=\operatorname {get-lambda} [V,E][V:=V\ W]\ \operatorname {in} \operatorname {let} W:F[V:=V\ W]\ \operatorname {in} L[V:=V\ W]]}$

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

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

1. lambda-form - تحويل التعبير إلى مجموعة من التعبيرات، كل منها من النموذج المتغير = expression .
   1. ${\displaystyle \operatorname {lambda-form} [G\ V=E]=\operatorname {lambda-form} [G=\lambda V.E]}$
   2. ${\displaystyle \operatorname {lambda-form} [E\land F]=\operatorname {lambda-form} [E]\land \operatorname {lambda-form} [F]}$
   3. ${\displaystyle \operatorname {lambda-form} [V=E]=V=E}$...... حيث V هو متغير.
2. lift-vars - الحصول على مجموعة المتغيرات التي تحتاج إلى X كمعلمة، لأن التعبير يحتوي على X كمتغير حر.
   1. ${\displaystyle X\in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{V\}}$
   2. ${\displaystyle X\not \in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{\}}$
   3. ${\displaystyle \operatorname {lift-vars} [X,E\land F]=\operatorname {lift-vars} [X,E]\cup \operatorname {lift-vars} [X.F]}$
3. المتغيرات الفرعية - لكل متغير في المجموعة، استبدله بالمتغير المطبق على X في التعبير. هذا يجعل X متغيرًا يتم تمريره كمعلمة، بدلاً من كونه متغيرًا حرًا في الجانب الأيمن من المعادلة.
   1. ${\displaystyle \operatorname {sub-vars} [E,\{V\}\cup S,X]=\operatorname {sub-vars} [E[V:=V\ X],S,X]}$
   2. ${\displaystyle \operatorname {sub-vars} [E,\{\},X]=E}$
4. إزالة - رفع كل شرط في E بحيث لا يكون X متغيرًا حرًا على الجانب الأيمن من المعادلة.
   1. ${\displaystyle {\begin{aligned}L&=\operatorname {lambda-form} [E]\land S=\operatorname {lift-vars} [X,L]\to \operatorname {de-let} [\operatorname {let} V\ldots W,X:E\land F\ \operatorname {in} G]\\&\equiv \operatorname {de-let} [\operatorname {let} V\ldots W:\operatorname {sub-vars} [L,S,X]\ \operatorname {in} \operatorname {let} \operatorname {sub-vars} [\operatorname {lambda-form} [F],S,X]\ \operatorname {in} \operatorname {sub-vars} [G,S,X]]\end{aligned}}}$

على سبيل المثال، تعبير let الذي تم الحصول عليه من مجموعة Y ،

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)\ \operatorname {in} p}$

يتم تحويله إلى،

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))}$

قاعدة	تعبير لامدا
6	${\displaystyle \operatorname {de-let} [\operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)\ \operatorname {in} p]}$ ${\displaystyle \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} V]}$ ${\displaystyle V=p,E=p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)}$ ${\displaystyle \operatorname {get-lambda} [V,E]}$
1	${\displaystyle \operatorname {get-lambda} [p,p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]}$ ${\displaystyle \operatorname {get-lambda} [F,G\ V=E]}$ ${\displaystyle F=p,G=p,V=f,E=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)}$ ${\displaystyle \operatorname {get-lambda} [F,G=\lambda V.E]}$
2	${\displaystyle \operatorname {get-lambda} [p,p=\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]}$ ${\displaystyle \operatorname {get-lambda} [F,F=E]}$ ${\displaystyle F=p,E=\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)}$ ${\displaystyle \operatorname {de-let} [E]}$
3	${\displaystyle \operatorname {de-let} [\lambda f.\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]}$ ${\displaystyle \operatorname {de-let} [\lambda V.E]}$ ${\displaystyle V=f,E=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)}$ ${\displaystyle \lambda V.\operatorname {de-let} [E]}$
7	${\displaystyle \lambda f.\operatorname {de-let} [\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]}$ ${\displaystyle \operatorname {de-let} [\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)]}$ ${\displaystyle V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]}$ ${\displaystyle V=x,E=x\ q=f\ (q\ q),L=f\ (x\ x)}$ ${\displaystyle (\lambda V.\operatorname {de-let} [L])\ \operatorname {get-lambda} [V,E]}$
4	${\displaystyle (\lambda x.\operatorname {de-let} [f\ (x\ x)])\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [f\ (x\ x)]}$ ${\displaystyle \operatorname {de-let} [M\ N]}$ ${\displaystyle M=f,N=(x\ x)}$ ${\displaystyle \operatorname {de-let} [M]\ \operatorname {de-let} [N]}$ ${\displaystyle \operatorname {de-let} [f]\ \operatorname {de-let} [x\ x]}$
4	${\displaystyle (\lambda x.\operatorname {de-let} [f]\ \operatorname {de-let} [x\ x])\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [x\ x]}$ ${\displaystyle \operatorname {de-let} [M\ N]}$ ${\displaystyle M=x,N=x}$ ${\displaystyle \operatorname {de-let} [M]\ \operatorname {de-let} [N]}$ ${\displaystyle \operatorname {de-let} [x]\ \operatorname {de-let} [x]}$
5	${\displaystyle (\lambda x.\operatorname {de-let} [f]\ (\operatorname {de-let} [x]\ \operatorname {de-let} [x]))\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [V]}$ ${\displaystyle V}$
1	${\displaystyle (\lambda x.f\ (x\ x))\ \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]}$ ${\displaystyle \operatorname {get-lambda} [x,x\ q=f\ (q\ q)]}$ ${\displaystyle \operatorname {get-lambda} [F,G\ V=E]}$ ${\displaystyle F=x,G=x,V=q,E=f\ (q\ q)}$ ${\displaystyle \operatorname {get-lambda} [F,G=\lambda V.E]}$ ${\displaystyle \operatorname {get-lambda} [x,x=\lambda q.f\ (q\ q)]}$
2	${\displaystyle (\lambda x.f\ (x\ x))\ \operatorname {get-lambda} [x,x=\lambda q.f\ (q\ q)]}$ ${\displaystyle \operatorname {get-lambda} [x,x=\lambda q.f\ (q\ q)]}$ ${\displaystyle \operatorname {get-lambda} [F,F=E]}$ ${\displaystyle F=x,E=\lambda q.f\ (q\ q)}$ ${\displaystyle \operatorname {de-let} [E]}$ ${\displaystyle \operatorname {de-let} [\lambda q.f\ (q\ q)]}$
3	${\displaystyle (\lambda x.f\ (x\ x))\ \operatorname {de-let} [\lambda q.f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [\lambda q.f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [\lambda V.E]}$ ${\displaystyle V=q,E=f\ (q\ q)}$ ${\displaystyle \lambda V.\operatorname {de-let} [E]}$ ${\displaystyle \lambda q.\operatorname {de-let} [f\ (q\ q)]}$
4	${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda q.\operatorname {de-let} [f\ (q\ q)])}$ ${\displaystyle \operatorname {de-let} [f\ (q\ q)]}$ ${\displaystyle \operatorname {de-let} [M_{1}\ N_{1}]}$ ${\displaystyle M_{1}=f,N_{1}=q\ q}$ ${\displaystyle \operatorname {de-let} [M_{1}]\ \operatorname {de-let} [N_{1}]}$ ${\displaystyle \operatorname {de-let} [f]\ \operatorname {de-let} [q\ q]}$ ${\displaystyle \operatorname {de-let} [M_{2}\ N_{2}]}$ ${\displaystyle M_{2}=q,N_{2}=q}$ ${\displaystyle \operatorname {de-let} [q]\ \operatorname {de-let} [q]}$
5	${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda q.\operatorname {de-let} [f]\ (\operatorname {de-let} [q]\ \operatorname {de-let} [q]))}$ ${\displaystyle \operatorname {de-let} [V]}$ ${\displaystyle }$ ${\displaystyle V}$
	${\displaystyle (\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))}$

للحصول على مثال ثانٍ، خذ النسخة المرفوعة من مُركب Y ،

${\displaystyle \operatorname {let} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p}$

يتم تحويله إلى،

${\displaystyle (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)}$

قاعدة	تعبير لامدا
8	${\displaystyle \operatorname {de-let} [\operatorname {let} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p]}$
7	${\displaystyle \operatorname {de-let} [\operatorname {let} p:p\ f\ x=f\ (x\ x)\ \operatorname {in} \operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p]}$
1, 2	${\displaystyle (\lambda p.\operatorname {de-let} [\operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p])\ \operatorname {get-lambda} [p,p\ f\ x=f\ (x\ x)]}$
7، 4، 5	${\displaystyle (\lambda p.\operatorname {de-let} [\operatorname {let} q:q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p])\ \lambda f.\lambda x.f\ (x\ x)}$
1, 2	${\displaystyle (\lambda p.(\lambda q.q\ p)\ \operatorname {get-lambda} [q,q\ p\ f=(p\ f)\ (p\ f)])\ \lambda f.\lambda x.f\ (x\ x)}$
	${\displaystyle (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)}$

وللحصول على مثال ثالث، فإن ترجمة،

${\displaystyle \operatorname {let} x:x\ f=f\ (x\ f)\ \operatorname {in} x}$

يكون،

${\displaystyle (\lambda x.x\ x)\ (\lambda x.\lambda f.f\ (x\ x\ f))}$

قاعدة	تعبير لامدا
9	${\displaystyle \operatorname {let} x:x\ f=f\ (x\ f)\ \operatorname {in} x}$
1	${\displaystyle \operatorname {let} x:x\ x=\operatorname {get-lambda} [x,x\ f=f\ (x\ f)][x:=x\ x]\ \operatorname {in} x[x:=x\ x]}$
2	${\displaystyle \operatorname {let} x:x\ x=\operatorname {get-lambda} [x,x=\lambda f.f\ (x\ f)][x:=x\ x]\ \operatorname {in} x\ x}$
	${\displaystyle \operatorname {let} x:x\ x=(\lambda f.f\ (x\ f))[x:=x\ x]\ \operatorname {in} x\ x}$
7	${\displaystyle \operatorname {let} x:x\ x=\lambda f.f\ (x\ x\ f)\ \operatorname {in} x\ x}$
1	${\displaystyle (\lambda x.x\ x)\ \operatorname {get-lambda} [x,x\ x=\lambda f.f\ (x\ x\ f)]}$
2	${\displaystyle (\lambda x.x\ x)\ \operatorname {get-lambda} [x,x=\lambda x.\lambda f.f\ (x\ x\ f)]}$
	${\displaystyle (\lambda x.x\ x)\ (\lambda x.\lambda f.f\ (x\ x\ f))}$

على سبيل المثال الرابع، ترجمة،

${\displaystyle \operatorname {let} x:x=f\ x\ \operatorname {in} x}$

يكون،

${\displaystyle (\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

وهو المركب y الشهير .

قاعدة	تعبير لامدا
9	${\displaystyle \operatorname {let} x:x=f\ x\ \operatorname {in} x}$
2	${\displaystyle \operatorname {let} x:x\ x=\operatorname {get-lambda} [x,x=f\ x][x:=x\ x]\ \operatorname {in} x[x:=x\ x]}$
	${\displaystyle \operatorname {let} x:x\ x=(f\ x)[x:=x\ x]\ \operatorname {in} x\ x}$
7	${\displaystyle \operatorname {let} x:x\ x=f\ (x\ x)\ \operatorname {in} x\ x}$
1	${\displaystyle (\lambda x.x\ x)\ \operatorname {get-lambda} [x,x\ x=f\ (x\ x)]}$
2	${\displaystyle (\lambda x.x\ x)\ \operatorname {get-lambda} [x,x=\lambda x.f\ (x\ x)]}$
	${\displaystyle (\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

• دانا سكوت

• النطاق (علوم الكمبيوتر)
• رفع لامدا
• مُجمِّع النقطة الثابتة
• حساب لامدا
• مفارقة كاري
• حساب لامدا الاستنتاجي
• برمجة المنطق المقيد
• تضييق مجموعات القيم الجبرية

• ميتشل، جون سي. (1996). أساسيات لغات البرمجة. مطبعة معهد ماساتشوستس للتكنولوجيا. رقم ISBN 978-0-262-13321-0.
• بلوتكين، جي دي (ديسمبر 1977). "LCF تعتبر لغة برمجة". علوم الكمبيوتر النظرية . 5 (3): 223-255. doi : 10.1016/0304-3975(77)90044-5 .