Agda
Niet te verwarren met Ada (programmeertaal).
Agda is een afhankelijk getypeerde functionele programmeertaal, oorspronkelijk ontwikkeld door Ulf Norell aan de Technische Universiteit Chalmers. Agda is niet Turingvolledig.
| Agda | ||||
|---|---|---|---|---|
| Paradigma | zuiver functioneel programmeren | |||
| Verschenen | 2007 (16 jaar) | |||
| Ontworpen door | Ulf Norell, Catarina Coquand | |||
| Ontwikkeld door | Ulf Norell, Catarina Coquand | |||
| Huidige versie | 2.6.4.3 (6 maart 2024)[1] 
| |||
| Typesysteem | sterke typering, manifest typering, afhankelijke typering, statisch typesysteem, nominatief typesysteem, type-inferentie | |||
| Beïnvloed door | Coq, Epigram, Haskell | |||
| Invloed op | Idris (programmeertaal) | |||
| Besturingssysteem | Platform-onafhankelijke software | |||
| Licentie | BSD-licentie | |||
| Bestandsextensies | agda, lagda
| |||
| Website | (en) Projectpagina | |||
| ||||
Agda is een bewijsassistent gebaseerd op het propositions-as-types paradigma, maar heeft in tegenstelling tot Coq geen aparte tactiektaal. Bewijzen worden geschreven in een functionele programmeerstijl. De taal heeft gebruikelijke programmeerconstructies zoals datatypes, pattern matching, records, let expressies en modules, en een Haskell-achtige syntaxis. Het systeem heeft interfaces voor Emacs, Atom en VS Code, maar kan ook in batchmodus worden uitgevoerd vanaf de commandoregel.
Agda is gebaseerd op Zhaohui Luo's unified theory of dependent types (UTT), een typetheorie die lijkt op de Martin-Löf typetheorie.
Kenmerken bewerken
Metavariabelen bewerken
Een van de onderscheidende kenmerken van Agda, vergeleken met andere vergelijkbare systemen zoals Coq, is de grote afhankelijkheid van metavariabelen voor programmaconstructie. Je kunt bijvoorbeeld functies als deze schrijven in Agda:
add : ℕ → ℕ → ℕ
add x y = ?
Hier is ? een metavariabele. Bij interactie met het systeem in emacs-modus wordt het verwachte type aan de gebruiker getoond en kan deze de metavariabele verfijnen, d.w.z. vervangen door meer gedetailleerde code. Deze functie maakt incrementele programmaconstructie mogelijk op een manier die vergelijkbaar is met bewijsassistenten gebaseerd op tactieken, zoals Coq.
Termination checking bewerken
Agda is een totale functionele programmeertaal. Dat wil zeggen dat elk programma moet eindigen en dat alle mogelijke patronen moeten worden gematched. Zonder deze eigenschap wordt de logica achter de taal inconsistent en wordt het mogelijk om willekeurige beweringen te bewijzen.
Bewijsautomatisering bewerken
Programmeren in pure typetheorie brengt veel vervelende en repetitieve bewijzen met zich mee. Hoewel Agda geen aparte tactiektaal heeft, is het mogelijk om nuttige tactieken in Agda zelf te programmeren. Typisch werkt dit door een Agda-functie te schrijven die optioneel een bewijs van een interessante eigenschap retourneert. Een tactiek wordt dan geconstrueerd door deze functie uit te voeren tijdens typechecking.
Daarnaast heeft Agda ondersteuning voor automatisering via reflectie, om complexere tactieken te schrijven. Het reflectiemechanisme maakt het mogelijk om programmafragmenten te quoten in - of te unquoten uit - de abstracte syntaxisboom. De manier waarop reflectie wordt gebruikt is vergelijkbaar met de manier waarop Template Haskell werkt.
Unicode bewerken
Een van de meest opmerkelijke kenmerken van Agda, is een sterke afhankelijkheid van Unicode in de programmabroncode. De standaard emacs-modus gebruikt snelkoppelingen voor invoer, zoals \Sigma voor Σ.
Bronnen, noten en/of referenties
|