Coq
Στην επιστήμη υπολογιστών, το Coq είναι ένας διαλογικό εργαλείο απόδειξης θεωρημάτων (interactive theorem prover). Υποστηρίζει την έκφραση μαθηματικών βεβαιώσεων, ελέγχει μηχανικά αποδείξεις τους, βοηθά στην εύρεση τυπικών αποδείξεων και εξάγει ένα πιστοποιημένο πρόγραμμα (certified program) από μια κατασκευαστική απόδειξη των τυπικών προδιαγραφών του. Το Coq λειτουργεί στη θεωρία του λογισμού των επαγωγικών κατασκευών (calculus of inductive constructions), ο οποίος αποτελεί παράγωγο του λογισμού των κατασκευών (calculus of constructions). Το Coq δεν είναι αυτόματος αποδείκτης θεωρημάτων αλλά περιλαμβάνει τακτικές αυτόματης απόδειξης θεωρημάτων και διάφορες διαδικασίες απόφασης (decision procedures).
Το Coq υλοποιεί μια συναρτησιακή γλώσσα προγραμματισμού με εξαρτώμενους τύπους (dependent types).[1]
Αναπτύσσεται στη Γαλλία, στο εγχείρημα TypiCal (πρώην LogiCal), στο οποίο συμμετέχουν από κοινού το INRIA, η Πολυτεχνική Σχολή (École Polytechnique), το Πανεπιστήμιο Paris-Sud 11 και το CNRS. παλιότερα υπήρχε και μια ομάδα στην École Normale Supérieure de Lyon. Ο αρχηγός της ομάδας είναι ο Benjamin Werner. Το Coq υλοποιείται σε Objective Caml.
Η λέξη coq σημαίνει "κόκορας" στα Γαλλικά και προκύπτει από μια παράδοση ονομασίας των Γαλλικών ερευνητικών εργαλείων με ονόματα ζώων. Αποτελεί επίσης αναφορά στον Τιερί Κοκάν (Thierry Coquand), ο οποίος ανέπτυξε το λογισμό των κατασκευών με το Ζεράρ Υ (Gérard Huet). Αρχικά, ονομαζόταν απλά Coc, τα αρχικά των λέξεων "calculus of construction".
Θεώρημα τεσσάρων χρωμάτων και η επέκταση ssreflect
[Επεξεργασία | επεξεργασία κώδικα]Ο Georges Gonthier (από το Microsoft Research, στο Κέιμπριτζ της Αγγλίας) και ο Benjamin Werner (από το INRIA) χρησιμοποίησαν το Coq για να δημιουργήσουν μια απόδειξη του θεωρήματος τεσσάρων χρωμάτων, η οποία ολοκληρώθηκε το Σεπτέμβριο του 2004.[2]
Με βάση αυτή τη δουλειά, αναππτύχθηκε μια σημαντική επέκταση του Coq που ονομάστηκε Ssreflect (που σημαίνει "small scale reflection" ή "ανάκλαση μικρής κλίμακας"). Παρά το όνομα, τα πιο πολλά από τα νέα χαρακτηριστικά που προσθέτει στο Coq η Ssreflect είναι ιδιότητες γενικής χρήσης, που δεν είναι χρήσιμα μόνο για το στυλ υπολογιστικής ανάκλασης της απόδειξης.
Δείτε επίσης
[Επεξεργασία | επεξεργασία κώδικα]Αναφορές
[Επεξεργασία | επεξεργασία κώδικα]- ↑ A short introduction to Coq.
- ↑ «Development of theories and tactics: Four Color Theorem». Αρχειοθετήθηκε από το πρωτότυπο στις 22 Φεβρουαρίου 2007. Ανακτήθηκε στις 4 Νοεμβρίου 2010.
Εξωτερικοί σύνδεσμοι
[Επεξεργασία | επεξεργασία κώδικα]
- The Coq proof assistant - η επίσημη σελίδα (Αγγλικά)
- Cocorico!, το Coq Wiki[νεκρός σύνδεσμος] (Αγγλικά)
- MSR Inria math components - η επέκταση Ssreflect (Αγγλικά)
- The Coq'Art - Βιβλίο για το Coq από τους Yves Bertot και Pierre Castéran (Αγγλικά)