حساب التفاضل والتكامل Lambda هو نظام رسمي في المنطق الرياضي للتعبير عن الحسابات القائمة على التجريد وتطبيق الوظائف باستخدام الاستبدال المتغير والربط. هذا نموذج عالمي يمكن تطبيقه على تصميم أي آلة تورينج. تم تقديم حساب لامدا لأول مرة من قبل تشيرش ، عالم رياضيات مشهور ، في ثلاثينيات القرن الماضي.
يتكون النظام من بناء أعضاء لامدا وإجراء عمليات تصغير عليهم.
شروحات وتطبيقات
يستخدم الحرف اليوناني لامدا (λ) في تعبيرات لامدا ومصطلحات لامدا للدلالة على ارتباط متغير في دالة.
حساب التفاضل والتكامل Lambda يمكن كتابته أو كتابته. في المتغير الأول ، لا يمكن استخدام الوظائف إلا إذا كانت قادرة على استقبال بيانات من هذا النوع. حسابات لامدا المصنّعة أضعف ، يمكنها التعبير عن قيمة أصغر. لكن ، من ناحية أخرى ، تسمح لك بإثبات المزيد من الأشياء.
أحد أسباب وجود العديد من الأنواع المختلفة هو رغبة العلماء في بذل المزيد من الجهد دون التخلي عن فرصة إثبات نظريات لامدا التفاضلية القوية.
للنظام تطبيقات في العديد من المجالات المختلفة للرياضيات والفلسفة واللغويات وعلوم الكمبيوتر. بادئ ذي بدء ، حساب لامدا هو حساب التفاضل والتكامل الذي لعب دورًا مهمًا في تطوير نظرية لغات البرمجة. إنها أنماط الخلق الوظيفي التي تنفذها الأنظمة. كما أنها موضوع بحث ساخن في نظرية هذه الفئات
للدمى
تم تقديم حساب لامدا من قبل عالم الرياضيات ألونزو تشيرش في ثلاثينيات القرن الماضي كجزء من بحثه في أسس العلم. تبين أن النظام الأصلي غير متسق منطقيًا في عام 1935 عندما طور ستيفن كلاين وجي بي روسر مفارقة كلاين روسر.
لاحقًا ، في عام 1936 ، خص تشرش ونشر الجزء المتعلق بالحسابات فقط ، وهو ما يسمى الآن بحساب لامدا غير المصنف. في عام 1940 قدم أيضًا نظرية أضعف ولكنها متسقة منطقيًا تعرف باسم نظام النوع الأولي. في عمله ، يشرح النظرية بأكملها بعبارات بسيطة ، لذلك يمكن القول أن تشرش نشر حساب لامدا التفاضل والتكامل للدمى.
حتى الستينيات ، عندما أصبحت علاقتها بلغات البرمجة واضحة ، كانت λ مجرد شكلية. بفضل تطبيقات ريتشارد مونتاجو ولغويين آخرين في دلالات اللغة الطبيعية ، احتل حساب التفاضل والتكامل مكان الصدارة في كل من علم اللغة وعلوم الكمبيوتر.
أصل الرمز
Lambda لا تعني كلمة أو اختصار ، إنها تأتي من مرجع في الرياضيات الأساسية لراسل متبوعًا بتغييرين مطبعيين. مثال على الترميز: بالنسبة للدالة f مع f (y)=2y + 1 هي 2ŷ + 1. وهنا نستخدم علامة الإقحام (“hat”) فوق y لتسمية متغير الإدخال.
قصدت الكنيسة في الأصل استخدام رموز مماثلة ، لكن الناضدين لم يتمكنوا من وضع رمز "القبعة" فوق الحروف. لذا بدلاً من ذلك قاموا بطباعته في الأصل كـ "/\y.2y+1". في الحلقة التالية من التحرير ، استبدل الطباعون "/ \" بشخصية متشابهة بصريًا.
مقدمة لحساب لامدا
يتكون النظام من لغة المصطلحات ، التي يتم اختيارها من خلال بناء جملة رسمي معين ، ومجموعة من قواعد التحويل التي تسمح بمعالجتها. يمكن اعتبار النقطة الأخيرة كنظرية معادلة أو تعريف تشغيلي.
جميع الوظائف في حساب لامدا هي مجهولة الهوية ، مما يعني أنه ليس لديها أسماء. يأخذون متغير إدخال واحد فقط ، ويتم استخدام الكاري لتنفيذ قطع ذات متغيرات متعددة.
شروط لامدا
يعرف تركيب التفاضل والتكامل بعض التعبيرات على أنها صالحة والبعض الآخر غير صالح. تمامًا مثل سلاسل الأحرف المختلفة هي برامج C صالحة وبعضها ليس كذلك. يسمى التعبير الفعلي لحساب لامدا "مصطلح لامدا".
توفر القواعد الثلاثة التالية تعريفًا استقرائيًا يمكن أن يكونتنطبق على بناء جميع المفاهيم الصالحة نحويًا:
المتغير x نفسه هو مصطلح لامدا صالح:
- إذا كانت T تساوي LT و x غير ثابتة ، فإن (lambda xt) تسمى تجريدًا.
- إذا كانت T بالإضافة إلى s هي مفاهيم ، فإن (TS) يسمى تطبيق.
لا شيء آخر هو مصطلح لامدا. وبالتالي ، يكون المفهوم صالحًا إذا وفقط إذا أمكن الحصول عليه من خلال التطبيق المتكرر لهذه القواعد الثلاثة. ومع ذلك ، قد يتم حذف بعض الأقواس وفقًا لمعايير أخرى.
التعريف
تتكون تعبيرات لامدا من:
- المتغيرات v 1، v 2،…، v n،…
- رموز التجريد 'λ' والنقطة '.'
- أقواس ().
المجموعة Λ يمكن تعريفها حثيًا:
- إذا كانت x متغيرًا ، إذن x ∈ Λ ؛
- س ليست ثابتة و M ∈ Λ ، ثم (λx. M) ∈ Λ ؛
- M ، N ∈ Λ ، ثم (MN) ∈ Λ.
التعيين
للحفاظ على تدوين تعبيرات لامدا منظمة ، يتم استخدام الاصطلاحات التالية بشكل شائع:
- الأقواس الخارجية تم حذفها: MN بدلاً من (MN).
- من المفترض أن تظل التطبيقات مرتبطة: يمكن للمرء كتابة MNP بدلاً من ((MN) P).
- يمتد جسم التجريد إلى اليمين: λx. MN تعني λx. (MN) ، وليس (x. M) N.
- يتم تقليل تسلسل التجريدات: λx.λy.λz. N يمكن أن تكون λxyz. N.
المتغيرات الحرة والمحددة
المشغل λ يربط غير ثابت أينما كان في جسم التجريد. المتغيرات التي تقع في النطاق تسمى ملزمة. في التعبير λ x. م ، غالبًا ما يُشار إلى الجزء x باسم الموثق. كما لو كان التلميح إلى أن المتغيرات تصبح مجموعة مع إضافة X x إلى M. جميع المتغيرات الأخرى غير المستقرة تسمى حرة.
على سبيل المثال ، في التعبير λ y. x x y و y - غير دائم و x مجاني. وتجدر الإشارة أيضًا إلى أن المتغير يتم تجميعه حسب تجريده "الأقرب". في المثال التالي ، يتم تمثيل حل حساب التفاضل والتكامل lambda من خلال تكرار واحد لـ x ، والذي يرتبط بالمصطلح الثاني:
λ x. y (λ x. z x)
مجموعة المتغيرات الحرة M يشار إليها على أنها FV (M) ويتم تعريفها بالعودة على هيكل المصطلحات على النحو التالي:
- FV (x)={x} ، حيث x متغير.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
الصيغة التي لا تحتوي على متغيرات حرة تسمى مغلقة. تُعرف تعبيرات لامدا المغلقة أيضًا بالمُجمعات وتعادل المصطلحات في المنطق التوافقي.
اختصار
يتم تحديد معنى تعبيرات لامدا من خلال كيفية تقصيرها.
هناك ثلاثة أنواع من التخفيضات:
- تحويل α: تغيير المتغيرات المرتبطة (ألفا).
- β-Red: تطبيق الدوال على وسيطاتها (تجريبي).
- η-transform: يغطي مفهوم الامتداد.
هنا أيضًانحن نتحدث عن التكافؤات الناتجة: تعبيران مكافئان لـ إذا كان من الممكن تحويلهما إلى نفس المكون ، ويتم تعريف التكافؤ α / بالمثل.
يشير مصطلح redex ، وهو اختصار لدوران قابل للاختزال ، إلى الموضوعات الفرعية التي يمكن تقليلها بإحدى القواعد. حساب لامدا للدمى ، أمثلة:
(λ x. M) N هو نسخة تجريبية من redex في التعبير لاستبدال N بـ x في M. يُطلق على المكون الذي يقلل redex إليه اختزاله. الاختزال (λ x. M) N هو M [x:=N].
إذا لم تكن x حرة في M ، λ x. M x أيضًا em-REDEX مع منظم M.
α- التحول
تسمح لك عمليات إعادة تسمية Alpha بتغيير أسماء المتغيرات المرتبطة. على سبيل المثال ، x. يمكن أن تعطي x λ y. ذ. يُقال أن المصطلحات التي تختلف فقط في تحويل ألفا هي مكافئة لـ α. في كثير من الأحيان ، عند استخدام حساب لامدا ، تعتبر مكافئات ألفا متبادلة.
القواعد الدقيقة لتحويل ألفا ليست تافهة تمامًا. أولاً ، مع هذا التجريد ، تتم إعادة تسمية المتغيرات المرتبطة بالنظام نفسه فقط. على سبيل المثال ، تحويل ألفا λ x.λ x. يمكن أن تؤدي x إلى λ y.λ x. x ، ولكن هذا قد لا يؤدي إلى λy.λx.y الأخير له معنى مختلف عن الأصل. هذا مشابه لمفهوم برمجة التظليل المتغير.
ثانيًا ، لا يكون تحويل ألفا ممكنًا إذا كان سيؤدي إلى التقاطه بواسطة تجريد آخر غير دائم. على سبيل المثال ، إذا استبدلت x بـ y في λ x.λ y. x ، ثم يمكنك الحصول عليهاλy.λy. ش ، وهي ليست هي نفسها على الإطلاق.
في لغات البرمجة ذات النطاق الثابت ، يمكن استخدام تحويل ألفا لتبسيط تحليل الاسم. في نفس الوقت ، مع الحرص على أن مفهوم المتغير لا يخفي التعيين في المنطقة المحتوية.
في تدوين فهرس De Bruyne ، أي مصطلحين مكافئين ألفا متطابقان من الناحية التركيبية.
استبدال
التغييرات المكتوبة بواسطة E [V:=R] هي عملية استبدال جميع التكرارات الحرة للمتغير V في التعبير E مع معدل الدوران R. حساب التفاضل والتكامل على هيكل المفهوم على النحو التالي (ملاحظة: x و y - المتغيرات فقط ، و M و N - أي تعبير λ).
x [x:=N] ≡ N
y [x:=N] ≡ y إذا كان x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) إذا x ≠ y بشرط أن y ∉ FV (N).
للاستبدال في تجريد لامدا ، في بعض الأحيان يكون من الضروري تحويل α لتعبير. على سبيل المثال ، ليس صحيحًا أن (λ x. Y) [y:=x] ينتج عنها (λ x. X) لأن x البديل كان يجب أن يكون مجانيًا ، ولكن انتهى به الأمر إلى تقييده. الاستبدال الصحيح في هذه الحالة هو (λ z. X) حتى α- التكافؤ. لاحظ أن الاستبدال محدد بشكل فريد حتى لامدا.
β تخفيض
تخفيض بيتا يعكس فكرة تطبيق وظيفة. يتم تعريف اختزال بيتا من حيثالاستبدال: ((X V. E) E ') هو E [V:=E'].
على سبيل المثال ، بافتراض بعض الترميز 2 ، 7 ، × ، هناك تخفيض β التالي: ((λ n. N × 2) 7) → 7 × 2.
يمكن النظر إلى تقليل بيتا على أنه نفس مفهوم الاختزال المحلي في ظل الاستنتاج الطبيعي عبر تماثل Curry-Howard.
η- تحويل
يعبر هذا التحويل عن فكرة التمدد ، والتي في هذا السياق هي أن وظيفتين متساويتين عندما يعطيان نفس النتيجة لجميع الوسائط. هذا التحويل يتبادل بين λ x. (F x) و f عندما لا يبدو x مجانيًا في f.
يمكن اعتبار هذا الإجراء على أنه نفس مفهوم الاكتمال المحلي في الاستنتاج الطبيعي من خلال تماثل Curry-Howard.
الأشكال العادية والانصهار
بالنسبة لحساب لامدا غير النمطي ، فإن قاعدة التخفيض β ليست بشكل عام تطبيع قوي ولا ضعيف.
ومع ذلك ، يمكن إثبات أن تقليل β يندمج عند التشغيل قبل تحويل α (على سبيل المثال ، يمكن اعتبار شكلين عاديين متساويين إذا كان التحويل α من أحدهما إلى الآخر ممكنًا).
لذلك ، فإن كلا من المصطلحات التطبيعية القوية والمصطلحات المعدلة بشكل ضعيف لها شكل عادي واحد. بالنسبة للشروط الأولى ، فإن أي استراتيجية تخفيض مضمونة لتؤدي إلى تكوين نموذجي. بينما لظروف التطبيع الضعيف ، قد لا تجدها بعض استراتيجيات التخفيض.
طرق البرمجة الإضافية
هناك الكثير من مصطلحات الإنشاء لحساب لامدا. تم تطوير العديد منها في الأصل في سياق استخدام الأنظمة كأساس لدلالات لغة البرمجة ، وتطبيقها بشكل فعال على أنها بناء منخفض المستوى. نظرًا لأن بعض الأنماط تتضمن حساب لامدا (أو شيء مشابه جدًا) كمقتطف ، فإن هذه الأساليب تجد استخدامها أيضًا في الإنشاء العملي ، ولكن قد يُنظر إليها بعد ذلك على أنها غامضة أو أجنبية.
الثوابت المسماة
في حساب التفاضل والتكامل lambda ، تأخذ المكتبة شكل مجموعة من الوظائف المحددة مسبقًا ، حيث تكون المصطلحات مجرد ثوابت ملموسة. لا يحتوي حساب التفاضل والتكامل النقي على مفهوم للمتغيرات المسماة لأن جميع مصطلحات لامدا الذرية هي متغيرات. ولكن يمكن تقليدها أيضًا من خلال أخذ المتغير كاسم للثابت ، واستخدام تجريد لامدا لربط هذا المتطاير في الجسم ، وتطبيق هذا التجريد على التعريف المقصود. لذا إذا استخدمت f لتمثيل M في N ، فيمكنك قول
(λ f. N) M.
غالبًا ما يقدم المؤلفون مفهومًا نحويًا مثل السماح لكتابة الأشياء بطريقة أكثر سهولة.
f=M إلى N
من خلال تسلسل هذه التعريفات ، يمكن للمرء كتابة "برنامج" حساب لامدا على أنه صفر أو أكثر من تعريفات الوظائف متبوعًا بعضو لامدا واحد ، باستخدام تلك التعريفات التي تشكل الجزء الأكبر من البرنامج.
أحد القيود الملحوظة لهذا السماح هو أن الاسم f لم يتم تعريفه في M ،بما أن M خارج النطاق الملزم لتجريد lambda f. هذا يعني أنه لا يمكن استخدام سمة دالة تكرارية كـ M مع let. بناء جملة letrec الأكثر تقدمًا ، والذي يسمح لك بكتابة تعريفات دالة تكرارية في هذا النمط ، بالإضافة إلى استخدام مُجمِّعات النقطة الثابتة بدلاً من ذلك.
نظائرها المطبوعة
هذا النوع عبارة عن شكليات مكتوبة تستخدم رمزًا لتمثيل تجريد دالة مجهولة. في هذا السياق ، عادةً ما تكون الأنواع كائنات ذات طبيعة نحوية يتم تخصيصها لمصطلحات لامدا. تعتمد الطبيعة الدقيقة على حساب التفاضل والتكامل المعني. من وجهة نظر معينة ، يمكن اعتبار LI المكتوب تحسينات لـ LI غير المكتوب. ولكن من ناحية أخرى ، يمكن اعتبارها أيضًا نظرية أكثر جوهرية ، وحساب لامدا غير المصنف هو حالة خاصة بنوع واحد فقط.
Typed LI هي أساس لغات البرمجة والعمود الفقري للغات الوظيفية مثل ML و Haskell. وبشكل غير مباشر أكثر ، أساليب الخلق الحتمية. تلعب حسابات لامدا المكتوبة دورًا مهمًا في تطوير أنظمة الكتابة للغات البرمجة. هنا ، عادةً ما تلتقط القابلية للطباعة الخصائص المطلوبة للبرنامج ، على سبيل المثال ، لن تتسبب في انتهاك الوصول إلى الذاكرة.
ترتبط حسابات لامدا المطبوعة ارتباطًا وثيقًا بالمنطق الرياضي ونظرية الإثبات من خلال تماثل كاري-هوارد ، ويمكن اعتبارها لغة داخلية لفئات الفئات ، على سبيل المثال ، والتيببساطة هو أسلوب الإغلاق الديكارتي.
