Agda

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

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

Αναφορές

[Επεξεργασία | επεξεργασία κώδικα]

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

[Επεξεργασία | επεξεργασία κώδικα]
  1. ↑ «Release 2.7.0.1». 12 Σεπτέμβριος 2024. Ανακτήθηκε στις 20 Σεπτέμβριος 2024.