Agda

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση
Απόσπασμα απόδειξης στο agda2

Το 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.

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

Εξωτερικοί σύνδεσμοι[Επεξεργασία | επεξεργασία κώδικα]

Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Agda (theorem prover) της Αγγλικής Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).