Agda

维基百科,自由的百科全书
跳转至: 导航搜索
Agda
编程范型 函数式编程
最新发行时间 2.4.2 / 2014年8月29日;18天前 (2014-08-29)
型態系統 静态类型, 强类型, 依赖类型
啟發語言 Coq, Epigram
作業系統 跨平台
許可證 参见LICENSE
常用文件扩展名 .agda, .lagda
網站 Agda wiki
一个Agda证明的片段

Agda是一个依赖类型函数式编程语言,同时亦可作为一个用于构建构造性证明证明辅助工具。Agda最早由瑞典查尔摩斯工学院的 Ulf Norell 设计并开发,作为他的博士论文课题[1]。目前的版本,Agda 2,则在第一版的基础上完全重写。

Agda体现了柯里-霍华德同构(Curry-Howard correspondence)。它的理论根基是 Zhaohui Luo 的UTT[2],该理论与 Per Martin-Löf直觉类型论相类似。

Agda与Coq的几点显著不同之处在于:它本身并不支持tactics;所有的证明均以函数式编程的方式书写;语言本身吸收了许多常规的程序语言元素,诸如:数据类型、模式匹配(pattern matching)、记录类型(records)、let表达式和模块(modules)等,而其语法则非常类似Haskell

Agda系统一般通过其提供的Emacs界面进行交互[3],亦可藉由命令行方式单独执行。

特性[编辑]

归纳类型[编辑]

在Agda中定义数据类型的形式与在其它非依赖类型的编程语言中定义代数数据类型相似。

例如,在Agda中定义皮亚诺数

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

这表示构造一个自然数有两种方式:zero 是一个自然数;若 n 是一个自然数,则 suc n 也必定是一个自然数。

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

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

第一处构造指出:zero 必定小于或等于任何自然数;第二处构造指出:当 n <= m 时必定有 (suc n) <= suc m。[4]

元变量[编辑]

Agda和其他类似的证明系统(如Coq)相比,一个显著的特性是程序构造中对元变量(metavariables)的大量使用。

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

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

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

标准库[编辑]

Agda的标准库包含了一些有用的数据结构、定义和相关的定理证明,例如自然数、list与vector。目前该标准库比起Coq尚欠成熟。

Unicode[编辑]

Agda大量吸收了Unicode字符集中的数学符号,这使得其证明更具可读性;但这同时也造成了键盘输入的不便。Agda的 Emacs mode 中提供了输入这些符号的快捷键。

编译器后端[编辑]

目前Agda具备三个编译器后端的实现:编译到Haskell平台的MAlonzo;一个编译到JavaScript的后端;以及一个Epic后端。

参考文献[编辑]

  1. ^ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf
  2. ^ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
  3. ^ Coquand, Catarina; Synek, Dan. An Emacs interface for type directed support constructing proofs and programs, European Joint Conferences on Theory and Practice of Software 2005. 
  4. ^ Nat from agda standard library. [07/20/2014]. 

外部链接[编辑]