Agda ist eine abhängig typisierte, rein funktionale Programmiersprache und zugleich ein Proof Assistant (Beweisassistent). Sie basiert auf der intuitionistischen Typentheorie von Per Martin-Löf. Der Ursprung liegt an der Chalmers University of Technology (Göteborg): Das ursprüngliche System entwickelte Catarina Coquand ab 1999, die heutige Version Agda 2 stammt aus der Dissertation von Ulf Norell (2007). Agda wird in der konstruktiven Mathematik und bei der formalen Verifikation eingesetzt.
Erste Schritte
agda Datei.agda # Typcheck einer Datei
agda --interactive Datei.agda # Interaktiver Modus (Emacs)
agda-mode # Emacs-Modus starten
c-c c-l # Load: Datei laden und prüfen
c-c c-t # Goal/Typ anzeigen
c-c c-c # Case split: Fallunterscheidung erzeugen
c-c c-a # Auto: Beweisversuch suchen (Auto-Suche)
agda --version # Version anzeigenKernkonzepte
- Dependent Types: Typen können von Werten abhängen; man schreibt Programme und Beweise in derselben Sprache (Curry-Howard-Korrespondenz).
- Interaktive Entwicklung: In Emacs entwickelt man Beweise schrittweise mit Goal-Anzeige, Case Splits und Lücken (
?). - Termination Checking: Agda akzeptiert nur terminierende Funktionen und vollständige Pattern-Matches — so bleiben Typen konsistent.
- Universe: Typen leben in Hierarchien (
Set,Set₁,Set₂, …), um Paradoxien zu vermeiden.
Praxis-Tipps
- Mit
cubical(Cubical Agda) lassen sich höhere induktive Typen und Homotopietypentheorie direkt ausdrücken. - Bibliotheken wie
agda-stdlibliefern fertige Beweise zu Zahlen, Listen und Relationen. - Beispiel:
data Nat : Set where zero : Nat; suc : Nat -> Natdefiniert die natürlichen Zahlen induktiv. - Beweise werden wie Funktionen geschrieben: Der Typ
1 + 1 ≡ 2ist ein Datentyp, dessen Konstruktor (der Beweis) gesucht wird.
Verwandte Grundlagen: Idris-Befehle, Coq-Befehle, Haskell-Befehle (Agda teilt mit Haskell die syntaktische Tradition).