تكامل لامدا

(بالتحويل من حسابات اللامدا)

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

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

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

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

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

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

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

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

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

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

مراجععدل

  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. ^ Coquand, Thierry, "Type Theory", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
  3. ^ 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
  4. ^ Computing Meaning - Google Books, Books.google.co.uk, 2008-07-02, ISBN 9781402059575, retrieved 2013-09-15
  5. ^ Mitchell, John C. (2003), Concepts in Programming Languages, Cambridge University Press, p. 57, ISBN 9780521780988.
  6. ^ Basic Category Theory for Computer Scientists, p. 53, Benjamin C. Pierce