Agda (programming language)

From Wikipedia, the free encyclopedia
  (Redirected from Agda (theorem prover))
Jump to: navigation, search
Agda
Paradigm(s) Functional
Designed by Ulf Norell
Developer Ulf Norell
Appeared in 2007
Stable release 2.4.2.1 / November 15, 2014 (2014-11-15)
Influenced by Coq, Epigram, Haskell
Influenced Idris
OS Cross-platform
License See the LICENSE file
Filename extension(s) .agda, .lagda
Website [1]

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis.[1] The current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999.[2] The current version is a complete rewrite, which should be considered a new language that shares a name and tradition.

Agda, unlike Coq, has no support for tactics and proofs are written in functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has an Emacs interface[3] but can also be run in batch mode from the command line.

Agda is based on Luo's UTT[4] a type theory similar to Martin Löf type theory.

Features[edit]

Inductive types[edit]

The main way of defining data types in Agda is via inductive data types which are similar to algebraic data types in non dependently typed programming languages.

Here's a definition of Peano numbers in Agda:

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

Basically, it means that there are two ways to construct a natural number. Zero is a natural number, and if n is a natural number, then suc n is a natural number too.

Here's a definition of less than or equal relation:

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

The first constructor allows us to state that zero is less than or equal to any number. The second constructor states that if n <= m then (suc n) <= suc m.[5]

Dependently typed pattern matching[edit]

In core type theory, induction and recursion principles are used to prove theorems about inductive types. In agda, dependently typed pattern matching is used instead. For example, natural number addition can be defined like this:

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

This way of writing recursive functions/inductive proofs is more natural than applying raw induction principles. In agda, dependently typed pattern matching is a primitive of the language, the core language doesn't have induction/recursion principles which pattern matching translates to.

Metavariables[edit]

One of the distinctive features of agda, when compared with other similar systems such as coq, is heavy reliance on metavariables for program construction. For example, we can write function like this in agda:

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

? here is a metavariable. When interacting with the system in emacs mode, it will show the user expected type and allow them to refine the meta variable, i.e. to replace it with more detailed code. This feature allows incremental program construction in a way similar to tactics based proof assistants such as coq.

Proof Automation[edit]

Programming in pure type theory involves a lot of tedious and repetitive proofs and Agda doesn't have support for tactics. Agda has support for automation via reflection. The reflection mechanism allows to quote/unquote fragments of programs into/from abstract syntax tree. The way the reflection is used is similar to the way Template Haskell works.[6]

Another mechanism for proof automation is proof search action in the emacs mode. It renumerates possible proof terms (in no more than 5 second), and if one of the terms suits the specification, it will be put in the meta variable where the action is invoked. This action accepts hints, i.e. which theorems and from which modules can be used, whether the action can use pattern matching, etc.[7]

Termination Checking[edit]

Agda is a total language, i.e. each program in it must terminate. Without this feature, the logic behind the language becomes inconsistent, and it becomes possible to prove arbitrary facts. As a result, the language isn't Turing complete. For termination checking agda uses approach of the Foetus termination checker.[8]

Standard library[edit]

Agda has an extensive de facto standard library, which includes many useful definitions and theorems about basic data structures, such as natural numbers, lists, and vectors. The library is in beta, and is under active development.

Unicode[edit]

One of the more notable features of Agda is a heavy reliance on Unicode in program source code. The standard emacs mode uses shortcuts for input, such as "\Sigma" for Σ.

Backends[edit]

There are three compiler backends, MAlonzo which targets Haskell, a JavaScript backend, and an Epic backend.

References[edit]

  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. ^ "Agda: An Interactive Proof Editor". Retrieved 2014-10-20. 
  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.  |first3= missing |last3= in Authors list (help)
  4. ^ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
  5. ^ "Nat from agda standard library". Retrieved 2014-07-20. 
  6. ^ Van Der Walt, Paul, and Wouter Swierstra. "Engineering proof by reflection in Agda." In Implementation and Application of Functional Languages, pp. 157-173. Springer Berlin Heidelberg, 2013. http://hal.inria.fr/docs/00/98/76/10/PDF/ReflectionProofs.pdf
  7. ^ Kokke, Pepijn, and Wouter Swierstra. "Auto in Agda." http://www.staff.science.uu.nl/~swier004/Publications/AutoInAgda.pdf
  8. ^ Abel, Andreas. "foetus–termination checker for simple functional programs."Programming Lab Report 474 (1998). http://www.tcs.informatik.uni-muenchen.de/~abel/foetus.pdf

External links[edit]