Agda (programmalastırıw tili)

Agda
Paradigması	Ulıwma funkcional
Islep shıǵarıwshılar	Ulf Norell; Katarina Kokuand (1.0)
Baǵdarlamashı	Chalmers texnologiya universiteti
Birinshi shıǵarılıwı	1.0 – 1999-jıl 2.0 – 2007-jıl
Turaqlı versiyası	2.8.0 / 5-iyul 2025-jıl
Tiplestiriw tártibi	Kúshli, statikalıq, ǵárezli, nominal, anıq, juwmaq
Implementaciya tili	Haskell
Operaciyalıq sistema	Kross-platformalı
Licenziya	BSD uqsas[1]
Fayl keńeytpeleri	.agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex
Veb-saytı	wiki.portal.chalmers.se/agda

Agda — bul ǵárezli tiplestirilgen funkcional programmalastırıw tili, dáslep Chalmers Texnologiya Universitetinde Ulf Norell tárepinen islep shıǵılǵan, onıń implementaciyası onıń PhD dissertaciyasında súwretlengen. Dáslepki Agda sisteması Chalmers universiteti tárepinen 1999-jılı Katarina Kokand tárepinen islep shıǵılǵan. Házirgi versiyası, dáslep Agda 2 dep atalǵan, tolıq qayta jazılǵan bolıp, onıń ataması hám dástúrin bólisetuǵın jańa til dep esaplaw kerek.

Agda sonday-aq propoziciyalar-tipler retinde paradigmasına (Karri-Govard sáykesligi) tiykarlanǵan dálillew járdemshisi bolıp tabıladı, biraq Rocq-tan ózgesheligi, onıń bólek taktikalar tili joq hám dáliller funkcional programmalastırıw stilinde jazıladı. Tilde maǵlıwmat tipleri, úlgi boyınsha sáykeslestiriw, jazbalar, let ańlatpaları hám moduller sıyaqlı ádettegi programmalastırıw konstrukciyaları hám Haskell-ge uqsas sintaksis bar. Sistemanıń Emacs, Atom hám VS Code interfeysleri bar, biraq onı komanda qatarı interfeysinen paketli qayta islew rejiminde de iske túsiriwge boladı.

Agda Chjaoxuey Luonıń ǵárezli tiplerdiń birlesken teoriyasına (UTT), yaǵnıy Martin-Lyof tip teoriyasına uqsas tip teoriyasına tiykarlanǵan.

Agda Kornelis Vresveyk tárepinen jazılǵan shved qosıǵı «Honan Agda» húrmetine atalǵan, bul qosıq Agda atlı tawıq haqqında. Bul dáslep Terri Kokan húrmetine Coq dep atalǵan Rocq teorema dálillewshisiniń atına meńzeydi.

Ózgeshelikleri

Induktiv tipler

Agdada maǵlıwmat tiplerin anıqlawdıń tiykarǵı usılı ǵárezli tiplestirilmegen programmalastırıw tillerindegi algebralıq maǵlıwmat tiplerine uqsas bolǵan induktiv maǵlıwmat tipleri arqalı ámelge asırıladı.

Tómende Agda da Peano sanlarınıń anıqlaması keltirilgen:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

Tiykarınan, bul tábiyiy sandı bildiretuǵın ℕ tipindegi mánisti qurıwdıń eki usılı bar ekenligin ańlatadı. Basında, nol tábiyiy san bolıp tabıladı, hám eger n tábiyiy san bolsa, onda n-niń keyingisin bildiretuǵın suc n de tábiyiy san boladı. Tómende, eki tábiyiy san arasındaǵı «kishi yamasa teń» qatnasınıń anıqlaması:

data _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} → zero ≤ n
  s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

Birinshi konstruktor, z≤n, nol qálegen tábiyiy sannan kishi yamasa teń degen aksiomaǵa sáykes keledi. Ekinshi konstruktor, s≤s, n ≤ m dálilin suc n ≤ suc m dáliline aylandırıwǵa múmkinshilik beretuǵın shıǵarıw qaǵıydasına sáykes keledi. Solay etip, s≤s {zero} {suc zero} (z≤n {suc zero}) mánisi bir (noldiń keyingisi) ekiden (birdiń keyingisi) kishi yamasa teń ekenliginiń dálili bolıp tabıladı. Figuralı qawsırmalar ishindegi parametrler, eger olar shıǵarılıwı múmkin bolsa, túsirip qaldırılıwı múmkin.

Ǵárezli tiplestirilgen úlgi boyınsha sáykeslestiriw

Tiykarǵı tip teoriyasında induktiv tipler haqqındaǵı teoremalardı dálillew ushın indukciya hám rekursiya principleri qollanıladı. Agdada onıń ornına ǵárezli tiplestirilgen úlgi boyınsha sáykeslestiriw qollanıladı. Mısalı, tábiyiy sanlardı qosıwdı tómendegishe anıqlawǵa boladı:

add zero n = n
add (suc m) n = suc (add m n)

Rekursiv funkciyalardı/induktiv dálillerdi jazıwdıń bul usılı taza indukciya principlerin qollanıwǵa qaraǵanda tábiyiyirek. Agdada ǵárezli tiplestirilgen úlgi boyınsha sáykeslestiriw tildiń primitivi bolıp tabıladı; tiykarǵı tilde úlgi boyınsha sáykeslestiriw awdarılatuǵın indukciya/rekursiya principleri joq.

Meta-ózgeriwshiler

Agdanıń Rocq sıyaqlı basqa uqsas sistemalar menen salıstırǵandaǵı ayrıqsha ózgeshelikleriniń biri - programma dúziw ushın meta-ózgeriwshilerge kóbirek súyeniwi. Mısalı, Agdada tómendegishe funkciyalar jazıwǵa boladı:

add : ℕ → ℕ → ℕ
add x y = ?

Bul jerdegi ? - meta-ózgeriwshi bolıp tabıladı. Emacs rejiminde sistema menen isleskende, ol paydalanıwshıǵa kútilgen tipti kórsetedi hám meta-ózgeriwshini anıqlastırıwǵa, yaǵnıy onı anıǵıraq kod penen almastırıwǵa múmkinshilik beredi. Bul ózgeshelik Rocq sıyaqlı taktikaǵa tiykarlanǵan dálillew járdemshilerine uqsas tárizde programmanı basqıshpa-basqısh dúziwge múmkinshilik beredi.

Dálillewdi avtomatlastırıw

Taza tip teoriyasında programmalastırıw kóplegen zeriktiretuǵın hám qaytalanatuǵın dálillerdi óz ishine aladı. Agdada ayrıqsha taktikalar tili bolmasa da, Agda ishinde paydalı taktikalar programmalastırıw múmkin. Ádette, bul belgili bir qásiyettiń dálilin qálew boyınsha qaytaratuǵın Agda funkciyasın jazıw arqalı isleydi. Sońınan taktika bul funkciyanı tip tekseriw waqtında iske túsiriw arqalı qurıladı, mısalı tómendegi járdemshi anıqlamalardı paydalanıp:

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

(Absurd dep atalatuǵın () úlgisi, eger tip tekseriwshi onıń tipiniń bos ekenligin, yaǵnıy onıń jalǵan usınıs ekenligin dálillese, sáykes keledi, sebebi ádette barlıq múmkin bolǵan konstruktorlardıń argumentleri qoljetimsiz boladı, yaǵnıy olardıń aldınǵı shártleri qanaatlandırılmaydı. Bul jerde isJust A tipindegi hesh qanday mánis qurıla almaydı, sebebi bul kontekstte Just konstruktorın qollanıwımız múmkin bolǵan A tipindegi mánis joq. Absurd úlgileri bar bolǵan hár qanday teńlemeniń oń tárepi túsirip qaldırıladı.) check-even : (n : ℕ) → Maybe (Even n) funkciyası berilgen bolsa, ol sandı kirgizip, tańlaw boyınsha onıń jup ekenliginiń dálilin qaytaradı, taktikanı tómendegishe dúziwge boladı:

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

Hárbir lemmanıń haqıyqıy dálili tip tekseriw waqtında avtomat túrde dúziledi. Eger taktika sátsiz bolsa, tip tekseriw de sátsiz boladı.

Bunnan basqa, quramalılıraq taktikalar jazıw ushın, Agda refleksiv programmalastırıw (refleksiya) arqalı avtomatlastırıwdı qollaydı. Refleksiya mexanizmi programma bólimlerin abstrakt sintaksislik teregine kirgiziwge yamasa onnan shıǵarıwǵa múmkinshilik beredi. Refleksiyanıń qollanılıw usılı Template Haskell-diń islew usılına uqsas.

Dálillewdi avtomatlastırıwdıń taǵı bir mexanizmi - Emacs rejimindegi dálilew izlew háreketi. Ol múmkin bolǵan dálil terminlerin (5 sekund penen sheklengen) dizip shıǵadı hám eger terminlerden biri specifikaciyaǵa sáykes kelse, ol háreket shaqırılǵan meta-ózgeriwshige qoyıladı. Bul háreket, mısalı, qaysı teoremalardıń hám qaysı modullerden paydalanıwǵa bolatuǵınlıǵı, hárekettiń úlgi boyınsha sáykeslestiriwdi paydalana alıw-almawı sıyaqlı kórsetpelerdi qabıl etedi.

Juwmaqlanıwdı tekseriw

Agda — bul tolıq funkcional programmalastırıw tili, yaǵnıy ondaǵı hárbir programma juwmaqlanıwı kerek hám barlıq múmkin bolǵan úlgilerge sáykes keliwi kerek. Bul ózgesheliksiz tildiń artındaǵı logika izbe-izsiz bolıp qaladı hám qálegen pikirlerdi dálillew múmkin bolıp qaladı. Juwmaqlanıwdı tekseriw ushın, Agda Foetus juwmaqlanıw tekseriwshisiniń usılın qollanadı.

Standart kitapxana

Agdanıń keń kólemli de-fakto standart kitapxanası bar, ol tábiyiy sanlar, dizimler hám vektorlar sıyaqlı tiykarǵı maǵlıwmat strukturaları haqqında kóplegen paydalı anıqlamalardı hám teoremalardı óz ishine aladı. Kitapxana beta-versiyada hám aktiv rawajlanıw basqıshında.

Unicode

Agdanıń eń kórnekli ózgeshelikleriniń biri - programma derek kodında Unicode qa kóp súyeniwi. Standart Emacs rejimi kirgiziw ushın \Sigma sıyaqlı qısqartpalardı paydalanadı (Σ ushın).

Bekendler

Eki kompilyator bekendi bar: MAlonzo (Haskell ushın) hám biri JavaScript ushın..