آگدا (زبان برنامه‌نویسی)
آگدا یک زبان برنامه‌نویسی تابعی است که به صورت وابسته تایپ شده‌است و در ابتدا توسط اولف نورل در دانشگاه فناوری چالمرز توسعه یافت و پیاده‌سازی آن در پایان‌نامه دکترای او شرح داده شد. سیستم اصلی آگدا در چالمرز توسط کاتارینا کوکواند در سال ۱۹۹۹ توسعه یافت. نسخه فعلی، که در ابتدا با نام آگدا۲ شناخته می‌شد، یک بازنویسی کامل است که باید زبان جدیدی در نظر گرفته شود که نام و سنت مشترکی به اشتراک می‌گذارد
آگدا همچنین یک دستیار اثبات مبتنی بر پارادایم گزاره‌ها به‌عنوان انواع است، اما برخلاف Coq، زبان تاکتیکی جداگانه‌ای ندارد و اثبات‌ها به سبک برنامه‌نویسی تابعی نوشته شده‌اند. این زبان دارای ساختارهای برنامه‌نویسی معمولی مانند انواع داده‌ها، تطبیق الگو، رکوردها، عبارات let و ماژول‌ها، و یک نحو (سینتکس) هسکل مانند است. این سیستم دارای رابط‌های Emacs و Atom است اما می‌تواند در حالت دسته ای (بچ مود) خط فرمان نیز اجرا شود.
آگدا بر اساس نظریه یکپارچه انواع وابسته (UTT) می‌باشد؛ یک نظریه نوع مانند نظریه نوع Martin-Löf.
نام آگدا برگرفته از آهنگ سوئدی «هونان آگدا»، نوشته کورنلیس وریسویک است که در مورد مرغی به نام آگدا می‌باشد. این به نامگذاری Coq مربوط می‌شود.
ویژگی‌ها
[ویرایش]انواع القایی
[ویرایش]استفاده از انواع داده‌های استقرایی، راه اصلی تعریف انواع داده‌ها در آگدا است که مانند انواع داده‌های جبری در زبان‌های برنامه‌نویسی غیر وابسته به تایپ است.
در اینجا تعریفی از اعداد پیانو در آگدا آورده شده‌است:
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
اساساً این به این معنی است که برای ساخت مقداری از نوع ℕ، دو رویکرد وجود دارد که نشان دهنده یک عدد طبیعی است. برای شروع، zero یک عدد طبیعی است، و اگر n یک عدد طبیعی باشد، پس suc n که کوتاه شدهٔ successor of n است نیز یک عدد طبیعی می‌باشد.
توصیفی از رابطه "کمتر یا مساوی" بین دو عدد طبیعی، در اینجا نوشته‌شده‌است:
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m
سازنده اول، z≤n ، با این اصل تطابق دارد که صفر، کوچکتر یا مساوی هر عدد طبیعی است. سازنده دوم، s≤s ، با یک قانون استنتاج مطابقت دارد که اجازه می‌دهد یک اثبات n ≤ m را به یک اثبات suc n ≤ suc m تبدیل شود. در نتیجه مقدار s≤s {zero} {suc zero} (z≤n {suc zero}) گواهی بر این مسئله است که یک (جانشین صفر)، کوچکتر یا مساوی دو (جانشین یک) است. اگر بتوان پارامترهای نشان داده شده در آکلادها را استنباط کرد، امکان دارد این پارامترها حذف شوند.
تطابق الگوی وابسته تایپ شده
[ویرایش]در نظریه نوع هسته، از اصل‌های استقرایی و بازگشتی برای اثبات قضیه‌های انواع استقرایی استفاده می‌شود. در آگدا، به جای آن از تطابق الگوی وابسته تایپ شده استفاده می‌شود. برای مثال، جمع اعداد طبیعی را می‌توان به صورت زیر تعریف کرد:
add zero n = n
add (suc m) n = suc (add m n)
این روش نوشتن توابع بازگشتی/ اثبات‌های استقرایی، طبیعی تر از اعمال اصل‌های استقرایی خام است. در آگدا، تطابق الگوی وابسته تایپ شده، از اصول ابتدایی زبان است. زبان اصلی فاقد اصول استقرا/بازگشت است که تطابق الگو به آن ترجمه می‌شود.
متا متغیرها
[ویرایش]این روش نوشتن توابع بازگشتی/ اثبات‌های استقرایی طبیعی تر از اعمال اصول استقرایی خام است. در آگدا، تطابق الگوی وابسته تایپ شده، از اصول ابتدایی زبان است. زبان اصلی فاقد اصول استقرا/بازگشت است که تطابق الگو به آن ترجمه می‌شود.
add : ℕ → ℕ → ℕ
add x y = ?
یک متامتغیر در اینجا وجود دارد. در زمان تعامل با سیستم در حالت emacs، نوع مورد توقع کاربر را نشان می‌دهد و به او اجازه می‌دهد تا بتواند متا متغیر را اصلاح کنند، یعنی آن را با کد دقیق‌تر (با جزئیات بیشتر) جایگزین کنند. این ویژگی، امکان ساخت برنامه افزایشی را به روشی مشابه دستیارهای اثبات مبتنی بر تاکتیک، مانند Coq می‌دهد.
اتوماسیون اثبات
[ویرایش]در تئوری نوع محض، برنامه‌نویسی شامل بسیاری از اثبات‌های خسته کننده و تکراری است. گرچه آگدا هیچ زبان تاکتیکی جداگانه ای ندارد، ولی می‌توان تاکتیک‌های مفید را در خود آگدا برنامه‌نویسی کرد. به صورت معمول، این کار با نوشتن یک تابع آگدا انجام می‌شود که به صورت اختیاری یک اثبات برخی از ویژگی‌های مورد علاقه را برمی‌گرداند. سپس یک تاکتیک با اجرای این تابع در زمان بررسی نوع، برای مثال با استفاده از تعریف‌های کمکی زیر ساخته می‌شود:
data Maybe (A : Set) : Set where
Just : A → Maybe A
Nothing : Maybe A
data isJust {A : Set} : Maybe A → Set where
auto : ∀ {x} → isJust (Just x)
Tactic : ∀ {A : Set} (x : Maybe A) → isJust x → A
Tactic Nothing ()
Tactic (Just x) auto = x
با توجه به تابع check-even : (n : ℕ) → Maybe (Even n) که عددی را به عنوان ورودی دریافت می‌کند و به صورت اختیاری اثبات زوج بودن آن را برمی‌گرداند، می‌توان تاکتیکی را به صورت زیر ساخت:
check-even-tactic : {n : ℕ} → isJust (check-even n) → Even n
check-even-tactic {n} = Tactic (check-even n)
lemma0 : Even zero
lemma0 = check-even-tactic auto
lemma2 : Even (suc (suc zero))
lemma2 = check-even-tactic auto
اثبات واقعی هر لم در زمان بررسی نوع، به صورت اتوماتیک ساخته می‌شود. اگر تاکتیک شکست بخورد، آن‌گاه بررسی نوع شکست خواهد خورد.
اضافه بر این، برای نوشتن تاکتیک‌های پیچیده‌تر، آگدا از اتوماسیون از طریق بازتاب (ریفلکشن) پشتیبانی می‌کند. مکانیسم بازتاب به فرد اجازه می‌دهد تا قطعات برنامه را به درخت نحو انتزاعی نقل قول کند یا آنها را از آن خارج کند. نحوه استفاده از بازتاب مشابه روشی است کهTemplate Haskell کار می‌کند.[۱]
یک مکانیزم دیگر برای اتوماسیون اثبات، اقدام جستجوی اثبات در حالت emacs است. این کار عبارت‌های اثبات احتمالی را برمی‌شمارد (محدود به ۵ ثانیه) و اگر یکی از عبارت‌ها با مشخصات همخوانی داشته باشد، در متا متغیر جایی که عمل فراخوانی می‌شود، قرار می‌گیرد. این کار نکته‌هایی را می‌پذیرد، به عنوان مثال، از کدام قضیه‌ها و از کدام ماژول‌ها می‌توان استفاده کرد، آیا می‌توان از تطابق الگو استفاده کند یا خیر، و ….
بررسی خاتمه
[ویرایش]آگدا یک زبان کل است، این بدان معنی است که هر برنامه در آن باید خاتمه یابد و همهٔ الگوهای ممکن باید تطابق داشته باشند. بدون این ویژگی، منطق پشت زبان ناسازگار می‌شود و امکان اثبات گزاره‌های دلخواه فراهم می‌شود. برای بررسی خاتمه، آگدا از روش بررسی کننده ختم جنین استفاده می‌کند.
کتابخانه استاندارد
[ویرایش]آگدا یک کتابخانه استاندارد بالفعل گسترده دارد که شامل تعریف‌ها و قضیه‌های مفید زیادی در مورد ساختارهای داده پایه، مانند اعداد طبیعی، لیست‌ها و بردارها می‌باشد. این کتابخانه در نسخه بتا است و تحت توسعه فعال است.
یونی‌کد
[ویرایش]یکی از برجسته‌ترین ویژگی‌های آگدا، وابستگی شدید به یونی‌کد در کد منبع برنامه است. حالت استاندارد emacs از میانبرهایی برای ورودی استفاده می‌کند، مانند \Sigma برای Σ.
بک‌اندها
[ویرایش]دو بک‌اند کامپایلر وجود دارد، MAlonzo برای Haskell و یکی دیگر برای جاوااسکریپت.
جستارهای وابسته
[ویرایش]منابع
[ویرایش]- ↑ Van Der Walt, Paul, and Wouter Swierstra. "Engineering proof by reflection in Agda." In Implementation and Application of Functional Languages, pp. 157-173. Springer Berlin Heidelberg, 2013.
پیوند به بیرون
[ویرایش]- وبگاه رسمی
- Dependently Typed Programming in Agda, by Ulf Norell
- A Brief Overview of Agda, by Ana Bove, Peter Dybjer, and Ulf Norell
- Introduction to Agda, a five-part YouTube playlist by Daniel Peebles
- Brutal [Meta]Introduction to Dependent Types in Agda
- Agda Tutorial: "explore programming in Agda without theoretical background"
