The Deep Link που εξισώνει τα μαθηματικά αποδείξεις και τα προγράμματα υπολογιστών | Περιοδικό Quanta

Ορισμένες επιστημονικές ανακαλύψεις έχουν σημασία επειδή αποκαλύπτουν κάτι νέο - τη διπλή ελικοειδή δομή του DNA, για παράδειγμα, ή την ύπαρξη μαύρων οπών. Ωστόσο, ορισμένες αποκαλύψεις είναι βαθιές επειδή δείχνουν ότι δύο παλιές έννοιες, που κάποτε θεωρούνταν διαφορετικές, είναι στην πραγματικότητα ίδιες. Πάρτε τις εξισώσεις του James Clerk Maxwell που δείχνουν ότι ο ηλεκτρισμός και ο μαγνητισμός είναι δύο όψεις ενός μεμονωμένου φαινομένου ή η σύνδεση της βαρύτητας της γενικής σχετικότητας με έναν καμπύλο χωροχρόνο.

Η αλληλογραφία Curry-Howard κάνει το ίδιο, αλλά σε μεγαλύτερη κλίμακα, συνδέοντας όχι μόνο ξεχωριστές έννοιες σε ένα πεδίο, αλλά ολόκληρους κλάδους: Πληροφορική και μαθηματική λογική. Επίσης γνωστός ως ισομορφισμός Curry-Howard (ένας όρος που σημαίνει ότι υπάρχει κάποιο είδος αντιστοιχίας ένα προς ένα μεταξύ δύο πραγμάτων), δημιουργεί μια σύνδεση μεταξύ μαθηματικών αποδείξεων και προγραμμάτων υπολογιστών.

Με απλά λόγια, η αλληλογραφία Curry-Howard υποστηρίζει ότι δύο έννοιες από την επιστήμη των υπολογιστών (τύποι και προγράμματα) είναι ισοδύναμες, αντίστοιχα, με προτάσεις και αποδείξεις - έννοιες από τη λογική.

Μια διακλάδωση αυτής της αντιστοιχίας είναι ότι ο προγραμματισμός - συχνά θεωρείται ως προσωπική τέχνη - ανυψώνεται στο εξιδανικευμένο επίπεδο των μαθηματικών. Η συγγραφή ενός προγράμματος δεν είναι απλώς «κωδικοποίηση», γίνεται πράξη απόδειξης ενός θεωρήματος. Αυτό επισημοποιεί την πράξη του προγραμματισμού και παρέχει τρόπους μαθηματικής αιτιολογίας σχετικά με την ορθότητα των προγραμμάτων.

Η αλληλογραφία πήρε το όνομά της από τους δύο ερευνητές που την ανακάλυψαν ανεξάρτητα. Το 1934, ο μαθηματικός και λογικός Haskell Curry παρατήρησε μια ομοιότητα μεταξύ των συναρτήσεων στα μαθηματικά και της υπονοούμενης σχέσης στη λογική, η οποία παίρνει τη μορφή δηλώσεων «αν-τότε» μεταξύ δύο προτάσεων.

Εμπνευσμένος από την παρατήρηση του Curry, ο μαθηματικός λογικός William Alvin Howard ανακάλυψε μια βαθύτερη σχέση μεταξύ υπολογισμού και λογικής το 1969, δείχνοντας ότι η εκτέλεση ενός προγράμματος υπολογιστή μοιάζει πολύ με την απλοποίηση μιας λογικής απόδειξης. Όταν εκτελείται ένα πρόγραμμα υπολογιστή, κάθε γραμμή «αξιολογείται» για να δώσει μία μόνο έξοδο. Ομοίως, σε μια απόδειξη, ξεκινάτε με σύνθετες προτάσεις που μπορείτε να απλοποιήσετε (αλείφοντας περιττά βήματα, για παράδειγμα, ή αντικαθιστώντας σύνθετες εκφράσεις με απλούστερες) μέχρι να καταλήξετε σε ένα συμπέρασμα — μια πιο συμπυκνωμένη και συνοπτική δήλωση που προέρχεται από πολλές ενδιάμεσες προτάσεις .

Ενώ αυτή η περιγραφή μεταφέρει μια γενική αίσθηση της αντιστοιχίας, για να την κατανοήσουμε πλήρως πρέπει να μάθουμε λίγο περισσότερα για αυτό που οι επιστήμονες υπολογιστών αποκαλούν «θεωρία τύπων».

Ας ξεκινήσουμε με ένα διάσημο παράδοξο: Σε ένα χωριό ζει ένας κουρέας που ξυρίζει όλους τους άντρες που δεν ξυρίζονται μόνοι τους και μόνο αυτούς. Ο κουρέας ξυρίζεται μόνος του; Εάν η απάντηση είναι ναι, τότε δεν πρέπει να ξυρίζεται μόνος του (γιατί ξυρίζει μόνο άντρες που δεν ξυρίζονται μόνοι τους). Εάν η απάντηση είναι όχι, τότε πρέπει να ξυριστεί μόνος του (γιατί ξυρίζει όλους τους άντρες που δεν ξυρίζονται μόνοι τους). Αυτή είναι μια άτυπη εκδοχή ενός παραδόξου που ανακάλυψε ο Μπέρτραντ Ράσελ προσπαθώντας να θεμελιώσει τα θεμέλια των μαθηματικών χρησιμοποιώντας μια έννοια που ονομάζεται σύνολα. Δηλαδή, είναι αδύνατο να ορίσετε ένα σύνολο που περιέχει όλα τα σύνολα που δεν περιέχουν τον εαυτό τους χωρίς να συναντήσετε αντιφάσεις.

Για να αποφύγουμε αυτό το παράδοξο, έδειξε ο Russell, μπορούμε να χρησιμοποιήσουμε «τύπους». Σε γενικές γραμμές, πρόκειται για κατηγορίες των οποίων οι συγκεκριμένες τιμές ονομάζονται αντικείμενα. Για παράδειγμα, εάν υπάρχει ένας τύπος που ονομάζεται "Nat", που σημαίνει φυσικούς αριθμούς, τα αντικείμενά του είναι 1, 2, 3 και ούτω καθεξής. Οι ερευνητές συνήθως χρησιμοποιούν άνω και κάτω τελεία για να δηλώσουν τον τύπο ενός αντικειμένου. Ο αριθμός 7, ακέραιου τύπου, μπορεί να γραφτεί ως "7: Ακέραιος". Μπορείτε να έχετε μια συνάρτηση που παίρνει ένα αντικείμενο του τύπου Α και φτύνει ένα αντικείμενο του τύπου Β ή μια συνάρτηση που συνδυάζει ένα ζεύγος αντικειμένων που ήταν τύπου Α και τύπου Β σε έναν νέο τύπο, που ονομάζεται "A × B".

Ένας τρόπος για να λυθεί το παράδοξο, επομένως, είναι να τεθούν αυτοί οι τύποι σε μια ιεραρχία, έτσι ώστε να μπορούν να περιέχουν μόνο στοιχεία ενός «κατώτερου επιπέδου» από τους ίδιους. Τότε ένας τύπος δεν μπορεί να συγκρατηθεί, γεγονός που αποφεύγει την αυτοαναφορικότητα που δημιουργεί το παράδοξο.

Στον κόσμο της θεωρίας τύπων, η απόδειξη ότι μια δήλωση είναι αληθής μπορεί να φαίνεται διαφορετική από ό,τι έχουμε συνηθίσει. Εάν θέλουμε να αποδείξουμε ότι ο ακέραιος αριθμός 8 είναι άρτιος, τότε το θέμα είναι να δείξουμε ότι το 8 είναι πράγματι ένα αντικείμενο συγκεκριμένου τύπου που ονομάζεται "Ζυγό", όπου ο κανόνας για τη συμμετοχή διαιρείται με το 2. Αφού επαληθεύσουμε ότι το 8 είναι διαιρετό με το 2, μπορούμε να συμπεράνουμε ότι το 8 είναι πράγματι «κάτοικος» του τύπου Even.

Οι Curry και Howard έδειξαν ότι οι τύποι είναι ουσιαστικά ισοδύναμοι με τις λογικές προτάσεις. Όταν μια συνάρτηση «κατοικεί» σε έναν τύπο — δηλαδή, όταν μπορείτε να ορίσετε με επιτυχία μια συνάρτηση που είναι αντικείμενο αυτού του τύπου — δείχνετε ουσιαστικά ότι η αντίστοιχη πρόταση είναι αληθής. Έτσι, οι συναρτήσεις που λαμβάνουν μια είσοδο τύπου A και δίνουν μια έξοδο τύπου B, που συμβολίζεται ως τύπος A → B, πρέπει να αντιστοιχούν σε μια υπονοούμενη: "Αν A, τότε B." Για παράδειγμα, πάρτε την πρόταση «Αν βρέχει, τότε το έδαφος είναι υγρό». Στη θεωρία τύπων, αυτή η πρόταση θα μοντελοποιηθεί από μια συνάρτηση με τον τύπο "Raining → GroundIsWet". Οι διατυπώσεις με διαφορετική εμφάνιση είναι στην πραγματικότητα μαθηματικά ίδιες.

Όσο αφηρημένη κι αν ακούγεται αυτή η σύνδεση, όχι μόνο άλλαξε τον τρόπο με τον οποίο οι επαγγελματίες των μαθηματικών και της επιστήμης υπολογιστών σκέφτονται για τη δουλειά τους, αλλά οδήγησε επίσης σε πολλές πρακτικές εφαρμογές και στους δύο τομείς. Για την επιστήμη των υπολογιστών, παρέχει μια θεωρητική βάση για την επαλήθευση λογισμικού, τη διαδικασία διασφάλισης της ορθότητας του λογισμικού. Πλαισιώνοντας τις επιθυμητές συμπεριφορές με όρους λογικών προτάσεων, οι προγραμματιστές μπορούν να αποδείξουν μαθηματικά ότι ένα πρόγραμμα συμπεριφέρεται όπως αναμένεται. Παρέχει επίσης μια ισχυρή θεωρητική βάση για το σχεδιασμό πιο ισχυρών λειτουργικών γλωσσών προγραμματισμού.

Και για τα μαθηματικά, η αλληλογραφία έχει οδηγήσει στη γέννηση του βοηθοί απόδειξης, που ονομάζονται επίσης διαδραστικοί αποδείκτες θεωρημάτων. Αυτά είναι εργαλεία λογισμικού που βοηθούν στη δημιουργία επίσημων αποδείξεων, όπως το Coq και το Lean. Στο Coq, κάθε βήμα της απόδειξης είναι ουσιαστικά ένα πρόγραμμα και η εγκυρότητα της απόδειξης ελέγχεται με αλγόριθμους ελέγχου τύπου. Οι μαθηματικοί έχουν επίσης χρησιμοποιήσει βοηθούς απόδειξης — ιδίως, τους Lean theorem prover — για την επισημοποίηση των μαθηματικών, η οποία περιλαμβάνει την αναπαράσταση μαθηματικών εννοιών, θεωρημάτων και αποδείξεων σε αυστηρή, επαληθεύσιμη από υπολογιστή μορφή. Αυτό επιτρέπει τον έλεγχο της μερικές φορές άτυπης γλώσσας των μαθηματικών από υπολογιστές.

Οι ερευνητές εξακολουθούν να διερευνούν τις συνέπειες αυτής της σχέσης μεταξύ μαθηματικών και προγραμματισμού. Η αρχική αλληλογραφία Curry-Howard συνδυάζει τον προγραμματισμό με ένα είδος λογικής που ονομάζεται διαισθητική λογική, αλλά αποδεικνύεται ότι περισσότεροι τύποι λογικής θα μπορούσαν επίσης να είναι επιδεκτικοί σε τέτοιες ενοποιήσεις.

«Αυτό που συνέβη στον αιώνα από τη διορατικότητα του Curry είναι ότι συνεχίζουμε να ανακαλύπτουμε όλο και περισσότερες περιπτώσεις όπου «το λογικό σύστημα Χ αντιστοιχεί στο υπολογιστικό σύστημα Υ», είπε. Μάικλ Κλάρκσον, επιστήμονας υπολογιστών στο Πανεπιστήμιο Cornell. Οι ερευνητές έχουν ήδη συνδέσει τον προγραμματισμό με άλλους τύπους λογικής όπως η γραμμική λογική, η οποία περιλαμβάνει την έννοια των «πόρων» και τη τροπική λογική, η οποία ασχολείται με τις έννοιες της δυνατότητας και της αναγκαιότητας.

Και ενώ αυτή η αλληλογραφία φέρει τα ονόματα του Curry και του Howard, σε καμία περίπτωση δεν είναι οι μόνοι που την ανακάλυψαν. Αυτό επιβεβαιώνει τη θεμελιώδη φύση της αλληλογραφίας: Οι άνθρωποι συνεχίζουν να την παρατηρούν ξανά και ξανά. «Δεν φαίνεται τυχαίο ότι υπάρχει μια βαθιά σύνδεση μεταξύ υπολογισμού και λογικής», είπε ο Clarkson.