Agda (dasturlash tili) - Agda (programming language)

Agda
Sans-serif testida
ParadigmaFunktsional
LoyihalashtirilganUlf Norell; Katarina Kokand (1,0)
TuzuvchiUlf Norell; Katarina Kokand (1,0)
Birinchi paydo bo'ldi2007; 13 yil oldin (2007) (1999 yilda 1,0); 21 yil oldin (1999))
Barqaror chiqish
2.6.1 / 2020 yil 16-mart; 8 oy oldin (2020-03-16)
Matnni yozishkuchli, statik, qaram, nominal, manifest, xulosa qilingan
Amalga oshirish tiliXaskell
OSO'zaro faoliyat platforma
LitsenziyaBSD-ga o'xshash[1]
Fayl nomi kengaytmalari.agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex
Veb-saytwiki.portal.chalmers.se/ agda
Ta'sirlangan
Coq, Epigramma, Xaskell
Ta'sirlangan
Idris

Agda a bog'liq ravishda yozildi funktsional dasturlash dastlab Ulf Norell tomonidan ishlab chiqilgan til Chalmers Texnologiya Universiteti doktorlik dissertatsiyasida bayon qilingan.[2] Asl Agda tizimi Chalmersda Katarina Kokand tomonidan 1999 yilda ishlab chiqilgan.[3] Dastlab "Agda 2" nomi bilan tanilgan hozirgi versiya to'liq qayta yozilgan bo'lib, uni ism va urf-odatlarga ega bo'lgan yangi til deb hisoblash kerak.

Agda shuningdek asosidagi yordamchi takliflar - har xil paradigma, ammo farqli o'laroq Coq, alohida yo'q taktika til va dalillar funktsional dasturlash uslubida yozilgan. Tilida oddiy dasturlash konstruktsiyalari mavjud ma'lumotlar turlari, naqshlarni moslashtirish, yozuvlar, iboralarga ruxsat bering va modullar va a Xaskell - sintaksisga o'xshash. Tizim mavjud Emak va Atom interfeyslar[4][5] lekin buyruq satridan ommaviy rejimda ham foydalanish mumkin.

Agda Zhaohui Luo'siga asoslangan qaram turlarning yagona nazariyasi (UTT),[6] ga o'xshash turdagi nazariya Martin-Lyof turi nazariyasi.

Agda nomi bilan atalgan Shved ssenariysi "Xyonan Agda" qo'shig'i Cornelis Vreeswijk,[7] taxminan a tovuq Agda ismli. Bu nomlanishni anglatadi Coq.

Xususiyatlari

Induktiv turlari

Agda ma'lumotlar turlarini aniqlashning asosiy usuli bu o'xshash induktiv ma'lumotlar turlari orqali amalga oshiriladi ma'lumotlarning algebraik turlari qaram bo'lmagan holda yozilgan dasturlash tillarida.

Ning ta'rifi Peano raqamlari Agda:

 ma'lumotlar ℕ : O'rnatish qayerda   nol : ℕ suc : ℕ → ℕ

Asosan, bu tabiiy sonni ifodalovchi ℕ turdagi qiymatni yasashning ikki yo'li mavjudligini anglatadi. Boshlamoq, nol bu tabiiy son, va agar bo'lsa n bu tabiiy son suc n, uchun turgan voris ning n, bu ham tabiiy son.

Ikki tabiiy son o'rtasidagi "kichik yoki teng" munosabatlarning ta'rifi:

 ma'lumotlar _≤_ : ℕ → ℕ → O'rnatish qayerda   z≤n : {n : ℕ} → nol n s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

Birinchi konstruktor, z≤n, nol har qanday natural sondan kichik yoki unga teng bo'lgan aksiomaga to'g'ri keladi. Ikkinchi konstruktor, s≤s, dalilni o'zgartirishga imkon beradigan xulosa qoidasiga mos keladi n ≤ m ning daliliga suc n ≤ suc m.[8] Shunday qilib, qiymat s≤s {zero} {suc zero} (z≤n {suc zero}) biri (nolning vorisi), ikkitadan kam yoki unga teng (birining vorisi) ekanligini isbotidir. Jingalak qavslarda berilgan parametrlar, agar ular haqida xulosa chiqarish mumkin bo'lsa, ularni qoldirib yuborish mumkin.

Bog'langan holda naqshga mos kelish

Yadro tiplari nazariyasida teoremalarni isbotlash uchun induksiya va rekursiya printsiplaridan foydalaniladi induktiv turlari. Agda o'rniga bog'liq ravishda kiritilgan naqsh mosligi ishlatiladi. Masalan, tabiiy sonni qo'shishni quyidagicha aniqlash mumkin:

 nol n qo'shing = n qo'shish (m m) n = suc (qo'shmoq m n)

Rekursiv funktsiyalarni / induktiv dalillarni yozishning bunday usuli xom induksiya tamoyillarini qo'llashdan ko'ra tabiiyroqdir. Agda, bog'liq ravishda terilgan naqshlarni moslashtirish tilning ibtidoiysi hisoblanadi; asosiy tilda naqshga mos keladigan indüksiya / rekursiya tamoyillari yo'q.

Metavariablelar

Kabi o'xshash tizimlar bilan taqqoslaganda Agdaning o'ziga xos xususiyatlaridan biri Coq, dasturni qurish uchun metavariantlarga katta ishonch. Masalan, Agda quyidagi funktsiyalarni yozishi mumkin:

 qo'shish : ℕ → ℕ → X x y qo'shing = ?

? bu erda metavariable. Tizim bilan emacs rejimida o'zaro aloqada bo'lganda, u foydalanuvchiga kutilgan turini ko'rsatadi va ularga metavariantni takomillashtirishga imkon beradi, ya'ni uni batafsilroq kod bilan almashtirishga imkon beradi. Ushbu funktsiya Coq kabi taktikaga asoslangan tasdiqlovchi yordamchilarga o'xshash tarzda qo'shimcha dastur tuzish imkonini beradi.

Avtomatlashtirishni tasdiqlash

Sof tur nazariyasida dasturlash ko'plab zerikarli va takrorlanadigan dalillarni o'z ichiga oladi. Agda alohida taktika tiliga ega bo'lmasa-da, Agdaning o'zida foydali taktikalarni dasturlash mumkin. Odatda, bu Agda funktsiyasini yozish orqali ishlaydi, bu ixtiyoriy ravishda qiziqishning ba'zi xususiyatlarining dalillarini qaytaradi. Keyinchalik taktika ushbu funktsiyani turni tekshirish vaqtida ishlatish bilan tuziladi, masalan quyidagi yordamchi ta'riflardan foydalangan holda:

  ma'lumotlar Balki (A : O'rnatish) : O'rnatish qayerda    Faqat : A → Ehtimol A Hech narsa yo'q : Ehtimol A ma'lumotlar faqat {A : O'rnatish} : Ehtimol A → O'rnatish qayerda    avtomatik : ∀ {x} → faqat (Faqat x)  Taktik : ∀ {A : O'rnatish} (x : Ehtimol A) → faqat x → Hech narsa yo'q ()  Taktik (Faqat x) avtomatik = x

Funktsiya berilgan check-even: (n: ℕ) → Ehtimol (Hatto n) raqamni kiritgan va ixtiyoriy ravishda uning tengligining isbotini keltirgan holda, taktika quyidagicha tuzilishi mumkin:

  hatto taktika : {n : ℕ} → faqat (che-n n) → Hatto n-hatto taktika {n} = Taktik (che-n n)  lemma0 : Hatto nol lemma0 = hatto taktikani ham avtomatik tekshirish lemma2 : Hatto (suc (nol nol))  lemma2 = hatto taktikani ham avtomatik tekshirish

Har bir lemmaning haqiqiy isboti turni tekshirish vaqtida avtomatik ravishda tuziladi. Agar taktika muvaffaqiyatsiz bo'lsa, yozuvlarni tekshirish muvaffaqiyatsiz bo'ladi.

Bundan tashqari, murakkab taktikalarni yozish uchun Agda orqali avtomatlashtirishni qo'llab-quvvatlaydi aks ettirish. Yansıtma mexanizmi, dastur fragmentlarini mavhum sintaksis daraxtiga taklif qilish yoki ulardan taklif qilish imkonini beradi. Ko'zgu ishlatilish usuli Shablon Haskell ish uslubiga o'xshaydi.[9]

Tasdiqlashni avtomatlashtirishning yana bir mexanizmi - bu emacs rejimida izlashni qidirish. Mumkin bo'lgan isbotlash shartlarini sanab chiqadi (5 soniya bilan cheklangan) va agar shartlardan biri spetsifikatsiyaga mos keladigan bo'lsa, u harakat qo'llaniladigan meta o'zgaruvchiga qo'yiladi. Ushbu harakat ko'rsatmalarni qabul qiladi, masalan, qaysi teoremalar va qaysi modullardan foydalanish mumkin, harakatlar naqshlarni moslashtirishdan foydalanishi mumkinmi va hokazo.[10]

Tugatishni tekshirish

Agda - a umumiy til, ya'ni undagi har bir dastur tugashi va barcha mumkin bo'lgan naqshlarga mos kelishi kerak. Ushbu xususiyat bo'lmasa, tilning mantiqiyligi mos kelmaydi va o'zboshimchalik bilan bayonotlarni isbotlash mumkin bo'ladi. Tugatishni tekshirish uchun Agda Xomilaning tugashini tekshiruvchi usulidan foydalanadi.[11]

Standart kutubxona

Agda tabiiy raqamlar, ro'yxatlar va vektorlar kabi asosiy ma'lumotlar tuzilmalari haqida ko'plab foydali ta'riflar va teoremalarni o'z ichiga olgan keng de-fakto standart kutubxonaga ega. Kutubxona beta-versiyada va faol rivojlanmoqda.

Unicode

Agdaning eng diqqatga sazovor xususiyatlaridan biri bu katta bog'liqlikdir Unicode dastur manba kodida. Standart emacs rejimi kirish uchun yorliqlardan foydalanadi, masalan Sigma Σ uchun.

Orqa tomonlar

Ikkita kompilyatorning orqa tomonlari mavjud, ular Haskell uchun MAlonzo va bittasi JavaScript.

Shuningdek qarang

Adabiyotlar

  1. ^ Agda litsenziyasi fayli
  2. ^ Ulf Norell. Qarama-qarshi turlar nazariyasiga asoslangan amaliy dasturlash tiliga. Nomzodlik dissertatsiyasi. Chalmers Texnologiya Universiteti, 2007 yil. [1]
  3. ^ "Agda: Interaktiv isbot muharriri". Arxivlandi asl nusxasi 2011-10-08 kunlari. Olingan 2014-10-20.
  4. ^ Kokand, Katarina; Sinek, Dan; Takeyama, Makoto. Dalillarni va dasturlarni tuzadigan yo'naltirilgan qo'llab-quvvatlash uchun Emacs interfeysi (PDF). Dasturiy ta'minot nazariyasi va amaliyoti bo'yicha Evropa qo'shma konferentsiyalari 2005. Arxivlangan asl nusxasi (PDF) 2011-07-22.
  5. ^ "Atomda agda-rejim". Olingan 7 aprel 2017.
  6. ^ Luo, Chjaoxi. Hisoblash va fikrlash: informatika uchun tip nazariyasi. Oksford universiteti matbuoti, Inc., 1994 yil.
  7. ^ "" Agda "ning kelib chiqishi? (Agda pochta ro'yxati)". Olingan 24 oktyabr 2020.
  8. ^ "Natura Agda standart kutubxonasidan". Olingan 2014-07-20.
  9. ^ Van Der Uolt, Pol va Vouter Svierstra. "Agda aks ettirish orqali muhandislik isboti." Yilda Funktsional tillarni amalga oshirish va qo'llash, 157-173-betlar. Springer Berlin Heidelberg, 2013 yil. [2]
  10. ^ Kokke, Pepijn va Wouter Swierstra. "Agda avtoulov".
  11. ^ Hobil, Andreas. "homila - oddiy funktsional dasturlarning tugatilishini tekshiruvchi." Dasturlash laboratoriyasining hisoboti 474 (1998).[3]

Tashqi havolalar