Agda

Το Agda είναι βοηθός αποδείξεων (proof assistant), δηλ. ένα πρόγραμμα υπολογιστή που μπορεί να ελέγχει μαθηματικές αποδείξεις. Αποτελεί ένα διαλογικό σύστημα για την ανάπτυξη κατασκευαστικών αποδείξεων σε μια παραλλαγή της Ιντουισιονιστικής Θεωρίας Τύπων του Περ Μάρτιν-Λεφ (Per Martin-Löf). Μπορεί να θεωρηθεί γλώσσα συναρτησιακού προγραμματισμού με εξαρτώμενους τύπους. Το Agda αναπτύχθηκε από τον Ουλφ Νόρελ, μεταδιδακτορικό ερευνητή του Πανεπιστημίου Τεχνολογίας του Τσάλμερς (Chalmers University of Technology).

Agda

Γενικά
Ημερ. Δημιουργίας	2007
Είδος	συναρτησιακή γλώσσα προγραμματισμού, γλώσσα προγραμματισμού, ελεύθερο λογισμικό
Διανομή
Έκδοση	2.7.0.1 (12 Σεπτέμβριος 2024)
Λειτουργικά	Microsoft Windows, στυλ Unix
Ανάπτυξη
Γραμμένο σε	Haskell
Άδεια χρήσης	άδεια BSD
Σύνδεσμοι
Επίσημος ιστότοπος
https://wiki.portal.chalmers.se/agda/pmwiki.php
Αποθετήριο κώδικα
https://github.com/agda/agda

Το Agda βασίζεται στην ιδέα του απευθείας χειρισμού των όρων μιας απόδειξης, και όχι στις τακτικές (tactics): μια απόδειξη είναι όρος, όχι σενάριο με τακτικές. Η γλώσσα έχει κλασικές προγραμματιστικές δομές, όπως οι τύποι δεδομένων και οι εκφράσεις ανάλυσής τους (case-expressions), οι υπογραφές (signatures) και οι εγγραφές (records), οι εκφράσεις let και οι μονάδες κώδικα (modules). Το σύστημα παρέχει μια διεπαφή για τον διορθωτή Emacs και μια γραφική διεπαφή, την Alfa.

Agda 2

Η τρέχουσα έκδοση του Agda, το Agda 2, αναπτύχθηκε στο Τσάλμερς από τον Ουλφ Νόρελ. Η σύνταξη έχει αλλάξει σε σχέση με το Agda 1 (αν και αναπτύσσονται και κάποια εργαλεία μετατροπής), με ένα χαρακτηριστικό που εισάγεται να είναι οι έμμεσες μεταβλητές (implicit variables), οι οποίες μπορούν να παραλειφθούν όταν προκύπτουν από τα συμφραζόμενα. Το Agda 2 χρησιμοποιεί εκτενώς το πρότυπο Unicode για πιο ευανάγνωστες αποδείξεις.

Το Agda 2 παρέχει είτε ένα εργαλείο της γραμμής εντολών, είτε ένα ισχυρό τρόπο εργασίας σε Emacs, που αναπτύχθηκε από το Μακότο Τακεγιάμα και το Νιλς Άντερς Ντάνιελσον.

Το Agda 2 είναι παρόμοιο με τη γλώσσα Epigram.

Αναφορές

• C. Coquand et al. An Emacs interface for type directed support constructing proofs and programs. ENTCS 2006. https://web.archive.org/web/20110722063632/https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf
• A. Abel, et al. Verifying Haskell Programs Using Constructive Type Theory, ACM SIGPLAN Workshop Haskell'05, Tallinn, Estonia, 30 September 2005 http://www.tcs.informatik.uni-muenchen.de/~abel/haskell05.pdf Αρχειοθετήθηκε 2008-11-21 στο Wayback Machine.
• M. Benke et al. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10(4):265-289, 2003. https://web.archive.org/web/20060506031858/http://www.cs.chalmers.se/~marcin/Papers/universes.pdf
• T. Coquand et al. Connecting a Logical Framework to a First-Order Logic Prover. FroCos 2005, pp. 285-301. http://www.cse.chalmers.se/~ulfn/papers/fol.pdf

Εξωτερικοί σύνδεσμοι

• Η σελίδα του Agda 2 (ένα wiki), περιλαμβάνει τεκμηρίωση και σύνδεσμο προς εργαλείο αναφοράς σφαλμάτων (Αγγλικά)
• Η σελίδα της 1ης έκδοσης του Agda (Αγγλικά)