Loading AI tools
来自维基百科,自由的百科全书
Agda 是一個依賴類型的純函數式程式語言。目前的版本,Agda 2,最初由瑞典查爾摩斯工學院的 Ulf Norell 作為博士論文課題設計並實現[3]。先前的版本 Agda 1 由 Catarina Coquand 在 1999 年開發,而現今的版本則是對其的徹底重寫,因此可視作一個全新的語言,但保留了 Agda 的命名和傳統。
Agda 的類型系統體現了柯里-霍華德同構(Curry-Howard correspondence),因此亦可作為一個構建構造性證明的證明輔助工具。它的類型理論基於 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 語言。
用戶可通過 Emacs 或 Atom 編輯器的界面與 Agda 系統進行交互[5]。Agda 系統亦可藉由命令行單獨調用。
通過類型檢查的 Agda 程序可以被編譯到 Haskell,並由 GHC 編譯器最終編譯為可執行的本地機器碼;亦有編譯到 JavaScript 的後端實現。
Agda 的名字來自於一首由音樂家 Cornelis Vreeswijk 創作的瑞典語歌曲「Hönan Agda」,歌詞講述了一隻名叫 Agda 的母雞的故事。這實際上影射了 Coq(Coq 在法語中意為公雞)。
將下述程序保存於文件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
進行編譯。
幾點解釋:
import
子句導入。例如在上述程序中,open import IO
導入 Agda 標準庫中的IO(標準輸入輸出)模塊,並將其在當前作用域中打開。main : IO a
的模塊即可以被編譯成可執行文件。例如,上述程序中的main
函數作用是將字符串「Hello, World!」寫到標準輸出,之後退出程序。在 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})
,則是對一小於二的證明。
在類型論中,歸納和遞歸原則通常被用來證明涉及到歸納類型的定理。Agda 則使用依賴類型模式匹配來達到此目的。例如,自然數的加法可被定義為:
add zero n = n
add (succ m) n = succ (add m n)
比起運用歸納/遞歸原則,直接定義遞歸函數更加簡單直觀。依賴類型模式匹配是 Agda 內置的語言特性之一;其核心類型論並沒有包含歸納/遞歸原則。
除了歸納類型之外,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
Agda 和其他類似的交互式證明系統(如 Coq)相比,一個顯著的特性是在證明構造中對元變量的大量利用。
例如,在 Agda 中可以寫出如下函數:
add : ℕ → ℕ → ℕ
add x y = ?
「?」即是一個元變量。在 Emacs mode 中交互時,系統會提示用戶所期望的類型,允許用戶進一步添加具體代碼到其中。該特性為漸進式程序構造提供了支持,從而達到與 Coq 的證明策略(tactics)類似的意圖。
作為一個定理證明系統,Agda 語言中的定義必須是完整(total)的。所有的程序必須終止,所有的模式必須得到匹配。若無法保證定義的完整性,其類型論背後所對應的邏輯將失去一致性,導致假命題可以被證明。
目前 Agda 使用 Foetus 終止檢查器。
Agda 語言大量吸收了 Unicode 字符集中的數學符號,這使得其證明更具可讀性。Agda 的 Emacs mode 中提供了輸入這些符號的快捷鍵;這仿照 TeX 中書寫數學符號的形式。例如,輸入 Σ 可以使用 \Sigma
。
Agda 的標準庫包含了一些常見數據結構的定義和相關的定理證明,例如自然數、列表(lists)與向量(vectors)。
Agda 目前具備兩個官方的編譯器後端:編譯到 Haskell 的 MAlonzo 後端;和另一個編譯到 JavaScript 的後端。
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.