لین (دستیار اثبات)
 | |
| پارادایم برنامه‌نویسی | برنامه‌نویسی تابعی، برنامه‌نویسی دستوری |
|---|---|
| توسعه‌دهنده | Lean FRO |
| ظهوریافته در | ۲۰۱۳ |
| انتشار پایدار | 4.7.0
/ ۳ آوریل ۲۰۲۴ |
| انتشار آزمایشی | 4.8.0-rc1
/ ۲ مه ۲۰۲۴ |
| ایستا، قوی، استنتاجی | |
زبان پیاده‌سازی | Lean , C++ |
| سیستم‌عامل | چندسکویی |
| پروانه | مجوز آپاچی ۲.۰ |
| وبگاه | |
| متأثر از | |
| ML Coq هسکل | |
Lean یک دستیار اثبات و یک زبان برنامه‌نویسی تابعی است.[۱] این زبان مبتنی بر حساب سازه‌ها با نوع‌های القایی است. Lean یک پروژه متن‌باز است که بر روی گیت‌هاب میزبانی می‌شود. این زبان به طور اولیه توسط لئوناردو د مورا در حین اشتغال در مایکروسافت ریسرچ توسعه داده شد و اکنون در آمازون وب سرویسز ادامه دارد. توسعه این زبان در حال حاضر توسط سازمان Lean سازمان تحقیقات متمرکز (FRO) پشتیبانی می‌شود.
تاریخچه[ویرایش]
Lean توسط لئوناردو د مورا در مایکروسافت ریسرچ در سال ۲۰۱۳ راه‌اندازی شد.[۲] نسخه‌های اولیه این زبان، که بعدها به نام Lean 1 و 2 شناخته شدند، آزمایشی بودند و ویژگی‌هایی مانند پشتیبانی از نظریه نوع هموتوپی داشتند که بعدها حذف شدند.
Lean 3 (برای اولین بار در ۲۰ ژانویه ۲۰۱۷ منتشر شد) اولین نسخه نسبتاً پایدار Lean بود. این نسخه عمدتاً با زبان C++ پیاده‌سازی شده بود و برخی از ویژگی‌ها نیز با خود زبان Lean نوشته شده بودند. پس از نسخه 3.4.2، Lean 3 به طور رسمی پایان عمر خود را اعلام کرد در حالی که توسعه Lean 4 آغاز شد. در این دوره بینابینی، اعضای جامعه Lean نسخه‌های غیررسمی تا 3.51.1 را توسعه داده و منتشر کردند.
در سال ۲۰۲۱، Lean 4 منتشر شد که بازسازی اثبات‌گر Lean بود که قادر به تولید کد C است که سپس کامپایل می‌شود و امکان توسعه خودکارسازی حوزه‌های خاص را فراهم می‌کند.[۳] Lean 4 همچنین سیستم ماکرو و بهبودهای سنتز کلاس نوع و روش‌های مدیریت حافظه را نسبت به نسخه قبلی داراست. یکی دیگر از مزایای آن نسبت به Lean 3، امکان اجتناب از لمس کد C++ برای تغییر رابط کاربری و دیگر قسمت‌های اصلی سیستم است، زیرا همه آنها اکنون در Lean پیاده‌سازی شده و در دسترس کاربر نهایی برای جایگزینی در صورت نیاز هستند.[نیازمند منبع]
Lean 4 با Lean 3 سازگاری معکوس ندارد.[۴]
در سال ۲۰۲۳، Lean FRO تشکیل شد، با اهداف بهبود مقیاس‌پذیری و قابلیت استفاده از زبان و اجرای اتوماسیون اثبات.[۵]
مرور کلی[ویرایش]
کتابخانه‌ها[ویرایش]
بسته رسمی Lean شامل یک کتابخانه استاندارد std4 است که ساختارهای داده‌ای مشترک را که می‌تواند برای هر دو تحقیق ریاضی و توسعه نرم‌افزار متعارف استفاده شود، پیاده‌سازی می‌کند.[۶]
در سال ۲۰۱۷، یک پروژه نگهداری شده توسط جامعه برای توسعه یک کتابخانه Lean mathlib آغاز شد، با هدف دیجیتالی کردن هر چه بیشتر ریاضیات ریاضیات محض در یک کتابخانه بزرگ یکپارچه، تا سطح تحقیقاتی ریاضی.[۷][۸] تا نوامبر ۲۰۲۳، mathlib بیش از ۱۲۷,۰۰۰ قضیه و ۷۰,۰۰۰ تعریف را در Lean رسمی کرده بود.[۹]
یکپارچه‌سازی ویرایشگرها[ویرایش]
Lean با:[۱۰]
ارتباط‌گیری از طریق یک سرور پروتکل زبان و یک افزونه کلاینت انجام می‌شود.
این زبان دارای پشتیبانی بومی از نمادهای یونیکد است که می‌توان با استفاده از توالی‌های شبیه به LaTeX، مانند "\times" برای "×" تایپ کرد. Lean همچنین می‌تواند به جاوااسکریپت کامپایل شود و در یک مرورگر وب دسترسی داشته باشد و از پشتیبانی گسترده‌ای برای فرا-برنامه‌نویسی برخوردار است.
نمونه‌ها (Lean 4)[ویرایش]
اعداد طبیعی می‌توانند به عنوان یک نوع القایی تعریف شوند. این تعریف بر اساس اصل پیانو است و بیان می‌کند که هر عدد طبیعی یا صفر است یا جانشین عدد طبیعی دیگری است.
inductive Nat : Type
| zero : Nat
| succ : Nat → Nat
جمع اعداد طبیعی می‌تواند به صورت تعریف بازگشتی تعریف شود، با استفاده از تطبیق الگو.
def Nat.add : Nat → Nat → Nat
| a, zero => a
| a, succ b => succ (Nat.add a b)
با استفاده از این تعریف‌ها، ما می‌توانیم یک اثبات تعریف بازگشتی برای یک قضیه ساده بنویسیم.
theorem zero_add (a : Nat) : Nat.add zero a = a :=
match a with
| zero => rfl
| succ a' => congrArg succ (zero_add a')
منابع[ویرایش]
- ↑ https://pp.ipd.kit.edu/uploads/publikationen/demoura21lean4.pdf
- ↑ "About". Lean Language. Retrieved 2024-03-13.
- ↑ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff (eds.). Automated Deduction -- CADE 28. Springer International Publishing. pp. 625–635. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5. S2CID 235800962. Retrieved 24 March 2023.
- ↑ "Significant changes from Lean 3". Lean Manual. Retrieved 24 March 2023.
- ↑ "Mission". Lean FRO. 2023-07-25. Retrieved 2024-03-14.
- ↑ "std4". GitHub. Retrieved 2024-03-13.
- ↑ "Building the Mathematical Library of the Future". Quanta Magazine. Archived from the original on 2 Oct 2020.
- ↑ "Lean community". leanprover-community.github.io. Retrieved 2023-10-24.
- ↑ "Mathlib statistics". leanprover-community.github.io. Retrieved 2023-11-01.
- ↑ "Installing Lean 4 on Linux". leanprover-community.github.io. Retrieved 2023-10-24.
پیوند به بیرون[ویرایش]
- دستیاران اثبات
- زبانهای برنامه‌نویسی تابعی
- نرمافزارهای چندسکویی
- نرمافزارهای آموزشی ریاضی
- نرم‌افزار آزاد و متن‌باز
- نرمافزارهای ریاضی آزاد
- نرمافزارهای آزاد نوشتهشده با سی++
- زبانهای تابعی
- مؤسسه تحقیقاتی مایکروسافت
- نرمافزارهای رایگان مایکروسافت
- دستیارهای اثباتی
- نرمافزارهایی که از پروانه آپاچی استفاده میکنند
- سیستمهای نرمافزاری اثبات قضیه