آگدا (زبان برنامه‌نویسی) کیست؟ توضیح بده.
آگدا یک زبان برنامه‌نویسی تابعی است که به صورت وابسته تایپ شده‌است و در ابتدا توسط اولف نورل در دانشگاه فناوری چالمرز توسعه یافت و پیاده‌سازی آن در پایان‌نامه دکترای او شرح داده شد. سیستم اصلی آگدا در چالمرز توسط کاتارینا کوکواند در سال ۱۹۹۹ توسعه یافت. نسخه فعلی، که در ابتدا با نام آگدا۲ شناخته می‌شد، یک بازنویسی کامل است که باید زبان جدیدی در نظر گرفته شود که نام و سنت مشترکی به اشتراک می‌گذاردآگدا همچنین یک دستیار اثبات مبتنی بر پارادایم گزاره‌ها به‌عنوان انواع است، اما برخلاف Coq، زبان تاکتیکی جداگانه‌ای ندارد و اثبات‌ها به سبک برنامه‌نویسی تابعی نوشته شده‌اند. این زبان دارای ساختارهای برنامه‌نویسی معمولی مانند انواع داده‌ها، تطبیق الگو، رکوردها، عبارات let و ماژول‌ها، و یک نحو (سینتکس) هسکل مانند است. این سیستم دارای رابط‌های Emacs و Atom است اما می‌تواند در حالت دسته ای (بچ مود) خط فرمان نیز اجرا شود.آگدا بر اساس نظریه یکپارچه انواع وابسته (UTT) می‌باشد؛ یک نظریه نوع مانند نظریه نوع Martin-Löf.نام آگدا برگرفته از آهنگ سوئدی «هونان آگدا»، نوشته کورنلیس وریسویک است که در مورد مرغی به نام آگدا می‌باشد. این به نامگذاری Coq مربوط می‌شود.ویژگی‌ها.انواع القایی.استفاده از انواع داده‌های استقرایی، راه اصلی تعریف انواع داده‌ها در آگدا است که مانند انواع داده‌های جبری در زبان‌های برنامه‌نویسی غیر وابسته به تایپ است.در اینجا تعریفی از اعداد پیانو در آگدا آورده شده‌است: data ℕ : Set where zero : ℕ suc : ℕ → ℕاساساً این به این معنی است که برای ساخت مقداری از نوع ℕ، دو رویکرد وجود دارد که نشان دهنده یک عدد طبیعی است. برای شروع، codice_1 یک عدد طبیعی است، و اگر codice_2 یک عدد طبیعی باشد، پس codice_3 که کوتاه شدهٔ successor of codice_2 است نیز یک عدد طبیعی می‌باشد.توصیفی از رابطه "کمتر یا مساوی" بین دو عدد طبیعی، در اینجا نوشته‌شده‌است: data _≤_ : ℕ → ℕ → Set where z≤n : {n : ℕ} → zero ≤ n s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc mسازنده اول، codice_5 ، با این اصل تطابق دارد که صفر، کوچکتر یا مساوی هر عدد طبیعی است. سازنده دوم، codice_6 ، با یک قانون استنتاج مطابقت دارد که اجازه می‌دهد یک اثبات codice_7 را به یک اثبات codice_8 تبدیل شود. در نتیجه مقدار codice_9 گواهی بر این مسئله است که یک (جانشین صفر)، کوچکتر یا مساوی دو (جانشین یک) است. اگر بتوان پارامترهای نشان داده شده در آکلادها را استنباط کرد، امکان دارد این پارامترها حذف شوند.تطابق الگوی وابسته تایپ شده.در نظریه نوع هسته، از اصل‌های استقرایی و بازگشتی برای اثبات قضیه‌های انواع استقرایی استفاده می‌شود. در آگدا، به جای آن از تطابق الگوی وابسته تایپ شده استفاده می‌شود. برای مثال، جمع اعداد طبیعی را می‌توان به صورت زیر تعریف کرد: 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با توجه به تابع codice_10 codice_11 codice_12 که عددی را به عنوان ورودی دریافت می‌کند و به صورت اختیاری اثبات زوج بودن آن را برمی‌گرداند، می‌توان تاکتیکی را به صورت زیر ساخت: 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 از میانبرهایی برای ورودی استفاده می‌کند، مانند codice_13 برای Σ.بک‌اندها.دو بک‌اند کامپایلر وجود دارد، MAlonzo برای Haskell و یکی دیگر برای جاوااسکریپت.