تكامل لامدا

من أرابيكا، الموسوعة الحرة
اذهب إلى التنقل اذهب إلى البحث
تكامل لامدا

تعديل - تعديل مصدريحول القالب

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

قبل التطرق إلى كيفية تركيب وتأليف العبارات السليمة التركيب لحدود لامبدا يتعين بدءً الحديث عن الأسباب الكامنة خلف ابداع حساب لامبدا ؟ لاحظ تشورش أنه عندما نمثل دالة بصيغة رياضية مثل x+y فإن الصيغة يعتورها الغموض والابهام، فهذه العبارة قد تدل على أكثر من معنى مثل:

1.     قد تدل العبارة x+y على عدد، حيث تشير x و y إلى عددين محددين.

2.     قد تدل كذلك على دالة معرفة بما يلي :   f :x⟼x+y  تُقرن كل عدد x من مجموعة الانطلاق بعددx+y   و y قيمة محددة سابقا.

3.     قد تدل على دالة أخرى معرفة بــ   g :y⟼x+y حيث تحول كل عدد y إلى قيمة x+y حيث x قيمة محددة سابقا.

4.     قد تدل على دالة بمتغيرين  :   h :x,y⟼x+y، هذه الدالة تأخذ موضوعين ثم تعطينا قيمة x+y.

هذه الصيغة كما تبين يمكن أن تكون مصدر  إبهام وغموض كبيرين لذلك اقترح تشورش ترميزا يساعد الرياضيين على رفع هذا الغموض مميزا بين المتغيرات التي تستعمل كمواضيع وبين المتغيرات التي تستعمل كقيم معرفة مسبقا.في هذا الترميز يكون المتغير المسبوق بالحرف اليوناني لامبدا λ  هو الموضوع. مثلا المعنى الثاني للعبارة f :x⟼x+y نرمز له بالرمز  x.x+yλ ، حيث x متغير وy عدد نعرفه مسبقا، في ضوء ذلك نرمز العبارات السابقة على الشكل الآتي:[2]

1.    نكتب العدد x+y على الشكل الآتي  x+y .

2.    نرمز الدالة  f :x⟼x+y   على الشكل الآتي: λx.x+y

3.    نرمز الدالة g :y⟼x+y على الصورة الآتية:  λy.x+y

4.    نرمز الدالة h :x,y⟼x+y على الصورة الآتية:  λxy.x+y

جرت عادة المناطقة في مستهل حديثهم عن الأنساق المنطقية تحديد العبارات السليمة التركيب وطريقة إنشائها، كذلك في نسق حساب لامبدا يتوجب بدءً تعريف الحدود المقبولة أو الجائز استعمالها في الحساب، والتي تسمى بحدود لامبدا  term-λ، سنتعرف على نوعين من العبارات : مجموعة من المتغيرات x،y،z... ومجموعة من الثوابت الذرية،  ننشئ عبارة مقبولة من حدود لامبدا تكراريا على الشكل الآتي:

جرت عادة المناطقة في مستهل حديثهم عن الأنساق المنطقية تحديد العبارات السليمة التركيب وطريقة إنشائها، كذلك في نسق حساب لامبدا يتوجب بدءً تعريف الحدود المقبولة أو الجائز استعمالها في الحساب، والتي تسمى بحدود لامبدا  term-λ ، سنتعرف على نوعين من العبارات: مجموعة من المتغيرات x،y،z... ومجموعة من الثوابت الذرية،  ننشئ عبارة مقبولة من حدود لامبدا تكراريا على الشكل الآتي:

  1. إذا كان x متغير فهو ينتمي إلى حدود لامبدا.
  2. إذا كان M و N حدين من حدود لامبدا فإن (MN) حد لامبدا، يسمى هذا التركيب بالتطبيق
  3. إذا كان M حد لامبدا و x متغير فإن التركيب λx.M هو حد لامبدا، تسمى هذه العملية بالتجريد.[3]

سنستعين بهاتين العمليتين في توليد الحدود الآتية: (λx.xy)، (λx.λy.xz), ((λz.z)(λxy.x))

توجد في حساب لانمبدا عمليات حساب الحدود تعرف بعمليات اختزال الحدود وتتضمن:

العملية اسم العملية الوصف 
(λx.M[x]) →(λy.M[y])
 تحويل ألفا تعيد تسمية المتغيرات المقيدة في العبارة، تجنبا لتصادم الأسماء 
((λx.M)E) →(M[x := E])
 تحويل بيطا يستبدل المتغيرات المقيدة بالمواضيع في جسم التجريد

الشرح والتطبيقات

حساب لامدا هو تورنغ كاملة وهو نموذج عام من الحوسبة والتي يمكن استخدامها لمحاكاة أي آلة تورنغ ذات شريط واحد. تحمل الاسم الحرف اليوناني لامدا (λ)، ويستخدم في تعبيرات لامدا وشروط لامدا لاسناد متغير في الوظيفة أو التابع.

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

حساب لامدا له تطبيقات في مجالات مختلفة في الرياضيات، الفلسفة، [4] اللسانيات، [5][6] وعلم الحاسوب.[7] وقد لعب حساب لامدا دورا هاما في تطوير نظرية لغات البرمجة. تطبق لغات البرمجة الوظيفية حساب لامدا. حساب لامدا أيضا هو موضوع البحث الحالي في نظرية الأصناف.[8]

المتغيرات الحرة والمقيدة

يتعين في البداية معرفة نطاق العامل λx  في عبارة لامبدا، سنستعين على ذلك بالمثال الآتي، لنعتبر الحد P

P=(λy.yx(λx.y(λy.z)x))vw

نطاق العامل λy الذي يوجد في أقصى اليسار هو العبارة yx(λx.y(λy.z)x ، ونطاق λx هوy(λy.z)x ، أما نطاق العامل λy الذي يوجد على اليمين هو z .

تعريف: يكون المتغير x في P مقيدا إذا كان يوجد في نطاق λx وإلا سُمي حرا.

مجموعة المتغيرات الحرة في P  يرمز لها بالرمز:  FV(P)، والحد المغلوق هو الحد الذي لا يتضمن أي متغير حر.

تعريف: نعرف مجموعة المتغيرات الحرة تكراريا على الشكل الآتي:

FV(x)={x}

FV(λx.M)=FV(M)-{x}

FV(MN)=FV(M) ∪ FV(N)

تكون M مغلوقة أو دالة توافقية  إذا كان FV(M)= ∅ ، نرمز لمجموعة الحدود المغلوقة بالرمز 0Λ مثال: لتعتبر الحد الآتي:    xv(λy.(λz.yv)w  ، بوضع الأقواس سنحصل على العبارة المقوسة الآتية:

P=(((xv)(λy.(λz.(yv)))w)  

المتغيرات الحرة في P هي  x و v و w أما y فهو متغير مقيد، العامل λx له نفس دور السور x∀ في منطق المحمولات.

ما هي المتغيرات الحرة في  M=x(λy.xy) ؟ المتغير x يرد حرا مرتين، بينما المتغير y فهو مقيد، لذلك نكتب: FV(M)={x} ، قد يرد أحيانا المتغير حرا ومقيدا مثل العبارة: y(λy.y).

الاستبدال في حساب لامبدا[9]

نعرف على حدود لامبدا عملية الاستبدال التي نرمز لها بالرمز: M[x :=N]   ، وتشير إلى تعويض المتغير الحر x في M بــ N .

أمثلة: سنقوم بتطبيق التجريد λx.x(xy)) على N ونرى كيف تتم عملية الاستبدال، بداية سنقوم بالبحث عن المتغيرات الحرة x في الحد x(xy)  بعد ذلك سنقوم باحلال N مكان هذه المتغيرات الحرة:

(λx.x(xy))N= (λx.x(xy))[x :=N]= N(Ny)

·      الدالة λx.y تمثل الدالة الثابتة  تأخذ القيمة y مهما يكن الموضوع x ، لأنه عندما نطبقها على N تنتج y:

(λx.y)N  =(λx.y)[x :=N]=  y

·      الدالة λx.x تمثل دالة المطابقة تأخذ الموضوع x ثم تعطي نفس الموضوع x :

(λx.x)N   = (λx.x) [x :=N]=  N

يسمى هذا التحويل الذي نقلنا من الصيغة (λx.x)N    إلى الصيغة  [x :=N](λx.x) حيث أحللنا N مكان x بتحويل بيطا أو اختزال بيطا، الصيغة الأولى  N(λx.x)   تسمى العبارة القابلة  للاختزال β-redex ، بينما الصيغة الثانية تسمى بالصيغة المختزلة أو المقلصة. سنرمز لهذا التحويل بالرمز ⊳β الصيغة المختصرة تكون على الشكل (λx.A)M إذا طبقنا اختزال-بيطا  على هذه الصيغة القابلة للاختزال ستتحول إلى الصيغة:

(λx.A)M  ⊳β  A[x :=M]

حيث حل M محل x في الحد A .

عملية الاستبدال في الحدود أحيانا لا تسير وفق الخطة التي شرحناها سابقا، أحيانا الاستبدالات قد تفضي إلى مفارقات، لنتأمل في المثال الآتي:

مثال: لنأخذ  F≡λxy.yx ونطبقها على M وN:

FMN ⊳β  ((λx.(λy.yx) M)N ⊳β  (λy.yM)N ⊳β  NM

هذه العملية كما رأينا تعكس ترتيب الحدود، إذا طبقنا F على yx من المنتظر أن نحصل على  Fyx=xy لكن الأمر ليس كذلك:

Fyx=((λx.(λy.yx))y)x ⊳β  (λy.yy)x=xx

وبالتالي فإن xy=xx وهذا تناقض، من هذه العبارة يمكن أن نشتق أي شيء، لذلك لابد من قواعد تضبط عملية الاستبدال تجنبنا الوقوع في هذه المفارقات، السؤال أين الخلل في التحويل السابق؟ نشأ الخلل في المرحلة:

( λx.(λy.yx) )y=λy.yy

المتغير الحر y أصبح مقيدا بعد أن قمنا بعملية استبداله بــ x في λy.yx  ، وذلك غير مسموح به.

إذن لابد من وضع قاعدة تحول دون أن يفضي تحويل الحدود إلى مفارقات، لأجل ذلك سنعرف تحويلا آخر، إلى جانب  تحويل بيطا، سنسميه  بتحويل ألفا α-conversion سنرمز لهذا التحويل بالرمز  ⊳α. يسعى تحويل-ألفا إلى إعادة تسمية المتغيرات المقيدة.[10]

مثال: 

λx.xy ⊳α  λz.zy

سنطبق تحويل ألفا على المثال السابق:

λxy.yx ⊳α  λwy.yw ⊳α  λwz.zw

الآن، بعد إجراء تحويل ألفا نكون في وضعية إجراء تحويل بيطا على الشكل الآتي:

Fyx=((λw.(λz.zw))y)x ⊳β (λz.zy)x   ⊳β  xy

عموما يجب الالتزام بالقواعد الآتية في عملية الاستبدال: 

	x[x :=N]   ≡  N
 
	a[a :=N]   ≡  a
 بالنسبة لجميع الذرات حيث إن a≠x 
    (PQ) [x :=N] ≡ P[x :=N] Q[x :=N]
 
	(λx.P) [x :=N]  ≡ λx.P
 
	(λy.P) [x :=N]  ≡ λy.P
 إذا كانت x لا تنتمي إلى المتغيرات الحرة في P

x∉FV(P) 

	(λy.P) [x :=N]  ≡ λy. [x :=N]P
إذا كانت x تنتمي إلى المتغيرات الحرة لـP وy لا تنتمي إلى المتغيرات الحرة لــ N

x∈FV(P) و  y∉FV(P)

  (λy.P) [x :=N]  ≡ λz. [x :=N][y :=z]P إذا كانت x تنتمي إلى المتغيرات الحرة لــ P وy تنتمي إلى المتغيرات الحرة لــ N .

x∈FV(P) و  y∈FV(P)

أمثلة

سنجري مجموعة من الاستبدالات على الحدود الآتية:

(λy.x(λw.vwx))[x :=uv] ⊳α  (λy.(uv)(λw.vw(uv)))	
(λy.x(λx. x))[x :=λy.xy] ⊳α   (λy.x(λz. z))[x :=λy.xy] ≡λy. λy.xy(λz. z)	
(y(λv.xv))[x :=λy.vy] ⊳α  (y(λz.xz))[x :=λy.vy] ≡ y(λz.( λy.vy)z)

تحويل بيطا[11]

موضوع هذا المحور هو طريقة حساب حدود لامبدا، رأينا سابقا أن الصيغة القابلة للاختزال تكون على الصورة (λx.A)M ، إذا طبقنا اختزال-بيطا  على هذه الصيغة ستتحول إلى الصيغة المقلصة:

(λx.A)M  ⊳β  A[x :=M]

حيث حل M محل المتغير الحر  x في الحد A ، عموما إذا تضمن الحد P الصيغة القابلة للاختزال  (λx.A)M ثم استبدلنا  هذه الصيغة الأخيرة بــ A[x :=M] فحصلنا على  حد جديد P' ، نقول حينئد أننا اختزلنا P إلى P’ ، ونكتب:

P  ⊳β  P'

إذا قمنا بتغيير P إلى Q بعد سلسلة من التقليصات وإعادة تسمية المتغيرات المقيدة، نقول أننا قمنا باختزال-بيطا P إلى Q فنكتب:

P ⊳β  Q

مثال

a)	(λx.x(xy))N      ⊳β   N(Ny)
b)	(λx.y)N          ⊳β   y
c)	(λx.(λy.yx)z)v   ⊳β   (λy.yx)z)[x :=v] ≡ (λy.yv)z  ⊳β   yv[y :=z] ≡ zv
d)	(λx.xx) (λx.xx)  ⊳β   (λx.xx)[x := λx.xx] ≡ (λx.xx) (λx.xx)  
                     ⊳β   (λx.xx)[x := λx.xx] ≡ (λx.xx) (λx.xx)
                            …..  
e)	(λx.xxy)(λx.xxy)  ⊳β    (λx.xxy)(λx.xxy) y
                      ⊳β    (λx.xxy)(λx.xxy) yy
                              …..

سنحاول التمييز بين نوعين من الاختزالات اختزال بخطوة وحيدة واختزال بعد سلسلة من الاختزالات:

تعريف 20 : (الاختزال بخطوة وحيدة ⊳β1 )  نقول أن A تختزل بخطوة وحيدة إلى B (نرمز لها بالرمز A  ⊳β1  B)  في حالة ما تضمن الحد A جزءَ C=(λx.M)N  ، ولا تختلف A عن B  إلا بكون الجزء C مستبدل في B بالجزء المقلص  M[x :=N]

في المثال السابق  b  الحد (λx.y)N   مختزل بخطوة وحيدة إلى y نكتب:   

(λx.y)N  ⊳β1   y

كذلك a مختزلة بخطوة وحيدة:

(λx.x(xy))N  ⊳β1   N(Ny)

تعريف 21  : سلسلة الاختزالات من حد A إلى الحد B هي سلسلة متناهية من الحدود s1….sn تبدأ من A وتنتهي بــ B حيث إن حدين متجاورين (s1,s2)  يحققان الخاصية الآتية: 

 sk  ⊳β1 sk+1

في المثال السابق نمثل لسلسلة الاختزالات بــ  c :

(λx.(λy.yx)z)v  ,   (λy.yv)z  , zv

الصيغة الطبيعية[12]

ملاحظة هامة في الحوسبة تستحق أن نقف عندها مفادها أن عملية اختزال الحدود  ) مثل a و b  و (c قد تتوقف عند صيغة محددة، إذ توقف الاختزال عند الصيغة N(Ny) بالنسبة لـ a ، وتوقف الاختزال عند الصيغة zv بالنسبة لــ c  ولم يبق لنا من سبيل إلى اختزالها أكثر، لأنه لا توجد صيغة قابلة للاختزال تنتظر منا أن نقلصها هذا من جهة، أما من جهة ثانية  توجد حدود من قبيل d و e لا تتوقف عملية الاختزال بل تستمر إلى غير نهاية؛ فكلما اختزلنا صيغة قابلة للاختزال إلا وظهرت في النتيجة صيغ أخرى قابلة للاختزال تنتظر الاختزال، يُرمز للحد (λx.xx) (λx.xx)   الذي يوجد في d بالرمز Ω .

هذه الملاحظة ستجرنا إلى تعريف خاصية جد مهمة يتعلق الأمر بالصيغة الطبيعية[1]  .

تعريف: الحد Q الذي لا يتضمن أية صيغة قابلة للاختزال β-redex يسمى بصيغة طبيعية (أو بعبارة أخرى يوجد في صيغة طبيعية ونختزلها في الرمز nf)، إذا اختزلنا P إلى الحد Q في صيغة طبيعية nf ، عندئذ يسمى Q بالصيغة الطبيعية لــ P .

في c من المثال السابق يعتبر الحد zv  صيغة طبيعية لــ 

(λx.(λy.yx)z)v

  وفي a الحد N(Ny)  هو الصيغة الطبيعية لــ  

(λx.x(xy))N

الحد (λx.xx)(λx.xx)=Ω الموجود في d من المثال   لا توجد له صيغة طبيعية، دائما يختزل إلى نفسه. سنختزل العبارات الآتية إلى صيغها الطبيعية:

(λx.xy)(λu.vuu)          ⊳β   (λu.vuu) y ⊳β    vyy
(λxy.yx)uv ⊳β   (λy.yu)v ⊳β   vu
(λx.xxy)(λy.yz)           ⊳β    (λy.yz) (λy.yz)y ≡ ((λy.yz) (λy.yz))y
                         ⊳β    ((λy.yz)z)y  ⊳β     zzy

ملاحظة مهمة تتعلق بكون بعض الحدود توجد أكثر من طريقة في اختزالها، إذا عدنا إلى الحد c الذي يوجد في  المثال 87، يمكن أن نختزل هذا الحد بطريقتين مختلفتين كما يتبين من الاختزالات الممكنة الآتية:

الإمكانية الأولى:

(λx.(λy.yx)z)v  ⊳β   (λy.yv)z) ⊳β   zv

الإمكانية الثانية: 

(λx.(λy.yx)z)v  ⊳β   (λy.yv)z) ⊳β   zv

في هذه الإمكانية اختزلنا الحد (z(λy.yx).الذي يوجد ضمن الحد الأكبر المتضمن له. يلاحظ أن كلا الامكانيتين أفضتا إلى صيغة طبيعية واحدة، وهذه خاصية لابد أن تتميز بها جميع الأنساق الحوسبية أي يتوجب أن توجد صيغة طبيعية واحد مهما اختلفت الطرق المؤدية إليها.

[1] - normal form

مراجع

1-طارق المالكي (2023) ، نظرية الربط البنيوي ، دار كنوز ،عمان.

  1. ^ Turing, A. M. (December 1937). "Computability and λ-Definability". The Journal of Symbolic Logic. 2 (4): 153–163. doi:10.2307/2268280. JSTOR 2268280.
  2. ^ طارق المالكي (2023). نظرية الربط البنيوي (ط. الاولى). عمان: دار كنوز. ص. 322. ISBN:978-9923-49-146-1.
  3. ^ طارق المالكي (2023). نظرية الربط البنيوي (ط. الاولى). دار كنوز المعرفة. ص. 323.
  4. ^ Coquand, Thierry, "Type Theory", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
  5. ^ Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus - Michael Moortgat - Google Books, Books.google.co.uk, 1988-01-01, ISBN 9789067653879, retrieved 2013-09-15
  6. ^ Computing Meaning - Google Books, Books.google.co.uk, 2008-07-02, ISBN 9781402059575, retrieved 2013-09-15
  7. ^ Mitchell, John C. (2003), Concepts in Programming Languages, Cambridge University Press, p. 57, ISBN 9780521780988.
  8. ^ Basic Category Theory for Computer Scientists, p. 53, Benjamin C. Pierce
  9. ^ طارق المالكي (2023). نظرية الربط البنيوي (ط. الاولى). دار كنوز المعرفة. ص. 328.
  10. ^ طارق المالكي (2023). نظرية الربط البنيوي (ط. الاولى). دار كنوز المعرفة.
  11. ^ طارق المالكي (2023). نظرية الربط البنيوي. دار كنوز المعرفة. ص. 332. ISBN:978-9923-49-146-1.
  12. ^ طارق المالكي (2023). نظرية الربط البنيوي (ط. الاولى). دار كنوز المعرفة. ص. 334. ISBN:978-9923-49-146-1.


مجلوبة من «https://3rabica.org/index.php?title=تكامل_لامدا&oldid=1440080»