.
Το Agda είναι βοηθός αποδείξεων (proof assistant), δηλ. ένα πρόγραμμα υπολογιστή που μπορεί να ελέγχει μαθηματικές αποδείξεις. Αποτελεί ένα διαλογικό σύστημα για την ανάπτυξη κατασκευαστικών αποδείξεων σε μια παραλλαγή της Ιντουισιονιστικής Θεωρίας Τύπων του Περ Μάρτιν-Λεφ (Per Martin-Löf). Μπορεί να θεωρηθεί γλώσσα συναρτησιακού προγραμματισμού με εξαρτώμενους τύπους. Το Agda αναπτύχθηκε από τον Ουλφ Νόρελ, μεταδιδακτορικό ερευνητή του Πανεπιστημίου Τεχνολογίας του Τσάλμερς (Chalmers University of Technology).
Το 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/ f
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
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/
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 (Αγγλικά)
Hellenica World - Scientific Library
Από τη ελληνική Βικιπαίδεια http://el.wikipedia.org . Όλα τα κείμενα είναι διαθέσιμα υπό την GNU Free Documentation License
