Share to: share facebook share twitter share wa share telegram print page

Agda

Agda
编程范型函数式编程
設計者Ulf Norell(2.0版)
Catarina Coquand(1.0版)
實作者Ulf Norell(2.0版)
Catarina Coquand(1.0版)
发行时间2007年,​17年前​(2007(2.0版)
1999年,​25年前​(1999(1.0版)
当前版本
  • 2.6.4.3 (2024年3月6日;穩定版本)[1]
編輯維基數據鏈接
型態系統静态类型强类型依赖类型
操作系统跨平台
許可證MITBSD-like[2]
文件扩展名.agda.lagda
網站Agda wiki
啟發語言
CoqEpigram英语EpigramHaskell
影響語言
Idris

Agda 是一个依赖类型纯函数式编程语言。目前的版本,Agda 2,最初由瑞典查尔摩斯工学院的 Ulf Norell 作为博士论文课题设计并实现[3]。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年开发,而现今的版本则是对其的彻底重写,因此可视作一个全新的语言,但保留了 Agda 的命名和传统。

Agda 的类型系统体现了柯里-霍华德同构(Curry-Howard correspondence),因此亦可作为一个构建构造性证明证明辅助工具英语Proof assistant。它的类型理论基于 Zhaohui Luo 提出的 UTT(unified theory of dependent types)[4],与 Per Martin-Löf直觉类型论相似。

Agda 与另一个基于依赖类型的证明辅助工具 Coq 设计上存在着显著的不同之处:它本身并不提供单独的证明策略语言(tactics),所有的证明均以函数式编程的方式书写;Agda 拥有许多常规的函数式程序语言要素,诸如:数据类型(data types)、模式匹配(pattern matching)、记录类型(records)、let表达式和模块(modules)等,而其语法设计则高度仿照 Haskell 语言。

用户可通过 EmacsAtom 编辑器的界面与 Agda 系统进行交互[5]。Agda 系统亦可藉由命令行单独调用。

通过类型检查的 Agda 程序可以被编译到 Haskell,并由 GHC 编译器最终编译为可执行的本地机器码;亦有编译到 JavaScript 的后端实现。

Agda 的名字来自于一首由音乐家 Cornelis Vreeswijk 创作的瑞典语歌曲“Hönan Agda”,歌词讲述了一只名叫 Agda 的母鸡的故事。这实际上影射了 Coq(Coq 在法语中意为公鸡)。

简介

一个简单的“Hello world”程序

将下述程序保存于文件hello-world.agda中:

module hello-world where

open import IO

main = run (putStrLn "Hello, World!")

在 Emacs 中可使用 C-c C-x C-c 来编译此程序;或在命令行中执行agda --compile hello-world.agda进行编译。

几点解释:

  • Agda 程序以模块(module)的形式组织而成。每一个文件中的第一个模块称之为最高级别(top-level)模块,其名称必须和文件名相符。模块的内容可以包括数据类型的定义、函数的定义等。
  • 外部模块可以通过import子句导入。例如在上述程序中,open import IO导入 Agda 标准库中的IO(标准输入输出)模块,并将其在当前作用域中打开。
  • 一个导出了函数名及类型签名main : IO a的模块即可以被编译成可执行文件。例如,上述程序中的main函数作用是将字符串“Hello, World!”写到标准输出,之后退出程序。

归纳类型(inductive types)

在 Agda 中定义数据类型的方式与其它(非依赖类型)编程语言中的代数数据类型相似。 例如,在 Agda 中归纳地定义皮亚诺数

data  : Set where
  zero :  
  succ :   

这表明存在两种形式可以用来构造一个自然数:首先,zero 是一个自然数;若已知 n 是一个自然数,则 succ n 也必定是一个自然数。

又如,Agda 中对小于或等于关系的定义:

data _≤_ :     Set where
  z≤n : {n : }  zero  n
  s≤s : {n m : }  n  m  succ n  succ m

第一处构造(z≤n)指出:zero 必定小于或等于任何自然数;第二处构造(s≤s)指出:当 n <= m 时必定有 succ n <= succ m。 例如,考虑z≤n {succ zero},依照定义,它是对零小于一的证明;再考虑s≤s {zero} {succ zero} (z≤n {succ zero}),则是对一小于二的证明。

依赖类型模式匹配(dependently typed pattern matching)

在类型论中,归纳和递归原则通常被用来证明涉及到归纳类型的定理。Agda 则使用依赖类型模式匹配来达到此目的。例如,自然数的加法可被定义为:

add zero n = n
add (succ m) n = succ (add m n)

比起运用归纳/递归原则,直接定义递归函数更加简单直观。依赖类型模式匹配是 Agda 内置的语言特性之一;其核心类型论并没有包含归纳/递归原则。

记录类型(records)

除了归纳类型之外,Agda 还支持记录类型。记录的作用是将若干类型的值包装在一起,并使用不同名称标识不同的域;它可看作是对依赖乘积类型(dependent product types)的推广。 例如,在 Agda 中定义一个值对(pair):

record Pair (A B : Set) : Set where
  field
    fst : A
    snd : B

以上代码定义了一个新的数据类型Pair : Set → Set → Set,以及两个投影函数:

Pair.fst : {A B : Set}  Pair A B  A
Pair.snd : {A B : Set}  Pair A B  B

记录类型的值可以使用记录表达式来创建,如:

p12 = record { fst = 1; snd = 2 }

若在定义记录类型时使用constructor关键字规定了构造器,则亦可直接使用相应的构造器来创建记录,如:

record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

p34 : Pair Nat Nat
p34 = 3 , 4

元变量(metavariables)

Agda 和其他类似的交互式证明系统(如 Coq)相比,一个显著的特性是在证明构造中对元变量的大量利用。

例如,在 Agda 中可以写出如下函数:

add :      
add x y = ?

“?”即是一个元变量。在 Emacs mode 中交互时,系统会提示用户所期望的类型,允许用户进一步添加具体代码到其中。该特性为渐进式程序构造提供了支持,从而达到与 Coq 的证明策略(tactics)类似的意图。

证明自动化和反射(reflection)

宇宙(universe)

高阶归纳类型(higher inductive types)

终止检查(termination checking)

作为一个定理证明系统,Agda 语言中的定义必须是完整(total)的。所有的程序必须终止,所有的模式必须得到匹配。若无法保证定义的完整性,其类型论背后所对应的逻辑将失去一致性,导致假命题可以被证明。

目前 Agda 使用 Foetus 终止检查器。

Unicode

Agda 语言大量吸收了 Unicode 字符集中的数学符号,这使得其证明更具可读性。Agda 的 Emacs mode 中提供了输入这些符号的快捷键;这仿照 TeX 中书写数学符号的形式。例如,输入 Σ 可以使用 \Sigma

标准库

Agda 的标准库包含了一些常见数据结构的定义和相关的定理证明,例如自然数、列表(lists)与矢量(vectors)。

编译器

Agda 目前具备两个官方的编译器后端:编译到 Haskell 的 MAlonzo 后端;和另一个编译到 JavaScript 的后端。


参见

参考文献

  1. ^ Release 2.6.4.3. 2024年3月6日 [2024年3月19日]. 
  2. ^ Agda license file. [2020-01-08]. (原始内容存档于2022-04-26). 
  3. ^ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [1]页面存档备份,存于互联网档案馆
  4. ^ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
  5. ^ Coquand, Catarina; Synek, Dan; Takeyama, Makoto. An Emacs interface for type directed support constructing proofs and programs (PDF). European Joint Conferences on Theory and Practice of Software 2005. [2013-12-24]. (原始内容 (PDF)存档于2011-07-22). 

外部链接

Read more information:

West Virginia Route 15Route informationMaintained by WVDOHLength64.1 mi[1] (103.2 km)Major junctionsWest end WV 4 near SuttonMajor intersections WV 20 in DianaEast end US 219 / WV 55 in Valley Head LocationCountryUnited StatesStateWest VirginiaCountiesBraxton, Webster, Randolph Highway system West Virginia State Highway System Interstate US State ← WV 14→ WV 16 West Virginia Route 15 at Webster County Route 5–3 in Guardian…

Artikel ini sebatang kara, artinya tidak ada artikel lain yang memiliki pranala balik ke halaman ini.Bantulah menambah pranala ke artikel ini dari artikel yang berhubungan atau coba peralatan pencari pranala.Tag ini diberikan pada November 2022. Light Novel no Tanoshii Kakikataライトノベルの楽しい書き方 Novel ringanPengarangToru HondaIlustratorKasumu KirinoPenerbitGA BunkoTerbit15 Februari 2008 – sekarangVolume9 Film laga hidupSutradaraKenichi OmoriTayang4 Desember 2010Durasi80 me…

Villota del Duque localidad Villota del DuqueUbicación de Villota del Duque en España. Villota del DuqueUbicación de Villota del Duque en la provincia de Palencia.País  España• Com. autónoma  Castilla y León• Provincia  Palencia• Municipio Loma de UciezaUbicación 42°29′28″N 4°36′11″O / 42.491111111111, -4.6030555555556• Altitud 902 mPoblación 39 hab. (INE 2020)Código postal 34118[editar …

Kwartir Daerah Sumatera Barat Lambang Kwartir daerah Sumatera Barat Pimpinan • Mahyeldi (Kamabida)• Audy Joinaldy (Kakwarda) Negara  Indonesia Kantor Jalan Pramuka Raya, Kelurahan Lolong Belanti, Padang Utara, Padang, Sumatera Barat 25135. Bumi perkemahan Padang Besi, Lubuk Kilangan, Padang Website www.pramukasumbar.com Gerakan Pramuka Kwartir Daerah 03 Sumatera Barat atau disingkat dengan Kwarda 03 Sumatera Barat, merupakan strukur organisasi Gerakan Pramuka Indonesia di tingkat Provin…

Biblioteca Pública de Chicago UbicaciónPaís  Estados UnidosLocalidad IllinoisDirección 400 South State Street, Chicago, IL 60605Coordenadas 41°52′35″N 87°37′42″O / 41.8763, -87.6282Datos generalesTipo library district of the United States, biblioteca pública y sistema de bibliotecasFundación 1873[editar datos en Wikidata] Harold Washington Library, la biblioteca central. La Biblioteca Pública de Chicago (en idioma inglés: Chicago Public Library, C…

この項目では、1970年に登場した2600系電車について説明しています。1940年に製造された初代2600形については「参宮急行電鉄2200系電車」をご覧ください。 共通事項基本情報製造所 近畿車輛主要諸元軌間 1,435 mm電気方式 直流1,500 V(架空電車線方式)最高運転速度 110 km/h車体長 20,720 mm全高 4,150 mm車体 普通鋼駆動方式 WNドライブ制御装置 抵抗制御制動装置 電磁直通ブレーキ …

Chan Santokhi Volledige naam Chandrikapersad Santokhi Geboren 3 februari 1959 Geboorteplaats Lelydorp Kieskring Wanica Land Suriname Functie President van Suriname Sinds 16 juli 2020 Voorganger Desi Bouterse Partij VHP Religie Hindoeïsme Functies 2005-2010 Minister van Justitie en Politie 2010-2020 Lid van De Nationale Assemblée 2011-heden Voorzitter van de VHP 2020-heden President van Suriname Website Portaal    Politiek Suriname Chandrikapersad (Chan) Santokhi (Sarnami: चा…

Paroisse de Sainte-Anne Situation de Sainte-Anne dans le comté de Madawaska Administration Pays Canada Province Nouveau-Brunswick Subdivision régionale Madawaska Statut municipal District de services locaux Constitution 9 novembre 1966 Démographie Population 949 hab. (2011 ) Densité 2,6 hab./km2 Géographie Coordonnées 47° 24′ 36″ nord, 67° 51′ 00″ ouest Superficie 36 930 ha = 369,30 km2 Divers Langue(s) Français Fu…

Ingin KucariAlbum studio karya Conny DioDirilis1 Januari 1997Direkam1995-1996GenreHard Rock, Pop RockLabelMusic PlusKronologi Conny Dio Esok yang Ceria (1994)Esok yang Ceria1994 Ingin Kucari (1997) Do'a Seorang KekasihString Module Error: Match not foundString Module Error: Match not found Ingin Kucari adalah album musik karya Conny Dio. Dirilis tahun 1997. Daftar lagu Ingin Kucari, Teddy Sujaya Keadaan, Wisnu S. Cinta Putih, Anang Baru Kau Sadari, Dadang S. Manaf Jalan Panjang Berliku, Eren…

Species of carnivore Ring-tailed vontsira Montagne d'Ambre National Park Conservation status Least Concern (IUCN 3.1)[1] Scientific classification Domain: Eukaryota Kingdom: Animalia Phylum: Chordata Class: Mammalia Order: Carnivora Suborder: Feliformia Family: Eupleridae Genus: GalidiaI. Geoffroy Saint-Hilaire, 1837 Species: G. elegans Binomial name Galidia elegansSaint-Hilaire, 1837 Ring-tailed vontsira range Skull and dentition, as illustrated in Gervais' Histoire naturelle …

No debe confundirse con El Libro de Rutas y Reinos (al-Bakri). Mapa de Eurasia mostrando la red de comercio de los Radhanitas (hacia 870), tal cual es descrito por ibn Khordadbeh en El Libro de Rutas y Reinos. El Libro de Rutas y Reinos (en árabe: كتاب المسالك والممالك, Kitab al-w'al Masalik-Mamalik) es un texto geográfico del siglo IX escrito por el geógrafo persa Ibn Khordadbeh.[1]​ El libro describe las principales rutas comerciales del mundo mulsumán de la …

Château de LochesLoches, Indre-et-Loire, France Aerial view of the châteauChâteau de LochesCoordinates47°07′29″N 0°59′48″E / 47.124722°N 0.996667°E / 47.124722; 0.996667TypeCastleSite informationOwnerCommune of LochesOpen tothe publicYesConditionRuinsSite historyMaterialsStone The Château de Loches (also called Le Logis Royal de Loches) is a castle located in the département of Indre-et-Loire in the Loire valley in France; it was constructed in …

North KoreaFIBA zoneFIBA AsiaWorld ChampionshipsAppearancesNoneAsian ChampionshipsAppearances2 (2000, 2002)MedalsNone The North Korea women's national under-18 basketball team is a national basketball team of North Korea, administered by the Amateur Basketball Association of DPR of Korea.[1] It represents the country in international under-18 (under age 18) women's basketball competitions. See also North Korea portalSports portal North Korea women's national basketball team References ^ …

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Taokas people – news · newspapers · books · scholar · JSTOR (February 2023) (Learn how and when to remove this template message) Taokas peopleTaokan, TaokasTaokas men on the annual ceremony Khantian.Regions with significant populationsHsinchu, Miaoli, and Nantou i…

Shopping mall in Calgary, Alberta, Canada Marlborough MallA Marlborough Mall entranceLocationCalgary, Alberta, CanadaCoordinates51°03′17″N 113°58′42″W / 51.05472°N 113.97833°W / 51.05472; -113.97833Address3800 Memorial Drive NEOpening dateNovember 1971ManagementPrimarisNo. of stores and services107No. of anchor tenants2 (1 open, 1 vacant)Total retail floor area53,032.5 m2 (570,837 sq ft)No. of floors1Websitemarlboroughmall.com Marlborough Mall i…

تومويوكي دان (باليابانية: 檀臣幸)‏  معلومات شخصية الميلاد 6 أغسطس 1963(1963-08-06)أوساكا الوفاة 10 أكتوبر 2013 (50 سنة)شينجوكو  مواطنة اليابان  الحياة العملية المهنة ممثل،  ومؤدي صوت  اللغات اليابانية  المواقع IMDB صفحته على IMDB  تعديل مصدري - تعديل   تومويوكي دان (檀臣幸 دا…

Private college This article does not cite any sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: De La Salle University College of Science – news · newspapers · books · scholar · JSTOR (June 2021) (Learn how and when to remove this template message) College of ScienceDalubhasaan ng AghamTypePrivateEstablished1982DeanDr. Mary Jane C. FloresAssociate DeanMs. Regi…

Human settlement in EnglandScapegoat HillView of the villageScapegoat HillLocation within West YorkshirePopulation1,246 OS grid referenceSE0884016430Metropolitan boroughKirkleesMetropolitan countyWest YorkshireRegionYorkshire and the HumberCountryEnglandSovereign stateUnited KingdomPost townHUDDERSFIELDPostcode districtHD7Dialling code01484PoliceWest YorkshireFireWest YorkshireAmbulanceYorkshire UK ParliamentColne Valley List of places UK England York…

For the village in Renfrewshire, Scotland, see Howwood. Human settlement in EnglandHow WoodAverage housing stock in How WoodHow WoodLocation within HertfordshirePopulation3,542 (2001 census)[1]OS grid referenceTL141036Civil parishSt StephenDistrictSt AlbansShire countyHertfordshireRegionEastCountryEnglandSovereign stateUnited KingdomPost townST ALBANSPostcode districtAL2Dialling code01727PoliceHertfordshireFireHertfordshireAmbulanceEast of England UK…

Baek Sung-dong Sepak bola Olimpiade, Korea versus Gabon. 2012Informasi pribadiTanggal lahir 13 Agustus 1991 (umur 32)Tempat lahir Korea SelatanPosisi bermain GelandangKarier senior*Tahun Tim Tampil (Gol)2012-2014 Júbilo Iwata 2015- Sagan Tosu * Penampilan dan gol di klub senior hanya dihitung dari liga domestik Baek Sung-dong (lahir 13 Agustus 1991) adalah pemain sepak bola asal Korea Selatan. Karier Baek Sung-dong pernah bermain untuk Júbilo Iwata dan Sagan Tosu. Pranala luar (Jepang) Pr…

Kembali kehalaman sebelumnya

Lokasi Pengunjung: 44.197.191.240