جبر لاندا

از ویکی‌پدیا، دانشنامهٔ آزاد
پرش به: ناوبری، جستجو

جبر لاندا یا جبر لامبدا (به انگلیسی: Lambda calculus یا λ-calculus) یک سیستم صوری در منطق ریاضی است که از آن برای نمایش محاسبات تحت انتزاع توابع استفاده می‌شود.[۱] این سیستم یک مدل محاسباتی است که قدرتش با یک ماشین تورینگ یک‌نواره برابری می‌کند و می‌تواند آن را شبیه‌سازی کند.[۲] جبر لاندا اولین بار در دهه ۱۹۳۰ توسط ریاضی‌دان آلونزو چرچ معرفی شد.[۱]

جبر لاندا از ساخت جملات لاندا و اعمال ساده‌سازی برروی آن‌ها تشکیل شده‌است. در ساده‌ترین حالت جبر لاندا، جملات تنها براساس قوانین زیر ساخته می‌شوند:[۳]

گرامر عنوان توضیحات
a متغیر یک حرف یا یک رشته که نماینده یک پارامتر یا مقدار منطقی یا ریاضی است.
(λx.M) انتزاع تعریف یک تابع (M یک عبارت لاندا است). متغیر x در این عبارت انقیاد می‌شود.
(M N) کاربرد اجرای یک تابع. M و N جملات لاندا هستند.

عملیات ساده‌سازی نیز پیرو قوانین زیر است:

عملیات عنوان توضیحات
(λx.M[x]) → (λy.M[y]) تبدیل آلفا تغییر نام متغیرها برای جلوگیری از برخورد نام متغیرها (Name collision).
((λx.M) E) → (M[x:=E]) ساده‌سازی بتا جایگذاری یک متغیر با آرگومان تابع در بدنه تابع.

اگر ساده‌سازی تکرار شده و بعد از چندین مرحله به پایان برسد، براساس قضیه چرچ-راسر به یک عبارت فرم نرمال بتا تبدیل خواهد شد.

تعریف و کاربرد[ویرایش]

جبر لاندا یک تورین کامل است، به عبارت دیگر، یک مدل محاسبه عمومی‌ست که می‌تواند هر ماشین تورینگ یک‌نواره را شبیه‌سازی کند.[۲] حرف یونانی لاندا (λ)، که در اسم این جبر حضور دارد، در عبارات لاندا و جملات لاندا برای نشان دادن انقیاد یک متغیر در یک تابع استفاده می‌شود.

جبر لاندا می‌تواند نوع‌دار (Typed) یا بدون نوع (Untyped) باشد. در جبر لاندای نوع‌دار یک تابع درصورتی می‌تواند صدا زده شود که توانایی پذیرش داده‌هایی با آن «نوع» خاص را داشته باشد. جبرهای لاندا نوع‌دار از لحاظ محاسباتی توانایی بیان کردن کمتری از جبرهای لاندای بدون نوع دارند؛ لذا از این جهت ضعیف‌تر هستند. اما از سوی دیگر قابلیت اثبات بالاتری دارند و می‌توانند چیزهای بیشتری را اثبات کنند. برای مثال در جبر لاندای نوع‌دار ساده، تمامی استراتژی‌های محاسبه تمام‌شدنی (terminating) هستند؛ در حالی که در جبر بدون نوع نیازی به تمام شدنی بودن نیست و محاسبه یک عبارت می‌تواند تا بینهایت ادامه پیدا کند.

جبر لاندا کاربردهای فراوانی در زمینه‌های مختلف از جمله ریاضیات، فلسفه،[۴] زبان‌شناسی[۵] و علوم رایانه[۶] دارد. همچنین این جبر نقش مهمی در گسترش نظریه زبان‌های برنامه‌نویسی ایفا می‌کند. برنامه‌نویسی تابعی در رایانه جبر لاندا را پیاده‌سازی می‌کند. این جبر هم‌اکنون یکی از موضوعات تحقیق در نظریه دسته‌هاست.[۱]

تاریخچه[ویرایش]

جبر لاندا برای اولین بار در دهه ۱۹۳۰ توسط آلونزو چرچ در قسمتی از تحقیقاتش دربارهٔ بنیان‌های ریاضیات مطرح شد.[۷] در سال ۱۹۳۵ استیون کلینی و جان راسر با مطرح کردن تناقض کلینی-راسر نشان دادند که سیستم مطرح شده اولیه از لحاظ منطقی ناسازگار است.[۸]

در نتیجه این اتفاق، در سال ۱۹۳۶ چرچ قسمتی از جبر که مربوط به محاسبات بود را جداگانه منتشر کرد. این قسمت امروزه جبر لاندای بدون نوع خوانده می‌شود.[۹] در سال ۱۹۴۰ نیز چرچ نسخه‌ای از جبر لاندا، که از لحاظ محاسباتی ضعیف‌تر، اما از لحاظ منطقی سازگار بود را تحت عنوان جبر لاندای نوع‌دار ساده منتشر کرد.[۱۰]

تا قبل از دهه ۱۹۶۰ که رابطه آن با زبان‌های برنامه‌نویسی مشخص شود، جبر لاندا تنها جنبه صوری داشت. بعدها نیز با این جبر در زبان‌شناسی[۱۱] و علوم رایانه از جایگاه مهمی برخوردار شد.[۱۲]

جستارهای وابسته[ویرایش]

منابع[ویرایش]

  1. ۱٫۰ ۱٫۱ ۱٫۲ Pierce, Benjamin C.. Basic Category Theory for Computer Scientists. p. 53. 
  2. ۲٫۰ ۲٫۱ Turing, A. M. (December 1937). "Computability and λ-Definability". The Journal of Symbolic Logic 2 (4): 153–163. JSTOR 2268280. doi:10.2307/2268280. 
  3. Barendregt، Henk. Introduction to Lambda Calculus. 1998. 
  4. Coquand, Thierry, "Type Theory", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
  5. Moortgat, Michael (1988). Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus. Foris Publications. ISBN 9789067653879. 
  6. Mitchell, John C. (2003), Concepts in Programming Languages, Cambridge University Press, p. 57, ISBN 978-0-521-78098-8 .
  7. Church, A. (1932). "A set of postulates for the foundation of logic". Annals of Mathematics. Series 2 33 (2): 346–366. JSTOR 1968337. doi:10.2307/1968337. 
  8. Kleene, S. C.; Rosser, J. B. (July 1935). "The Inconsistency of Certain Formal Logics". The Annals of Mathematics 36 (3): 630. doi:10.2307/1968646. 
  9. Church, A. (1936). "An unsolvable problem of elementary number theory". American Journal of Mathematics 58 (2): 345–363. JSTOR 2371045. doi:10.2307/2371045. 
  10. Church, A. (1940). "A Formulation of the Simple Theory of Types". Journal of Symbolic Logic 5 (2): 56–68. JSTOR 2266170. doi:10.2307/2266170. 
  11. Partee, B. B. H.; ter Meulen, A.; Wall, R. E. (1990). Mathematical Methods in Linguistics. Springer. Retrieved 29 Dec 2016. 
  12. Alama, Jesse "The Lambda Calculus", The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).