Coq

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

Στην επιστήμη υπολογιστών, το 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 είναι ιδιότητες γενικής χρήσης, που δεν είναι χρήσιμα μόνο για το στυλ υπολογιστικής ανάκλασης της απόδειξης.

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

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

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


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