آگدا (زبان برنامه‌نویسی)

بندانگشتی|تصویری از یک قطعه کد آگدا
**آگدا** یک زبان برنامه‌نویسی تابعی است که به صورت وابسته تایپ شده‌است و در ابتدا توسط اولف نورل در دانشگاه فناوری چالمرز توسعه یافت و پیاده‌سازی آن در پایان‌نامه دکترای او شرح داده شد. سیستم اصلی آگدا در چالمرز توسط کاتارینا کوکواند در سال ۱۹۹۹ توسعه یافت. نسخه فعلی، که در ابتدا با نام آگدا۲ شناخته می‌شد، یک بازنویسی کامل است که باید زبان جدیدی در نظر گرفته شود که نام و سنت مشترکی به اشتراک می‌گذارد

آگدا همچنین یک دستیار اثبات مبتنی بر پارادایم گزاره‌ها به‌عنوان انواع است، اما برخلاف Coq، زبان تاکتیکی جداگانه‌ای ندارد و اثبات‌ها به سبک برنامه‌نویسی تابعی نوشته شده‌اند. این زبان دارای ساختارهای برنامه‌نویسی معمولی مانند انواع داده‌ها، تطبیق الگو، رکوردها، عبارات let و ماژول‌ها، و یک نحو (سینتکس) هسکل مانند است. این سیستم دارای رابط‌های Emacs و Atom است اما می‌تواند در حالت دسته ای (بچ مود) خط فرمان نیز اجرا شود.

آگدا بر اساس نظریه یکپارچه انواع وابسته (UTT) می‌باشد؛ یک نظریه نوع مانند نظریه نوع Martin-Löf.

نام آگدا برگرفته از آهنگ سوئدی «هونان آگدا»، نوشته کورنلیس وریسویک است که در مورد مرغی به نام آگدا می‌باشد. این به نامگذاری Coq مربوط می‌شود.

## ویژگی‌ها
### انواع القایی
استفاده از انواع داده‌های استقرایی، راه اصلی تعریف انواع داده‌ها در آگدا است که مانند انواع داده‌های جبری در زبان‌های برنامه‌نویسی غیر وابسته به تایپ است.

در اینجا تعریفی از اعداد پیانو در آگدا آورده شده‌است:
```agda
data ℕ : Set where
   zero : ℕ
   suc : ℕ → ℕ
```
اساساً این به این معنی است که برای ساخت مقداری از نوع ℕ، دو رویکرد وجود دارد که نشان دهنده یک عدد طبیعی است. برای شروع، `zero` یک عدد طبیعی است، و اگر `n` یک عدد طبیعی باشد، پس `suc n` که کوتاه شدهٔ successor of `n` است نیز یک عدد طبیعی می‌باشد.

توصیفی از رابطه "کمتر یا مساوی" بین دو عدد طبیعی، در اینجا نوشته‌شده‌است:
```agda
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})` گواهی بر این مسئله است که یک (جانشین صفر)، کوچکتر یا مساوی دو (جانشین یک) است. اگر بتوان پارامترهای نشان داده شده در آکلادها را استنباط کرد، امکان دارد این پارامترها حذف شوند.

### تطابق الگوی وابسته تایپ شده
در نظریه نوع هسته، از اصل‌های استقرایی و بازگشتی برای اثبات قضیه‌های انواع استقرایی استفاده می‌شود. در آگدا، به جای آن از تطابق الگوی وابسته تایپ شده استفاده می‌شود. برای مثال، جمع اعداد طبیعی را می‌توان به صورت زیر تعریف کرد:
```agda
add zero n = n
 add (suc m) n = suc (add m n)
```
این روش نوشتن توابع بازگشتی/ اثبات‌های استقرایی، طبیعی تر از اعمال اصل‌های استقرایی خام است. در آگدا، تطابق الگوی وابسته تایپ شده، از اصول ابتدایی زبان است. زبان اصلی فاقد اصول استقرا/بازگشت است که تطابق الگو به آن ترجمه می‌شود.

### متا متغیرها
این روش نوشتن توابع بازگشتی/ اثبات‌های استقرایی طبیعی تر از اعمال اصول استقرایی خام است. در آگدا، تطابق الگوی وابسته تایپ شده، از اصول ابتدایی زبان است. زبان اصلی فاقد اصول استقرا/بازگشت است که تطابق الگو به آن ترجمه می‌شود.
```agda
add : ℕ → ℕ → ℕ
 add x y = ?
```
 یک متامتغیر در اینجا وجود دارد. در زمان تعامل با سیستم در حالت emacs، نوع مورد توقع کاربر را نشان می‌دهد و به او اجازه می‌دهد تا بتواند متا متغیر را اصلاح کنند، یعنی آن را با کد دقیق‌تر (با جزئیات بیشتر) جایگزین کنند. این ویژگی، امکان ساخت برنامه افزایشی را به روشی مشابه دستیارهای اثبات مبتنی بر تاکتیک، مانند Coq می‌دهد.

### اتوماسیون اثبات
در تئوری نوع محض، برنامه‌نویسی شامل بسیاری از اثبات‌های خسته کننده و تکراری است. گرچه آگدا هیچ زبان تاکتیکی جداگانه ای ندارد، ولی می‌توان تاکتیک‌های مفید را در خود آگدا برنامه‌نویسی کرد. به صورت معمول، این کار با نوشتن یک تابع آگدا انجام می‌شود که به صورت اختیاری یک اثبات برخی از ویژگی‌های مورد علاقه را برمی‌گرداند. سپس یک تاکتیک با اجرای این تابع در زمان بررسی نوع، برای مثال با استفاده از تعریف‌های کمکی زیر ساخته می‌شود:
```agda
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)` که عددی را به عنوان ورودی دریافت می‌کند و به صورت اختیاری اثبات زوج بودن آن را برمی‌گرداند، می‌توان تاکتیکی را به صورت زیر ساخت:
```agda
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 و یکی دیگر برای جاوااسکریپت.

## جستارهای وابسته
* Coq
* HOL (دستیار اثبات)
* Idris (زبان برنامه‌نویسی)
* Isabelle (دستیار اثبات)

## منابع

## پیوند به بیرون
* 
* 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 &#x5B;Meta&#x5D;Introduction to Dependent Types in Agda
* Agda Tutorial: "explore programming in Agda without theoretical background"

رده:دانشگاه صنعتی چالمرز
رده:دستیارهای اثباتی
رده:زبان‌های برنامه‌نویسی آکادمیک
رده:زبان‌های برنامه‌نویسی ایستا
رده:زبان‌های برنامه‌نویسی تطبیق الگو
رده:زبان‌های برنامه‌نویسی ساخته‌شده در ۲۰۰۷ (میلادی)
رده:زبان‌های برنامه‌نویسی
رده:زبان‌های تابعی
رده:کامپایلرها و مفسرهای آزاد
رده:نرم‌افزارهای آزاد چندسکویی
رده:نرم‌افزارهای ۲۰۰۷ (میلادی)