ΔΙΑΠΡΑΓΜΑΤΕΥΟΜΕΝΟΙ ΤΗΝ ΑΡΙΘΜΗΤΙΚΗ,ΚΑΤΑΣΚΕΥΑΖΟΝΤΑΣ ΤΗΝ ΑΠΟΔΕΙΞΗ

ΔΙΑΠΡΑΓΜΑΤΕΥΟΜΕΝΟΙ ΤΗΝ ΑΡΙΘΜΗΤΙΚΗ, ΚΑΤΑΣΚΕΥΑΖΟΝΤΑΣ ΤΗΝ ΑΠΟΔΕΙΞΗ

Donald MacKenzie

Τα συστήματα πληροφορικής υπήρξαν αντικείμενο αυξημένου ενδιαφέροντος για τους κοινωνιολόγους από τη δεκαετία του 1960. Η ακτινοβολία τους, τα πιθανά αποτελέσματά τους στις επιχειρήσεις, στα επίπεδα της εργασιακής απασχόλησης και στην κοινωνία γενικότερα, η εξέλιξη της βιομηχανίας της τεχνολογίας – αυτά και άλλα θέματα έχουν λάβει ιδιαίτερη προσοχή. Τα συστήματα Πληροφορικής ως μαθηματικές οντότητες έχουν, ωστόσο, παραμείνει σχεδόν αποκλειστικά στην δικαιοδοσία των τεχνικών ειδικών. Εδώ θα ήθελα να αποκαταστήσω την ισορροπία ισχυριζόμενος ότι τα συστήματα πληροφορικής προσφέρουν ενδιαφέρουσες και ακριβείς μελέτες δεδομένων πάνω στην κοινωνιολογία των μαθηματικών.

Δύο διαφορετικές διαστάσεις των συστημάτων πληροφορικής ως μαθηματικών οντοτήτων θα αναλυθούν παρακάτω. Η πρώτη είναι ο υπολογιστής (και το προηγμένο digital κομπιουτεράκι) ως εργαλείο αριθμητικής. Η διαίσθηση ίσως να υποδηλώνει οτι η αριθμητική που πραγματοποιείται από κομπιουτεράκι ή από υπολογιστή θα ήταν χωρίς κανένα πρόβλημα. Η αριθμητική, ούτως ή άλλως, είναι το απόλυτο παράδειγμα της ασφαλούς, αποδεκτής γνώσης και βέβαια το κομπιουτεράκι ή ο υπολογιστής απλώς μεταφέρουν την πλήξη και τη ροπή προς το λάθος των αριθμητικών πράξεων που γίνονται από τους ανθρώπους! Κι όμως. Όχι μόνο χρειάζεται αρκετή προσπάθεια, που κανονικά θεωρείται απόλυτα δεδομένη, για να πραγματοποιηθούν αριθμητικές πράξεις σωστά ακόμα και σε απλά κομπιουτεράκια (βλ. υπ. 1) ακόμα, πρέπει να υπάρχει αξιόλογη επιχειρηματολογία όσον αφορά στη φύση των αριθμητικών πράξεων που πρόκειται να γίνουν, τουλάχιστον όταν οι αριθμοί με τους οποίους πρόκειται να δουλέψει κανείς δεν είναι ακέραιοι. Διαφορετικές αριθμητικές πράξεις μέσω κομπιούτερ έχουν προταθεί, και η κοντινότερη στρογγυλοποίηση προς μία αποδεκτή αριθμητική πράξη από κομπιούτερ, το στάνταρντ για αριθμητική κινητής υποδιαστολής Ινστιτούτο για Ηλεκτρολόγους και Ηλεκτρονικούς Μηχανολόγους, έπρεπε να διαπραγματευθεί, παρά να αφαιρεθεί από τις υπάρχουσες ανθρώπινες αριθμητικές πράξεις.

Η δεύτερη διάσταση των συστημάτων πληροφορικής που θα αναφερθεί εδώ είναι η μαθηματική απόδειξη της ορθότητας ενός προγράμματος ή ενός σχεδιασμού φυσικού εξαρτήματος υπολογιστή (hardware). Καθώς τα κομπιούτερς χρησιμοποιούνται ολοένα και περισσότερο σε περιστάσεις όπου η εθνική ασφάλεια και η ανθρώπινη ζωή εξαρτώνται από αυτά, έχει υπάρξει αυξημένη ζήτηση για τέτοιου είδους μαθηματικές αποδείξεις στη θέση του, ή πρόσθετα προς, τον εμπειρικό έλεγχο. Αυτό παρουσιάζει ενδιαφέρον από την κοινωνιολογική πλευρά της γνώσης διότι μετακινεί την απόδειξη από τον κόσμο των μαθηματικών και των επιστημόνων της λογικής σε εκείνο των μηχανολόγων, των επιχειρήσεων και των δικηγόρων.

Αν και η μαθηματική απόδειξη αναζητείται ακριβώς λόγω της σιγουριάς που θεωρείται οτι προσδίδει, το να κατασκευάζεις αποδείξεις της ορθότητας των υπολογιστών αποδεικνύεται επίσης οτι δεν είναι απλή “εφαρμογή” των μαθηματικών. Περιλαμβάνει τη διαπραγμάτευση του σε τι συνίσταται η απόδειξη. Το 1987, οι Peláez, Fleck και εγώ προβλέψαμε ότι η ζήτηση αποδείξεων της ορθότητας των συστημάτων πληροφορικής θα οδηγούσε αναπόφευκτα σε ένα επίσημο νομικό θέσπισμα σχετικά με τη φύση της μαθηματικής απόδειξης( βλ. υπ. 2). Αυτό το κεφάλαιο αναπτύσσει την ανάπτυξη της αμφισβήτησης η οποία οδήγησε στο γεγονός οτι αυτή η πρόβλεψη έχει σχεδόν φθάσει να επιβεβαιωθεί˙ επίσης ερευνά πιο γενικά θέματα της “κοινωνιολογίας της απόδειξης” στο πλαίσιο των υπολογιστών.

Διαπραγματευόμενοι την Αριθμητική

Η ανθρώπινη αριθμητική είναι ομόφωνα δεκτή και ανεπτυγμένη στις βιομηχανικές κοινωνίες. Τυπικά μπορεί να υπάρξει συμφωνία πάνω στο ορθό αποτέλεσμα οποιασδήποτε πράξης. Για παράδειγμα, όσο γνωρίζω δεν έχουν υπάρξει επιστημονικές διαφωνίες στις οποίες οι πλευρές έχουν διαφωνήσει ως προς το επίπεδο της αριθμητικής. Επιπλέον, υπάρχουν ορισμένοι “ιδανικοί” κανόνες που όλοι συμφωνούμε οτι πρέπει να ισχύουν, ανεξαρτητα από οποιαδήποτε συγκεκριμένη πράξη. Για παράδειγμα, όλοι συμφωνούμε οτι η πρόσθεση και ο πολλαπλασιασμός των πραγματικών αριθμών θα πρέπει να είναι τόσο αντιμεταθετική όσο και προσεταιριστική πράξη – οτι δηλ.,

α+β=β+α,

(α+β)+γ=α+(β+γ),

α* β=β* α,

και

(α* β) * γ=α* (β* γ)

οποιεσδήποτε κι αν είναι οι τιμές των α, β,και γ.

Η αποδεκτή κατάσταση της αριθμητικής πράγματι έχει ληφθεί ως υποδεικνύουσα ενός αυταπόδεικτου ορίου του αντικειμένου της κοινωνιολογίας της γνώσης( βλ. υπ 3). Ίσως φαίνεται οτι κάνει την εφαρμογή της αριθμητικής σε ένα κομπιουτεράκι ή σε έναν υπολογιστή ακριβή. Κι όμως αυτό δεν ισχύει.

Οι δυσκολίες είναι πιο έντονες στη μορφή της αριθμητικής η οποία χρησιμοποιείται στον τύπο της πράξης που βρίσκεται συνήθως στην επιστημονική εργασία: αριθμητική κινητής υποδιαστολής. Αυτό είναι το κομπιούτερ το ανάλογο προς τη γνωστή “επιστημονική σημειογραφία” για την έκφραση των αριθμών. Στην τελευταία, ο αριθμός εκφράζεται σε τρία τμήματα: ένα θετικό ή ένα αρνητικό σύμβολο (το πρώτο είναι συνήθως συνεπαγόμενο)˙ ένα σύνολο δεκαδικών στοιχείων (η βάση ή το δεκαδικό τμήμα του λογαρίθμου), συμπεριλαμβανομένου ενός δεκαδικού ψηφίου˙ και ένα ακόμη σύνολο δεκαδικών (τον εκθέτη), που είναι μία δύναμη του 10. Επομένως, το 1.245.000 θα μπορούσε να εκφραστεί σε “επιστημονική σημειογραφία” ως +1.245* 10^6, και το -0.0006734 ως –6.734* 10^-4. Το πλεονέκτημα της επιστημονικής σημειογραφίας είναι οτι επιτρέποντας στο δεκαδικό ψηφίο να “κινείται” κατ’ αυτόν τον τρόπο οδηγεί σε μια πιο οικονομική και εύχρηστη μορφή απ’ ότι η στάνταρ έκφραση, όπου το δεκαδικό ψηφίο είναι “σταθερό” στη θέση του.

Η αριθμητική κινητής υποδιαστολής του υπολογιστή κουβαλάει αυτήν την ευκαμψία, και μοιάζει αρκετά, εκτός από τις ακόλουθες πλευρές:

Η δεκαδική (με βάση το 10) αναπαράσταση τώρα είναι σπάνια˙ η δεκαεξαδική (με βάση το 16) και η διαδική (με βάση το 2) αναπαραστάσεις είναι πιο συνήθεις. Εφόσον το επεισόδιο το οποίο πρόκειται να αναφέρω αφορά τη διαδική αριθμητική, ας επικεντρωθούμε σε αυτό. Κάθε ψηφίο είναι είτε 1 είτε 0¨το δεκαδικό 3, για παράδειγμα, εκφράζεται ως 11, το δεκαδικό 4 ως 100 και ούτω καθ’ εξής. Ο δείκτης είναι μία δύναμη του 2, και το ισάξιο του δεκαδικού σημείου είναι γνωστό ως δυαδικό σημείο. Το πρόσημο, ομοίως, εκφράζεται ως δυαδικό ψηφίο, συνήθως με ένα 0 για θετικούς αριθμούς και ένα 1 για αρνητικούς αριθμούς( βλ υπ. 4).

Μία σίγουρη απόφαση πρέπει να παρθεί όσον αφορά στον αριθμό των δυαδικών αριθμών (ψηφίων) στην βάση και στο δείκτη. Στην αριθμητική που πρόκειται να αναφερθεί, η βασική μορφή(βλ. υπ. 5) έχει ένα δυαδικό ψηφίο το οποίο εκφράζει το πρόσημο, οκτώ για να εκφράζουν το δείκτη( βλ. υπ. 6), και 23 για να εκφράζουν τη βάση, σύνολο 32. (σχήμα 1). Ο συνολικός αριθμός των ψηφίων (που ορισμένες φορές καλείται “μήκος των λέξεων” είναι αρκετά σημαντικός, καθώς τα πιο εξελιγμένα κομπιούτερς προσπαθούν να επεξεργαστούν όλα τα ψηφία σχηματίζοντας έναν αριθμό παράλληλα αντί για το ένα μετά το άλλο. Όσο περισσότερα είναι τα ψηφία που πρόκειται να επεξεργαστούν ταυτόχρονα, τόσο μεγαλύτερη η πολυπλοκότητα των φυσικών εξαρτημάτων (hardware) που απαιτούνται.

Οποιοδήποτε σύστημα κινητής υποδιαστολής, εκτός εάν δέχεται περιορισμούς, επιτρέπει πολλαπλές αναπαραστάσεις του ίδιου αριθμού. Για παράδειγμα, το

-0.0006734 θα μπορούσε να εκφραστεί ως –67.34* 10^-5 καθώς και ως –6.734 * 10^-4. Τα συστήματα υπολογιστή κινητής υποδιαστολής, όμως, συνήθως περιλαμβάνουν μία μοναδική “κανονική” έκφραση κάθε αριθμού διαφορετικού από το μηδέν. Σε αυτή την αναπαράσταση, υπάρχει πάντα ένα ψηφίο διαφορετικό του μηδενός στα αριστερά του δυαδικού σημείου. Καθώς αυτό το ψηφίο πρέπει να είναι το 1, δε χρειάζεται να φυλάσσεται ιδιαιτέρως, και μόνο τα τμήματα της βάση στα δεξιά του δυαδικού αριθμού (γνωστού για ευνόητους λόγους ως κλάσμα) είναι σαφή.

Σχήμα 1

Αριθμητική αναπαράσταση σε ΙΕΕΕ αριθμητική κινητής υποδιαστολής. Πηγή: IEEE Standard for Binary Floating-Point Arithmetic, American National Standards Institute/Institute for Electrical and Electronics Engineers Standard 754-186 (Institute for Electrical and Electronics Engineers, 12 Αυγούστου, 1985), σελ. 9.

Υπάρχουν πολλές αποφάσεις, λοιπόν, οι οποίες πρέπει να ληφθούν όταν κανείς εφαρμόζει την αριθμητική κινητής υποδιαστολής σε υπολογιστή. Ποιά βάση θα χρησιμοποιηθεί; Ποιο μήκος λέξεων, ποιο μέγεθος βάσης, και ποιο μέγεθος δείκτη; Ένα ψηφίο πρόσημου 1 θα αντιπροσωπεύει αρνητικούς αριθμούς, ή θετικούς αριθμούς; Πώς θα εκφράζεται το μηδέν; Ποίες μέθοδοι στρογγυλοποίησης θα χρησιμοποιηθούν; Τι πρέπει να γίνει εάν το αποτέλεσμα της πράξης ξεπερνά τη μεγαλύτερη απόλυτη αξία που είναι δυνατόν να εκφραστεί στο σύστημα που έχει επιλεγεί (π.χ. εάν “υπερεκχειλίζει”), ή εάν βρίσκεται κάτω από τη μικρότερη (π.χ., εάν “υπερχειλίζει”); Τι πρέπει να γίνει εάν ένας χρήστης επιχειρήσει μία πράξη που μαθηματικά είναι χωρίς νόημα, όπως το να διαιρέσει το μηδέν με το μηδέν;

Διαφορετικοί κατασκευαστές υπολογιστών ( και έπειτα, καθώς έγινε δυνατό να εφαρμοστεί η αριθμητική κινητής υποδιαστολής στις ηλεκτρονικές αριθμομηχανές, διαφορετικοί κατασκευαστές υπολογιστών χειρός) απάντησαν σε αυτές τις ερωτήσεις με διαφορετικό τρόπο. Αυτό ήταν ολοφάνερα μια πηγή μιας πρακτικής δυσκολίας, καθώς καθιστούσε δύσκολο το να χρησιμοποιηθεί ένα πρόγραμμα αριθμών γραμμένο για έναν υπολογιστή σε έναν άλλο, ακόμα και όταν είχε χρησιμοποιηθεί μια δεδομένη γλώσσα προγραμματισμού όπως η Fortran. Αλλά μήπως είχε πιο βαθιά σημασία από αυτό; Τα αποτελέσματα των διαφόρων αποφάσεων ήταν πράγματι διαφορετικές αριθμητικές, ή ήταν απλώς διαφορετικοί αλλά βασικά ισάξιοι τρόποι εφαρμογής της μίας και αληθινής αριθμητικής;

Η απάντηση εξαρτιόταν από το πώς κανείς αντιδρούσε σε αυτό που μπορεί να ονομαστεί ανώμαλες πράξεις. Κάτω από κάποιες συνθήκες, διαφορετικά μηχανήματα αποδίδουν αρκετά διαφορετικά αποτελέσματα για την ίδια πράξη. Σε άλλες περιπτώσεις, η αριθμητική των μηχανημάτων παραβιάζει βασικές αρχές της ανθρώπινης αριθμητικής. Μικρές διαφοροποιήσεις ανάμεσα στα αποτελέσματα των ίδιων υπολογισμών που έχουν γίνει σε διαφορετικά μηχανήματα είναι συχνές, και ειδικοί στον τομέα μπορούν να δημιουργήσουν περιπτώσεις όπου τα αποτελέσματα διαφέρουν αρκετά. Ένας ειδικός αναφέρει ένα πρόβλημα επιτοκίου το οποίο παράγει τέσσερις διαφορετικές απαντήσεις όταν πραγματοποιείται σε κομπιουτεράκια τεσσάρων διαφορετικών τύπων: $331,667.00, $293,539.16, $334,858.18, και $331, 559.38. Διακρίνει μηχανές στις οποίες α/1 δεν ισούται με α (όπως πρέπει να είναι πάντοτε στην ανθρώπινη αριθμητική) και eπ – πe δεν ισούται με το μηδέν( βλ. υπ. 7).

Διαφορετικές αντιδράσεις σε ανώμαλες πράξεις πρέπει να κατηγοριοποιηθούν ανάλογα με το σχήμα που έχει αναπτυχθεί από τον Imre Lakatos στην περίφημη ανάλυσή του θεωρήματος του Euler σχετικά με τη σχέση ανάμεσα στα νούμερα των πλευρών (F), των άκρων (E), και των κορυφών (V) ενός πολύεδρου. Ο Lakatos έδειξε οτι απόπειρες να αποδειχθεί η σχέση V-E+F=2 παρεμποδίζονταν από παραδείγματα που κατέρριπταν τη θεωρία: αριθμούς που μπορούσαν να θεωρηθούν πολύεδρα αλλά οι οποίοι δεν συμφωνούσαν με τους κανόνες( βλ. υπ. 8)(. Μία αντίδραση σε αυτούς τους “ανώμαλους αριθμούς” ήταν αυτό που ο Lakatos καλεί “στοιχειώδες εξαιρούμενο”: απλή αδιαφορία για την ύπαρξή τους. Αυτή η αντίδραση χαρακτηρίζει καλά αυτό που φαίνεται οτι ήταν η πλειοψηφία σε ανώμαλους υπολογισμούς από κομπιούτερ ή κομπιουτεράκια. Οι περισσότεροι χρήστες πιθανότατα είτε αγνοούν τη δυνατότητα ύπαρξης ανώμαλων πράξεων είτε δεν ενδιαφέρονται για εκείνες κατά τον ίδια λογική που συνεχίζουμε να διασχίζουμε γέφυρες ακόμα κι αν γνωρίζουμε οτι κάποιες γέφυρες έχουν καταρρεύσει. Για πολλού σχεδιαστές υπολογιστών επίσης, οι ανώμαλοι υπολογισμοί φαίνεται οτι βρίσκονται πολύ χαμηλά στη λίστα των ζητημάτων που χρειάζονταν προσοχή, αν ήταν ποτέ μέσα σε αυτή τη λίστα.

Μια πιο εξελιγμένη στρατηγική “εξαίρεσης” ήταν να αναφερθεί ο τεράστιος αριθμός των πράξεων που πραγματοποιούνταν με απόλυτη επιτυχία, και να επιχειρηματολογηθεί οτι οι ανώμαλοι υπολογισμοί ήταν περιπτώσεις προβλημάτων που δεν είχαν “τεθεί σωστά”. Ένα πρόβλημα που είχε τεθεί σωστά ήταν ένα στο οποίο μία μικρή αλλαγή των δεδομένων προκαλούσε μόνο μια μικρή αλλαγή στο αποτέλεσμα˙ η λύση χρησιμοποιούσε έναν αλγόριθμο ο οποίος ήταν κατ’ αυτήν την έννοια “αριθμητικά σταθερός”. Η νεοδημιουργηθείσα τεχνική “αναδρομικής ανάλυσης των λαθών” χρησιμοποιήθηκε, για να δικαιολογηθεί αυτή η αντίδραση, για να γίνει διαχωρισμός μεταξύ των προβλημάτων που έχουν τεθεί σωστά και εκείνων που δεν είχαν τεθεί σωστά. Οι υπολογιστές και οι αριθμομηχανές δούλευαν σωστά σε προβλήματα που είχαν τεθεί σωστά. Εάν “παθολογικοί” υπολογισμοί και “εκφυλισμένα” προβλήματα αποφεύγονταν ( η χρήση αυτών των όρων θα μπορούσε να θεωρηθεί ως ενδεικτική του οτι η εξαίρεση έπεφτε σε αυτό που ο Lakatos ονομάζει τερατώδη-εξαίρεση), δεν θα δημιουργούνταν οποιεσδήποτε δυσκολίες(βλ. υπ. 9).

Ένας μικρός αριθμός επιστημόνων της πληροφορικής, όμως, επιζητούσε τα “τέρατα”( βλ. υπ. 10). Ένας ηγέτης μεταξύ τους ήταν ο Καθηγητής W. Kahan, ο οποίος ανήκει στο Μαθηματικό Τμήμα καθώς και στο Τμήμα Ηλεκτρολογικής Μηχανολογίας και Πληροφορικής Επιστήμης του Πανεπιστημίου της Καλιφόρνιας στο Μπέρκλεϋ. Η προσέγγιση του Kahan είναι ένα παράδειγμα αυτού που ο Lakatos καλεί “διαλεκτική” στρατηγική, ως προς το ότι “ανωμαλίες και αντικανονικότητες είναι ευπρόσδεκτες και θεωρούνται ως η δικαιολογία για νέες προσεγγίσεις, νέες αρχές, και νέες μεθόδους( βλ. υπ. 11). Πράγματι έχει παρατηρηθεί πολλές φορές στην ιστορία των επιστημών και ιδιαίτερα των μαθηματικών ότι τα κρίσιμα σημεία κάποιας θεωρίας εκεί δηλαδή που προκύπτουν ανωμαλίες και παράδοξα δημιουργούν νέες αφετηρίες για την επιστήμη ανάλογα και με την εκάστοτε αντιμετώπιση π.χ. εναλλακτική θεωρία συνόλων ,μη ευκλείδειες γεωμετρίες κ.α. O Kahan υπήρξε ένας μεταρρυθμιστής, δυσαρεστημένος με την παρούσα κατάσταση της αριθμητικής κινητής υποδιαστολής των υπολογιστών και των αριθμομηχανών και μονίμως προσπαθούσε να επινοήσει, και να δομήσει υποστήριξη για, τρόπους βελτίωσής της. Έχει ηθελημένα προσπαθήσει να ανακαλύψει και να κοινοποιήσει ανωμαλίες που μπορούν να χρησιμοποιηθούν για να δείξουν οτι οι διαφορές μεταξύ των μαθηματικών πράξεων που τελούνται από υπολογιστές είναι σοβαρές και επακόλουθες.

Αυτό που πρωτοέδωσε στον Kahan την ευκαιρία να ανασχηματίσει την αριθμητική προς την κατεύθυνση που επιθυμούσε ήταν ο ανταγωνισμός μεταξύ δύο ηγετικών κατασκευαστών εξελιγμένων αριθμομηχανών, της Texas Instruments και της Hewlett Packard. Η ΤΙ αμφισβήτησε την ακρίβεια των αριθμομηχανών της HP˙ Η ΗΡ αντέδρασε ισχυριζόμενη οτι οι υπολογισμοί με τα μηχανήματα των ανταγωνιστών της επεδείκνυαν περισσότερες ανωμαλίες. Ένα στέλεχος της Hewlett Packard, ο Dennis Harms, είδε ένα πλεονέκτημα στην προσπάθεια να ενδυναμώσει τη θέση της εταιρείας του από αυτήν την άποψη, και προσέλαβε τον Kahan ως σύμβουλο για το σχεδιασμό της αριθμητικής των αριθμομηχανών νέας γενιάς της εταιρείας του, επιτρέποντας κατ’ αυτόν τον τρόπο στον Kahan να συμπεριλάβει τις ιδέες του σε αυτές( βλ. υπ. 12).

Η επόμενη ευκαιρία για τον Kahan ήρθε γύρω στο 1977 όταν η ηγέτιδα εταιρεία μικροεπεξεργαστών, Intel, άρχισε να αναπτύσσει ένα τσιπ σιλικόνης ειδικά για να πραγματοποιεί αριθμητικές πράξεις κινητής υποδιαστολής. Οι υπάρχοντες μικροϋπολογιστές εφήρμοζαν την αριθμητική κινητής υποδιαστολής στα προγράμματα (software) αντί για τα φυσικά τμήματα των υπολογιστών τους (hardware), ενώ οι μονάδες κινητής υποδιαστολής στα μεγάλα κομπιούτερς ήταν πολύ-τσιπ. Το Intel i8087, όπως ονομάστηκε τελικά το τσιπ, προοριζόταν για “συνεπεξεργαστής κινητής υποδιαστολής” που θα λειτουργούσε ταυτόχρονα με το βασικό τσιπ επεξεργασίας σε ένα μικροϋπολογιστή για να βελτιώσει την αριθμητική του απόδοση.

Ο John Palmer, ο μηχανολόγος που ήταν υπεύθυνος για το σχεδιασμό του i8087, είχε παρακολουθήσει διαλέξεις του Kahan ως φοιτητής , και απευθύνθηκε σε εκείνον για συμβουλή(βλ. υπ. 13). O Palmer απέρριψε την ιδέα της υιοθέτησης “αριθμητικής IBM”, παρά την ευρεία χρήση της˙ ο Kahan θεωρούσε αυτή την αριθμητική υποδεέστερη. Η αριθμητική του ηγέτη κατασκευαστή μίνι-υπολογιστών, της Digital Equipment Corporation, απερρίφθη επίσης. Ο Palmer, ωστόσο, δεν επιζητούσε απλώς τη “διαφοροποίηση στο προϊόν”. Ανησυχούσε οτι εάν λαμβάνονταν λανθασμένες αποφάσεις θα ήταν αδύνατον να μοιραστούν κάποια προγράμματα μεταξύ “διαφορετικών κουτιών που θα έφεραν όλα το λογότυπο της Intel”, και ήθελε να αποφύγει την αριθμητική κινητής υποδιαστολής στους μικροεπεξεργαστές “τη χαοτική κατάσταση που υπάρχει τώρα στα mainframe και στα μίνι-κομπιούτερ περιβάλλοντα.”( βλ. υπ. 14)

H Intel και άλλοι κατασκευαστές τσιπ της Silicon Valley υποστήριξαν τη δημιουργία μιας επιτροπής που θα εξέταζε τα στάνταρντ για την αριθμητική κινητής υποδιαστολής. Η πρωτοβουλία για την επιτροπή είχε υπάρξει από ένα ανεξάρτητο σύμβουλο, τον Robert Stewart, ο οποίος ήταν ενεργό μέλος της Ένωσης Υπολογιστών του Ινστιτούτου Ηλεκτρολόγων και Ηλεκτρονικών Μηχανολόγων (ΙΕΕΕ), υπό την αιγίδα του οποίόυ ιδρύθηκε η επιτροπή. Ο Stewart πήρε στην επιτροπή τον Kahan και αντιπροσώπους της Intel, άλλων κατασκευαστών τσιπ, και μινικομπιούτερς. O Richard Delp ορίστηκε από τον Stewart ως πρώτος πρόεδρος του εργαζόμενου γκρουπ(βλ. υπ. 15). Η Intel – η οποία ήταν πολύ απασχολημένη με άλλες εργασίες – συμφώνησε να καθυστερήσει την ολοκλήρωση της αριθμητικής του i8087 ενώ η επιτροπή συσκέπτετο, αν και η Intel ξεκάθαρα ήλπιζε οτι το τελευταίο στάνταρντ θα ήταν παρόμοιο με εκείνο που είχαν ήδη δημιουργήσει.

Η διαπραγμάτευση της αριθμητικής απεδείχθη μια μακρά διαδικασία. Η επιτροπή ξεκίνησε τις εργασίες της το Σεπτέμβριο του 1977, και η ΙΕΕΕ Στάνταρντ 754, Δυαδική κινητής υποδιαστολής Αριθμητική, υιοθετήθηκε μόνο το 1985( βλ. υπ. 16). Η γενική φύση των επενδεδυμένων συμφερόντων που αναμειγνύονταν είναι ξεκάθαρη. Εάν η επιτροπή δεν έπαιρνε τον εύκολο δρόμο της γραφής ενός γενικού στάνταρντ που θα αποτελούσε πρόγονο όλων των υπαρχουσών αριθμητικών οι οποίες χρησιμοποιούνται ευρέως (μία περίπτωση που εξεταζόταν αλλά απερρίφθη), ή εάν δεν επέλεγε μία αριθμητική ριζικά διαφορετική από οποιαδήποτε υπάρχουσα, οτιδήποτε αποφάσιζε θα ήταν βέβαιο οτι θα ωφελούσε εκείνες τις εταιρείες των οποίων η υπάρχουσα πρακτική ήταν πιο κοντά στο στάνταρντ και θα περιόριζε εκείνες των οποίων η πρακτική διέφερε κατά πολύ από αυτό. Οι τελευταίες θα ωθούνταν σε μια δυσάρεστη επιλογή. Εάν διατηρούσαν την υπάρχουσα αριθμητική, η αγορά τους θα μπορούσε να μειωθεί ως αποτέλεσμα της προτίμησης από την πλευρά των χρηστών μηχανών που εφήρμοζαν το στάνταρντ. Εάν άλλαζαν, αρκετή επένδυση χρόνου και χρήματος θα έπρεπε να διαγραφεί, και ίσως να υπήρχαν ενοχλητικές ασυμβατότητες μεταξύ των νέων μηχανών τους και των παλαιών τους.

Τελικά η επιλογή κατέληξε σε δύο αριθμητικές αρκετά ευθυγραμμισμένες με βασικά εταιρικά συμφέροντα. Η μία ήταν βασικά η αριθμητική που εφαρμοζόταν από τη Digital Equipment Corporation (DEC), την ηγέτιδα κατασκευάστρια εταιρεία μίνι-υπολογιστών. Οι μηχανές VAX της DEX χρησιμοποιούνταν ευρύτατα στους επιστημονικόυς υπολογισμούς, και η αριθμητική τους γινόταν αποδεκτή ακόμα και από τους επικριτές της ως “έγκυρη” και “αξιοσέβαστη”( βλ. υπ. 17)(. Η άλλη ήταν μία αριθμητική που προτάθηκε από τον Kahan, το απόφοιτο μαθητή του Jerome Coonen, και τον Harold Stone, Διευθυντή Εξελιγμένων Αρχιτεκτονικών στο Εργαστήριο Yorktown Heights της ΙΒΜ. Δεν είναι διόλου παράξενο, δεδομένης της συνεργασίας μεταξύ του Kahan και του Palmer της Intel, το γεγονός οτι εκείνη η πρόταση έμοιαζε πολύ με εκείνη που η Intel ήταν ήδη έτοιμη να εφαρμόσει( βλ. υπ. 18).

Το σχήμα Kahan-Coonen-Stone έχει πολλά ενδιαφέροντα χαρακτηριστικά, όπως ο χειρισμός του μηδενός. Στη βασική μορφή τους επέλεξαν εκείνο που αποκαλείται ένα “κανονικοποιημένο μηδέν”. Το μηδέν εκφράζεται μόνο από μια μηδενική βάση και ένα μηδενικό δείκτη (0* 2^0). Ο συνδυασμός της μηδενικής significand και ενός μη μηδενικού δείκτη (0* 2^1, 0* 2^2, κλπ.) δεν επιτρέπεται. Αλλά επέτρεψαν στο ψηφίο του πρόσημου να λαμβάνει και τις δύο αξίες, και επέτρεψαν η αξία του να έχει νόημα. Με άλλα λόγια, η αριθμητική τους περιέχει ένα θετικό και ένα αρνητικό μηδέν, με, για παράδειγμα, τον κανόνα οτι η τετραγωνική ρίζα του –0 είναι –0( βλ. υπ. 19).

Αυτά και άλλα χαρακτηριστικά της αριθμητικής τους ήταν, ωστόσο, σχετικά μη αμφισβητήσιμα. Το πεδίο διαφωνίας ανάμεσα στην πρότασή τους και τη βασική εναλλακτική αριθμητική ήταν η υποροή Αντίθετα με την αριθμητική των πραγματικών αριθμών, όπου δεν υπάρχει κανένας αριθμός “δίπλα στο μηδέν” και αόριστα μικροί αριθμοί είναι πιθανοί, οι αριθμητικές των υπολογιστών περιέχουν ένα χαμηλότερο όριο, μολονότι πολύ μικρό, στο μέγεθος αριθμού που μπορεί να αντιπροσωπευτεί. Για παράδειγμα, 2^-126, ή περίπου 10^-38, είναι ο μικρότερος δυνατός αριθμός στην κανονική αναπαράσταση στη βασική μορφή του σχήματος των Kahan-Coonen-Stone. Όπως η πλειοψηφία των υπαρχόντων αριθμητικών των υπολογιστών, η αριθμητική DEC απλώς αναπαριστούσε όλους τους αριθμούς με τη μεγαλύτερη δυνατή ακρίβεια έως ότου προσεγγιζόταν ο αριθμός δίπλα στο μηδέν. Εάν η πράξη έδινε ένα αποτέλεσμα μικρότερο από αυτόν τον πολύ μικρό αριθμό, το αποτέλεσμα αποθηκευόταν ως μηδέν. Αυτό το σχήμα ονομαζόταν γενικά “πλήρης προς το μηδέν υποροή”

Ο Kahan και συνάδελφοί του υποστήριζαν τη διαφορετική αρχή της “σταδιακής υποροής”( βλ. υπ. 20). Εισήγαγαν ένα ειδικό σετ “ανωμαλοποιημένων αριθμών” μικρότερων σε μέγεθος από το συνήθους μορφής αριθμό δίπλα στο μηδέν. Όπως σημειώθηκε παραπάνω, στην κλασσικής μορφής κινητής υποδιαστολής αριθμητική το ψηφίο αριστερά του δυαδικού σημείου είναι πάντοτε 1. Σε ένα ανωμαλοποιημένο αριθμό είναι 0. Ανωμαλοποιημένοι αριθμοί δημιουργούνται μετακινώντας προς τα δεξιά την βάση ώστε ο εκθέτης παραμένει πάντοτε στα όρια του πεδίου που είναι δυνατόν να εκφραστεί. Σε ένα σύστημα όπου ο μικρότερος κανονικός αριθμός είναι το 2^-126, επομένως, το 2^-127 θα μπορούσε να δοθεί ανωμαλοποιημένη έκφραση ως ½ (0.1 στο δυαδικό) * 2^-126 ˙ ôο 2^-128 ως ¼ (0.01 στο δυαδικό) * 2^-126 και ούτω καθ’ εξής. Βεβαίως, αυτό σήμαινε οτι η ακρίβεια συνήθως χανότανε, καθώς ένα ή περισσότερα σημαντικά ψηφία θα έπρεπε να αποβληθούν κατά τη μεταφορά της βάσης προς τα δεξιά. Αλλά στους υποστηρικτές του φαινόταν ένα αποδεκτό τίμημα για μια πιο σταδιακή προσέγγιση του μηδενός. Το επιχείρημά τους απέναντι σε αυτό που ορισμένοι θεωρούσαν ως την “εμφανή” διαδικασία DEC, ήταν οτι χρησιμοποιώντας την τελευταία, καθώς ένας προσέγγιζε το μηδέν οι διαφορές μεταξύ διαδοχικών αριθμών λιγόστευαν έως ότου ένας πλησίαζε τον αριθμό δίπλα στο μηδέν, του οποίου η απόσταση από το μηδέν θα ήταν πολύ μεγαλύτερη από την απόστασή του από τον επόμενο μεγαλύτερο αριθμό. Στη διαδοχική υποροή οι διαφορές μεταξύ διαδοχικών αριθμών μειωνόταν μονοτονικά μέχρι το μηδέν (δες σχήμα 2).

Η σταδιακή υποροή έγινε το επίκεντρο των επιθέσεων προς την αριθμητική που πρότειναν οι Kahan, Coonen και Stone:

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

Σχήμα 2

Μικροί αριθμοί σε ροή προς το μηδέν και σταδιακή υποροή. Βασισμένο στο ”Underflow and denormalized numbers” του Jerome T. Coonen, Computers, Μάρτιος 1981, σελ. 77.

Δεν υπήρχε κανένας καθαρά εξαναγκαστικός τρόπος κατά τον οποίο ένα σχήμα θα μπορούσε να αποδειχθεί ανώτερο του άλλου. Οι υποστηρικτές του σχήματος Kahan-Coonen-Stone μπορούσαν να οδηγηθούν στο συμπέρασμα οτι οι ανωμαλίες που δημιουργούνταν, υποστήριζαν, από την ροή προς το μηδέν – ανωμαλίες που θα διορθώνονταν από τη σταδιακή υποροή:

Σκεφτείτε την απλή πράξη (Υ-Χ) + Χ όπου Υ-Χ υπορέει. Η σταδιακή υποροή πάντα δίνει ακριβώς Υ, η ροή προς το μηδέν δίνει Χ…. Θα μπορούσαμε να το δούμε ως ένα ακόμα μεμονωμένο παράδειγμα, αλλά προτιμώ να το δω ως τη διατήρηση του συσχετικού νόμου της πρόσθεσης του εντός στρογγυλοποίησης λάθους. Δηλαδή, κατά τη σταδιακή υποροή πάντοτε έχουμε (Υ-Χ) + Χ=Υ + (-Χ + Χ) στο εντός στρογγυλοποίησης λάθος. Αυτό είναι υποχρεωτικό, κατά τη γνώμη μου( βλ. υπ. 22).

Οι υπερασπιστές του πιο παραδοσιακού σχήματος DEC θα μπορούσαν, ωστόσο, να οδηγηθούν σε πιθανά προβλήματα με τη σταδιακή υποροή.

Ο πολλαπλασιασμός των ανωμαλοποιημένων αριθμών με αριθμούς μεγαλύτερους από το 1 (ή η διαίρεση με αριθμούς μικρότερους από το 1) μπορεί να δημιουργήσει σημαντικές ανακρίβειες. Εάν ένα τέτοιο γινόμενο (ή πηλίκο) βρίσκεται στη συνηθισμένη σειρά αριθμών, δεν μπορεί να αναπαρασταθεί σε ανωμαλοποιημένη μορφή, λόγω του κρυμμένου ψηφίου που χρησιμοποιείται στην KCS (αριθμητική των Kahan-Coonen-Stone). Ωστόσο, ο ανωμαλοποιημένος συντελεστής έχει λιγότερα (ίσως πολύ λιγότερα) από τον ενδεδειγμένο αριθμό ψηφία για το βαθμό ακριβείας του. Επομένως το γινόμενο (ή πηλίκο) θα μπορούσε στη χειρότερη περίπτωση να περιέχει μόνο ένα ισχύον ψηφίο. Η KCS ορίζει δύο μεθόδους αντιμετώπισης αυτού του προβλήματος. Η “προειδοποιητική μέθοδος” είναι υποχρεωτική: η αβάσιμη ένδειξη τίθεται, και ένα σύμβολο ΝαΝ (Νοt a Number : Δεν είναι Αριθμός) αποθηκεύεται για το αποτέλεσμα…Η άλλη μέθοδος, “ομαλοποίησε”, είναι προαιρετική: εάν υπάρχει, και επιλεγεί, το αποτέλεσμα που πιθανότατα είναι πολύ ανακριβές αποθηκεύεται ως κανονικός αριθμός, δεν τίθεται καμία ένδειξη, και, βέβαια, περαιτέρω παρακολούθηση του αποτελέσματος της αρχικής υποροής είναι αδύνατη( βλ. υπ. 23).

Από εκείνη τη στιγμή, μία εξαίρεση εσφαλμένης λειτουργίας εγείρεται όταν ένας ανωμαλοποιημένος αριθμός πολλαπλασιάζεται με μία αξία 2 ή μεγαλύτερη. Αλλά εάν το εξετάσουμε πιο λεπτομερώς, υπάρχουν ανωμαλοποιημένοι αριθμοί που βρίσκονται κοντά στην ανωμαλοποιημένη σειρά οι οποίοι έχουν πιο ακανόνιστη συμπεριφορά. Ο ανωμαλοποιημένος αριθμός ¾* 2^-126, για παράδειγμα, θα δημιουργήσει μία εξαίρεση εσφαλμένης λειτουργίας όταν πολλαπλασιαστεί με το 5, αλλά όχι όταν πολλαπλασιάζεται με το 6. Όταν πολλαπλασιάζεται με το 8 και πάλι θα δημιουργηθεί μία εξαίρεση…Αυτό το αποτέλεσμα δημιουργείται διότι η εξαίρεση για τον πολλαπλασιασμό συμβαίνει όταν προσπαθεί κάποιος να αποθηκεύσει έναν ανωμαλοποιημένο αριθμό σε μία βασική μορφή. Όταν πολλαπλασιάζουμε με το 8=1* 2^3, το αποτέλεσμα είναι ¾* 2^-123, τι οποίο είναι ανωμαλοποιημένο. Αλλά ο πολλαπλασιασμός με το 6=3/2* 2^2 δίνει 9/8* 2^-124, το οποίο είναι ομαλοποιημένο( βλ. υπ. 24).

Αυτές οι ενστάσεις θα μπορούσαν να εξαλειφθούν με τη σειρά τους:

Όπως κάθε νέο εργαλείο, είναι δυνατόν να γίνει λάθος χρήση της δυνατότητας και να υπάρξει δυσλειτουργία…Δεν πιστεύω οτι η δυνατότητα εισάγει δυσλειτουργίες σε διαδικασίες που προηγουμένως δούλευαν (με την ροή προς το μηδέν)( βλ. υπ. 25).

Η τάση των δύο αριθμητικών να προκαλούν σφάλματα και ανώμαλους υπολογισμούς δεν ήταν το μόνο ζήτημα που έπρεπε να εξεταστεί. Δεν υπήρχε, για παράδειγμα, αμφιβολία ότι η σταδιακή υποροή ήταν πιο πολύπλοκη να εφαρμοστεί από οτι η ροή προς το μηδέν επομένως, θα κόστιζε χρήματα και (ίσως) χρόνο από τις μαθηματικές πράξεις όπως ο πολλαπλασιασμός. Ίσως να έκανε το προτεινόμενο στάνταρντ δυσκολότερο να τηρηθεί, καθώς, δεδομένης της πολυπλοκότητάς του, οι κατασκευαστές ίσως να επέλεγαν να το εφαρμόσουν σε πρόγραμμα (software) αντί σε (φανερά παρόν ή απόν) φυσικό εξάρτημα υπολογιστή (hardware)( βλ. υπ. 26). Τέλος, το σχήμα της DEC είχε απλώς το τεράστιο πλεονέκτημα οτι ήταν βασικά ήδη εφαρμοσμένο στα πιο φημισμένα στον κόσμο ηλεκτρονικά μίνι-κομπιούτερ.

Επομένως, τίποτε επίσημο δεν εγγυόταν ότι το σχήμα των Kahan-Coonen-Stone θα κέρδιζε : όπως ακριβώς είπε ο καθηγητής Kahan “αυτό δεν ήταν ένα προκαθορισμένο συμπέρασμα”( βλ. υπ. 27). Υπέρ του ήταν η σύνθεση της εργαζόμενης ομάδας, τα γεγονότα της γεωγραφίας, και το στάτους του ως το πρώτο εν λειτουργία έγγραφο της ομάδας. Η Mary Payne της DEC που είχε ως έδρα τη Μασαχουσέτη σχολίασε:

Τα ενεργά (και εκλογικά) μέλη της Ενεργούς Ομάδας προέρχονται κατά βάση από κατασκευαστές μίνι-κομπιούτερ και ημιαγωγών, την Ακαδημία, και προμηθευτές φορητών προγραμμάτων (software). Ουσιαστικά δεν υπάρχει καμία συμμετοχή από Mainframe υπολογιστές και “απλούς χρήστες” – άτομα που γράφουν μόνα τους τα προγράμματα για προσωπική (ή των εργοδοτών τους) χρήση. Τα περισσότερα από τα ενεργά μέλη κατάγονται από την περιοχή του San Francisco Bay και όλα τα μίτινγκς, εκτός από ένα, έχουν γίνει σε αυτήν τη περιοχή( βλ. υπ. 28).

Άλλοι, ωστόσο, αναφέρουν την επιρροή της πειθούς και της δυνατής προσωπικότητας του Kahan. Ο ίδιος ο Kahan θεωρεί ως σημαντικές δύο επιδείξεις της τεχνολογικής δυνατότητας της σταδιακής υποροής (η Intel την εφήρμοσε στον κώδικα μικροπρογραμματισμού του πρώτου i8087, και ένας από τους μαθητές του Kahan, ο George Taylor, σχεδίασε μία πλακέτα υπολογιστή για το VAX της DEC το οποίο αναγνωρίστηκε οτι εφαρμόζει με επιτυχία τη σταδιακή υποροή) σε συνδυασμό με την αρμόδια υποστήριξη για σταδιακή υποροή που δόθηκε από έναν φημισμένο αναλυτή, τον Καθηγητή G. W. Stewart III του Πανεπιστημίου Maryland, ο οποίος στην πραγματικότητα είχε προσληφθεί για να ερευνήσει το θέμα από τη DEC.

Σε μια ανοιξιάτικη ψηφοφορία της επιτροπής το σχήμα των Kahan-Coonen-Stone έλαβε την απαραίτητη υποστήριξη για να υιοθετηθεί της πλειοψηφίας των δύο τρίτων. Το σχήμα τότε χρειάστηκε πολλά χρόνια για να περάσει από μεγαλύτερες επιτροπές του Ινστιτούτου Ηλεκτρολογικών και Ηλεκτρονικών Μηχανικών, αλλά τελικά ενεκρίθη από το Σώμα ΙΕΕΕ Στάνταρντ το Μάρτιο του 1985, και από το Αμερικάνικο Ινστιτούτο Εθνικών Στάνταρντ ως ANSI/IEEE ΣΤΑΝΤΑΡΤΝΤ 754 τον Ιούλιο του 1985.

Δεν είναι ένα παγκόσμιο στάνταρντ. Τα περισσότερα σούπερ-κομπιούτερς (όπως τα Crays), τα mainframes (όπως τα μηχανήματα της ΙΒΜ), και τα μίνι-κομπιούτερς (όπως τα VAX της DEC) δεν θεωρούνται συμβατά με αυτό. Παρ’ όλα αυτά, δεν έχει συμφωνηθεί κανένα ανταγωνιστικό συλλογικό στάνταρντ. Επομένως, υπάρχει ένας φαύλος κύκλος: καθώς το Στάνταρντ ΙΕΕΕ 754 γίνεται ευρύτερα γνωστό, τα προβλήματα που αφορούν στη μεταφορά αριθμητικών προγραμμάτων από το ένα μηχάνημα στο άλλο μειώνονται, και έτσι όλο και περισσότερα προγράμματα γράφονται έχοντας υπ’ όψιν το Στάνταρντ 754, αυξάνοντας τη δημοτικότητά του. Οι υποστηρικτές των νέων τεχνολογιών υιοθετούν το Στάνταρντ 754 ώστε οι χρήστες δεν πρέπει να ξαναγράψουν προγράμματα για να μεταφερθούν σε αυτές τις νέες τεχνολογίες (βλ. υπ. 29).

Αυτό που έχει συμβεί λοιπόν είναι μία έκδοση μιας μορφής “ολοκλήρωσης” τυπικής στην τεχνολογία. Σύμφωνα με τον Brian Arthur:

Πολύ συχνά, οι τεχνολογίες δείχνουν αυξανόμενη απόδοση της υιοθεσίας- όσο πιο πολύ υιοθετούνται τόσο πιο πολύ βελτιώνονται…Όταν δύο ή περισσότερες αυξανόμενης απόδοσης τεχνολογίες ανταγωνίζονται για ενστερνιστές, γεγονότα ασήμαντης “τύχης” μπορούν να δώσουν σε μία από τις τεχνολογίες ένα αρχικό αβαντάζ εφαρμογής. Τότε μεγαλύτερη εμπειρία αποκτάται με την τεχνολογία και επομένως βελτιώνεται; τότε υιοθετείται ακόμα πιο ευρέως, με αποτέλεσμα να βελτιώνεται ακόμα περισσότερο. Έτσι, η τεχνολογία που κατά “τύχη” κάνει ένα καλό ξεκίνημα μπορεί τελικά να μονοπωλήσει την αγορά των μελλοντικών ενστερνιστών, ενώ οι άλλες τεχνολογίες σταδιακά εκτοπίζονται (βλ. υπ. 30).

Υπάρχουν αυτοί που αρνούνται οτι αυτό που έχει θεσμοθετηθεί είναι η καλύτερη δυνατή αριθμητική( βλ. υπ. 31), και οι οποίοι πραγματικά θα απέδιδαν την εφαρμογή του στάνταρντ σε “τυχαία γεγονότα” παρά στην ουσιαστική αξία που οι θα ισχυρίζονταν οι υποστηρικτές του. Αυτή η διαφωνία, ωστόσο, τώρα είναι ουσιαστικά άσχετη: η ίδια η διαδικασία της θεσμοθέτησης του στάνταρντ του προσδίδει πρακτικά αβαντάζ που κάνουν απίθανη την ανατροπή του από κάποιο ανταγωνιστή.

Αποτελεί ειρωνεία το ότι μια επιλογή όπως αυτή που αναφέρθηκε και η οποία θα έπρεπε να περιμένει κάποιος ότι θα καθορίζεται από καθαρά ορθολογιστικά κριτήρια[μια και αφορά την επιλογή αριθμητικής αυτό θα ήταν και το αναμενόμενο] πέρα από τυχαίους και ‘’ασαφείς ‘’ παραγοντες,τελικα φαινεται να είναι αποτελεσμα γεγονότων που αφορούν την κοινωνιολογία την ψυχολογία και την καθαρή τύχη…Αυτό από μόνο του δείχνει το πώς οι έννοιες της τεχνολογίας, της επιστήμης και της κοινωνίας είναι αλληλοεπιρεαζομενες και πως η πορεία μιας τόσο νευραλγικής επιστήμης όπως η πληροφορική και η τεχνολογία των υπολογιστών μπορεί να καθοριστεί από οικονομικές ανάγκες της αγοράς που δεν μπορεί να μην ληφθεί υπ’οψιν.

Κατασκευάζοντας την απόδειξη

Όπως σημειώθηκε στο κεφάλαιο 7, έχει υποστηριχθεί με σημαίνοντα τρόπο οτι η πολυπλοκότητα των συστημάτων πληροφορικής περιορίζει το όριο στο οποίο ο εμπειρικός έλεγχος μπορεί να επιδείξει την ορθότητα του προγράμματος του υπολογιστή ή το σχέδιο του φυσικού εξαρτήματος του υπολογιστή. Εφόσον ο έλεγχος του προγράμματος φυσιολογικά δεν μπορεί να είναι ολοκληρωτικός, “μπορεί να είναι ένας πολύ αποτελεσματικός τρόπος επίδειξης της παρουσίας ελαττωμάτων, αλλά είναι τελείως ακατάλληλος για να επιδείξει την απουσία τους.”( βλ. υπ. 32) “Μαθηματικοποιώντας” επιστήμονες της πληροφορικής έχουν νιώσει οτι υπάρχει μόνο ένας σίγουρος τρόπος για το σχεδιασμό των προγραμμάτων ή των φυσικών εξαρτημάτων των υπολογιστών που είναι φανερά σωστές εφαρμογές των προδιαγραφών τους: επαγωγική, μαθηματική απόδειξη. “Ο μόνος αποτελεσματικός τρόπος να αυξηθεί σημαντικά το επίπεδο εμπιστοσύνης ενός προγράμματος είναι να δοθεί πειστική απόδειξη της ορθότητάς του( βλ. υπ. 33).

Μέχρι τη δεκαετία του 1980, αυτά τα επιχειρήματα που αρχικά ήταν σε ακαδημαϊκό επίπεδο, άρχιζαν να απασχολούν εκείνους που ήταν υπεύθυνοι για συστήματα υπολογιστών ιδιαίτερης σημασίας είτε για την εθνική ασφάλεια είτε για την ανθρώπινη ασφάλεια. Ο πρώτος ο οποίος έλαβε δράση πάνω σε αυτά ήταν το Αμερικάνικο Υπουργείο Αμύνης, το οποίο το 1983 θέσπισε τα Κριτήρια για την Αξιολόγηση Έμπιστων Συστημάτων Πληροφορικής, γνωστά από το χρώμα του εξώφυλλου του εγχειριδίου που τα περιείχε ως το “Πορτοκαλί Βιβλίο”. Το πορτοκαλί βιβλίο έθετε μια ιεραρχία κριτηρίων προς εφαρμογή σε συστήματα υπολογιστών που περιείχαν πληροφορίες κριτικής σημασίας για την εθνική ασφάλεια. Για να αποκτήσουν τη μεγαλύτερη αξιολόγηση-Συστήματα Κλάσης Α1 (“Ελεγμένο Σχέδιο”)- απαιτεί μαθηματική απόδειξη οτι το σχέδιο ενός συστήματος συμμορφώνεται με ένα επίσημό μοντέλο αυτού του οποίου δημιουργεί “ασφάλεια”( βλ. υπ. 34).

Στην Ευρώπη η ζήτηση για μαθηματική απόδειξη έχει ακουστεί πιο έντονα για συστήματα πληροφορικής κριτικής σημασίας για την ανθρώπινη ασφάλεια παρά για εκείνα που είναι κριτικής σημασίας για την εθνική ασφάλεια (αν και Ευρωπαϊκά κριτήρια χαλαρά ανάλογα προς το Πορτοκαλί Βιβλίο έχουν εκδοθεί). Το 1986 η Συμβουλευτική Επιτροπή Εφηρμοσμένης έρευνας και Ανάπτυξης του Βρετανικού Υπουργικού Γραφείου ζήτησε μαθηματική απόδειξη σε περίπτωση που συστήματα των οποίων η αποτυχία θα μπορούσε αν οδηγήσει πάνω από δέκα θανάτους, και το 1991 το Προσωρινό Στάνταρντ Αμύνης 00-55 απαιτούσε επίσημη μαθηματική απόδειξη οτι τα προγράμματα τα οποία ήταν πιο ζωτικής σημασίας για την ασφάλεια είναι ορθές εφαρμογές των προδιαγραφών τους( βλ. υπ. 35).

Σε τέτοια κείμενα, με εξαίρεση το πιο πρόσφατο (Στάνταρντ Αμύνης 00-55, το οποίο αναφέρεται παρακάτω), η έννοια της “απόδειξης” έχει τυπικά χρησιμοποιηθεί σαν το νόημά της να ήταν δίχως προβλήματα. Το 1987, ο Peláez, o Fleck κι εγώ θεωρήσαμε οτι αυτή η μη-προβληματική χρήση δεν θα επιβίωνε της εισόδου της απόδειξης στους εμπορικούς και ρυθμιστικούς τομείς. Προβλέψαμε οτι ίσως να μην περνούσε καιρός για να “πρέπει να αποφασίσει ένα δικαστήριο τι αποτελεί μία διαδικασία μαθηματικής απόδειξης( βλ. υπ 36). Αυτή η πρόβλεψη βασίστηκε στις θεωρίες της κοινωνιολογίας-της-κοινωνιολογία που παρατίθενται στο κεφάλαιο Ι και στην αξιοσημείωτη ποικιλία, η οποία αποκαλύπτεται από την ιστορία των μαθηματικών, με τις μορφές επιχειρημάτων που έχουν θεωρηθεί ουσιώδεις αποδείξεις. Για παράδειγμα, η Judith Grabiner έχει δείξει πως επιχειρήματα που ικανοποιούσαν τους μαθηματικούς του δέκατου όγδοου αιώνα απερρίφθησαν ως μη ουσιώδεις αποδείξεις από τους διαδόχους τους του δέκατου ένατου αιώνα, όπως είναι ο Cauchy ( βλ. υπ. 37). Εδώ γίνεται αναφορά για την ίδια την πορεία της επιστήμης στον χρονο,για την εξέλιξη της και την παράλληλη αλλαγή της άποψης που έχει η επιστημονική κοινότητα κάθε εποχής για το τι αποτελεί ‘’αλήθεια’’. Στην περίπτωση των μαθηματικών αυτό έχει καθοριστική σημασία για την τεχνολογία την επιστήμη και κατ’επεκταση τον ίδιο τον πολιτισμό μας μια που τα μαθηματικά είναι η λογική της επιστήμης Η πρόβλεψή μας βασιζόταν στην υπόθεση οτι προσπάθειες για να αποδειχθεί η ορθότητα του σχεδιασμού συστημάτων υπολογιστών θα έφερνε στο φως παρόμοιες διαφωνίες σχετικά με τη φύση της απόδειξης.

Μέχρι το 1991, η πρόβλεψη της αντιδικίας επιβεβαιώθηκε στη διαμάχη, που αναφέρθηκε στο κεφάλαιο 7, πάνω στο εάν η αλυσίδα των συλλογισμών- όπως ήταν τότε( βλ. υπ. 38)- που συνέδεε το σχεδιασμό του μικροεπεξεργαστή VIPER με την προδιαγραφή του, θα μπορούσε δίκαια να ονομαστεί “απόδειξη”. Μόνο η χρεοκοπία του αντίδικου Charter Technologies Ltd., εμπόδισε την υπόθεση να φθάσει στο δικαστήριο( βλ. υπ. 39).

Η διαφωνία πάνω στο VIPER δεν πρέπει να αντιμετωπιστεί ως ολοκληρωτικά sui generis (μοναδική) . Αυτό που ήταν (τουλάχιστον δυνητικά) σε διαφωνία δεν ήταν απλώς η κατάσταση μιας συγκεκριμένης αλυσίδας μαθηματικού συλλογισμού, αλλά και αυτό που πρέπει να θεωρηθεί οτι σημαίνει η μαθηματική “απόδειξη” - ένα ζήτημα που ξεκάθαρα φτάνει πέρα από τα δεδομένα αυτού του επεισοδίου. Αυτό θα είναι το επίκεντρο του υπόλοιπου κεφαλαίου.

Μία σημασία της “απόδειξης” αναφέρεται συνοπτικά από τον Robert Boyer και τον J. Strother Moore, οι οποίοι είναι βασικοί υποστηρικτές της χρήσης των συστημάτων πληροφορικής για την απόδειξη μαθηματικών θεωρημάτων (και συνάδελφοι δύο εκ των επικριτών της απόδειξης VIPER, του Bishop Brock και του Warren Hunt) ως εξής: “Μία τυπική μαθηματική απόδειξη είναι μία μετρήσιμη ακολουθία από φόρμουλες, εκ των οποίων το κάθε στοιχείο είναι είτε ένα αξίωμα είτε το αποτέλεσμα της εφαρμογής ενός από ένα δεδομένο σετ μηχανικών κανόνων σε προηγούμενες φόρμουλες στη σειρά( βλ. υπ. 40). Η εφαρμογή αυτού του κριτηρίου στο VIPER δεν αμφισβητήθηκε ποτέ δημόσια πριν ή κατά την αντιδικία. Παρατηρείται συνήθως το εξής σχήμα στην εφαρμογή της θεωρίας στην τεχνολογία, θεωρητικά μοντέλα να χρησιμοποιούνται από την έρευνα στο επίπεδο των τεχνολογικών εφαρμογών και βάση αυτών να δημιουργείται μια νέα τεχνολογία. Η χρησιμοποίηση αυτής της μορφής απόδειξης[μαθηματική απόδειξη μέσω συστήματος πληροφορικής] όταν αυτή καθεαυτή η μορφή δεν είναι αποδεκτή από το σύνολο της μαθηματικής κοινότητας και αποτελεί λοιπόν θέμα ερευνάς στο πεδίο των θεωρητικών μαθηματικών έρχεται να ανατρέψει αυτό το σχήμα και εξ ορισμού δημιουργεί προβλήματα. Έτσι αναφέρεται παρακάτω το παράδοξο για τον θεωρητικό μαθηματικό ενδεχόμενο να εξαρτάται η πορεία της έρευνας του από νομικές διαδικασίες. Η άμυνα του Υπουργείου έναντι των απαιτήσεων του αντίδικου είναι ένα απόρρητο έγγραφο. Η μοναδική εκδεδομένη απάντηση (γνωστή σε αυτόν τον συγγραφέα) ενός μέλους της ομάδας VIPER στην κριτική του ισχυρισμού δεν επιχείρησε μια αναθεώρηση( βλ. υπ. 41). Ούτως ή άλλως, ο εναγόμενος στη μήνυση ήταν το Υπουργείο παρά τα ίδια τα μέλη της ομάδας, επομένως η σειρά των επιχειρημάτων που υιοθετήθηκαν ίσως να μην ήταν δικά τους.

Έτσι κι αλλιώς, μία επίθεση στην τυπική έννοια της απόδειξης ήταν πράγματι η βάση της υπεράσπισης της VIPER έτσι όπως κορυφώθηκε, αφού έπαψε η αντιδικία, από τo Martyn Thomas, κεφαλή του οίκου προγραμματισμού Praxis:

Πρέπει να προσέξουμε να μην κρατήσουμε το χαρακτηρισμό “απόδειξη” περιορισμένο σε μία, εξαιρετικά τυπική, προσέγγιση της επαλήθευσης. Εάν η απόδειξη μπορεί να σημαίνει μόνο αξιωματική επαλήθευση με αποδείξεις θεωρημάτων, τα περισσότερα μαθηματικά είναι αναπόδεικτα και δεν μπορούν να αποδειχθούν. Οι “κοινωνικές” διαδικασίες της απόδειξης είναι αρκετά καλές για μηχανικούς σε άλλα αξιώματα, αρκετά καλά για μαθηματικούς αλλά όχι αρκετά καλά για εμένα… Εάν κρατάμε τη λέξη “απόδειξη” για τις δραστηριότητες των οπαδών του Hilbert, χάνουμε μία χρήσιμη λέξη, και βρισκόμαστε σε κίνδυνο να επαινέσουμε υπερβολικά τα αποτελέσματα των δραστηριοτήτων τους( βλ. υπ. 42).

Ο David Hilbert (1862-1943) ήταν ένας τυπικός(φορμαλιστής) μαθηματικός του οποίου ο ορισμός της “απόδειξης” ήταν από τις περισσότερες απόψεις παρόμοιος με εκείνον που δόθηκε παραπάνω από τους Boyer και Moore( βλ. υπ. 43). Η παράδοση των φορμαλιστών των οποίων ηγέτης ήταν ο Hilbert προσπαθούσε να σπάσει τη σύνδεση μεταξύ των μαθηματικών συμβόλων και των φυσικών ή των πνευματικών τους αναφορών. Τα σύμβολα, υποστηρίζει ο φορμαλιστής, είναι απλώς σημάδια επάνω στο χαρτί, κενά από εσωτερική σημασία( βλ. υπ. 44). Οι αποδείξεις σχηματίζονται χρησιμοποιώντας αυτά τα σύμβολα σύμφωνα με τις αρχές του μετασχηματισμού της τυπικής λογικής- αρχές που δέχονται μια ακριβή, “μηχανική” μορφή( βλ. υπ. 45).

Παρά την αξιοσημείωτη επιρροή του φορμαλισμού μεταξύ των μαθηματικών, δεν παίρνουν όλες οι μαθηματικές αποδείξεις την ίδια μορφή. Οι περισσότερες στην πραγματικότητα είναι μικρότερες, πιο “υψηλού επιπέδου” και πιο “ανεπίσημες”. Μέρος του λόγου γι’ αυτό είναι η καθαρά πληκτική διαδικασία της παραγωγής μαθηματικών αποδείξεων, και η έκτασή τους˙ αυτό αποτελεί επίσης μεγάλο μέρος της έλξης αυτόματων ή ημιαυτόματων συστημάτων δημιουργίας-αποδείξεων, όπως είναι το σύστημα HOL το οποίο χρησιμοποιείται στην απόδειξη VIPER ή στον αυτοματοποιημένο αποδεικτή θεωρημάτων που έχει δημιουργηθεί από τους Boyer και Moore.

Η σχετικά ανεπίσημη φύση πολλών μαθηματικών αποδείξεων ήταν μια πηγή για την υπεράσπιση της αξίωσης απόδειξης για το VIPER, όπως δείχνουν τα παραπάνω λεγόμενα του Thomas. Ήταν επίσης η βάση για μια γενική επίθεση προς την τυπική επιβεβαίωση των προγραμμάτων που αμφισβητήθηκε ευρύτατα, μία επιστημονική δημοσίευση του Richard De Millo του Georgia Institute of Technology και του Alan Perlis του Τμήματος Πληροφορικής του Πανεπιστημίου Yale( βλ. υπ. 46). Αποδείξεις θεωρημάτων στα μαθηματικά και τυπικές επαληθεύσεις των προγραμμάτων υπολογιστών ήταν τελείως διαφορετικές έννοιες, ισχυρίζονταν:

Μία απόδειξη δεν είναι ένα όμορφο αφηρημένο αντικείμενο με ανεξάρτητη ύπαρξη. Κανένας μαθηματικός δε συλλαμβάνει μία απόδειξη, κάθεται πίσω, και αναστενάζει με ευχαρίστηση με τη γνώση οτι τώρα μπορεί να είναι βέβαιος για την αλήθεια του θεωρήματός του. Τρέχει στο διάδρομο και ψάχνει κάποιον για να το ακούσει. Ορμά στο γραφείο ενός συναδέλφου και καταλαμβάνει το μαυροπίνακα. Βάζει στην άκρη το θέμα που είχε προγραμματιστεί και γλεντάει με ένα σεμινάριο με τη νέα του ιδέα. Τραβάει τους μαθητές του από τις πτυχιακές τους εργασίες για να τον ακούσουν. Πιάνει το τηλέφωνο και τα λέει στους συναδέλφους του στο Τέξας και στο Τορόντο…

Μετά από αρκετή εσωτερίκευση, αρκετό ανασχηματισμό, αρκετές γενικεύσεις , αρκετή χρήση, και αρκετή σύνδεση, η μαθηματική κοινωνία τελικά αποφασίζει οτι οι κεντρικές έννοιες στο γενικό θεώρημα, το οποίο μάλλον είναι πολύ διαφοροποιημένο, έχουν μία τελική σταθερότητα. Εάν οι διάφορες αποδείξεις φαίνονται σωστές και τα αποτελέσματα εξετάζονται από αρκετές πλευρές, τότε η αλήθεια του θεωρήματος τελικά θεωρείται εδραιωμένη. Το θεώρημα θεωρείται αληθινό με την κλασσική έννοια- δηλαδή, με την έννοια οτι θα μπορούσε να παρουσιαστεί από την τυπική επαγωγική λογική, αν και για σχεδόν όλα τα θεωρήματα καμία τέτοια επαγωγή δεν έλαβε ή πρόκειται να λάβει χώρα…

Οι μαθηματικές αποδείξεις αυξάνουν την αυτοπεποίθησή μας μόνο εφόσον έχουν εκτεθεί στους κοινωνικούς μηχανισμούς της μαθηματικής κοινωνίας. Αυτοί οι ίδιοι οι μηχανισμοί καταδικάζουν τις λεγόμενες αποδείξεις των προγραμμάτων υπολογιστών (software), τις μακρές τυπικές επαληθεύσεις που αντιστοιχούν όχι στη λειτουργική μαθηματική απόδειξη, αλλά στη φανταστική λογική δομή που ο μαθηματικός φαντάζεται οτι περιγράφει την αίσθηση του πιστεύω του. Οι επαληθεύσεις δεν είναι μηνύματα˙ ένα άτομο το οποίο μπορεί να τρέξει στο διάδρομο για να μεταδώσει την τελευταία του επαλήθευση σύντομα θα έβλεπε τον εαυτό του κοινωνικό απόβλητο. Οι επαληθεύσεις δεν μπορούν να διαβαστούν άμεσα ˙ ένας αναγνώστης μπορεί να γδαρθεί μέσω μιας από τις μικρότερες με τη δύναμη ηρωικής προσπάθειας, αλλά αυτό δεν είναι διάβασμα. Καθώς δεν είναι δυνατόν να αναγνωστούν και -στην ουσία – δεν είναι δυνατόν να ειπωθούν, οι επαληθεύσεις δεν μπορούν να εσωτερικευθούν, να μετατραπούν, να γενικευθούν, να χρησιμοποιηθούν, να συσχετισθούν με άλλες αρχές, και τελικά να ενσωματωθούν σε μια συνείδηση της κοινωνίας. Δεν μπορούν να κερδίσουν αξιοπιστία σταδιακά, όπως κάνει ένα μαθηματικό θεώρημα˙ ένας είτε τις πιστεύει τυφλά, ως μια πράξη καθαρής πίστης, ή δεν τις πιστεύει καθόλου( βλ υπ. 47).

Η επιστημονική δημοσίευση των De Millo-Lipton-Perlis προκάλεσε οξεία κριτική από τους υποστηρικτές της αναπτυσσόμενης πρακτικής της επαλήθευσης προγραμμάτων. Ένας έγραψε: Είμαι ένας από εκείνους τους “κλασικιστές” που πιστεύουν οτι ένα θεώρημα είτε μπορεί είτε δεν μπορεί να εξαχθεί από ένα σετ αξιωμάτων. Δεν πιστεύω οτι η ορθότητα ενός θεωρήματος πρέπει να αποφασίζεται από μία γενική εκλογή ( βλ. υπ. 48). Ο Edsger Dijkstra, ένας από τους ηγέτες του κινήματος της μαθηματικοποίησης της πληροφορικής , περιέγραψε την επιστημονική δημοσίευση των De Millo-Lipton-Perlis ως ένα “πολιτικό φυλλάδιο από το μεσαίωνα”. Προκαλεί το ενδιαφέρον, ωστόσο, το γεγονός οτι η υπεράσπιση του Dijkstra ήταν σύντομων, κομψών, ανθρώπινων (αντί μηχανικών) αποδείξεων προγραμμάτων. Αποδέχτηκε οτι “η επικοινωνία μεταξύ των μαθηματικών είναι απαραίτητο συστατικό της μαθηματικής μας κουλτούρας” και ομολόγησε οτι “μακρές τυπικές αποδείξεις δεν είναι πειστικές” ( βλ. υπ. 49). Αλλού, ο Dijkstra είχε γράψει: “Πάνω στην ιδέα οτι οι αποδείξεις είναι τόσο βαρετές που δεν μπορούμε να βασιστούμε επάνω τους, εκτός και αν ελέγχονται μηχανικά έχω σχεδόν φιλοσοφικές ενστάσεις, καθώς θεωρώ τις μαθηματικές αποδείξεις ως μία αντανάκλαση της αντίληψής μου, και η “ αντίληψή” είναι κάτι που δεν μπορούμε να μεταβιβάσουμε, είτε σε ένα άλλο άτομο είτε σε μία μηχανή.”( βλ. υπ. 50)

Τουλάχιστον τρεις θέσεις επομένως διαγωνίζονταν στη διαμάχη που δημιουργήθηκε από τους De Millo, Lipton, και Perlis: η τυπική, μηχανοποιημένη επαλήθευση των σχεδίων προγραμμάτων και φυσικών εξαρτημάτων υπολογιστών (software και hardware)˙ και η προάσπιση της ανθρώπινης αντί της μηχανικής απόδειξης. Κανένα ολοκληρωτικά οριστικό κλείσιμο της διαμάχης μέσα στην πληροφορική δεν επιτεύχθηκε, και η ισχύς της αναλογίας μεταξύ αποδείξεων στα μαθηματικά και τυπικής επαλήθευσης των συστημάτων πληροφορικής παραμένει αμφισβητήσιμη( βλ. υπ. 51).

Και στα μαθηματικά, επίσης, η κατάσταση των αποδείξεων που υποστηρίζονται από υπολογιστές έχει υπάρξει θέμα που προκάλεσε αμφισβητήσεις. Η αμφισβήτηση παγιοποιήθηκε πιο καθαρά γύρω από τη βασισμένη σε υπολογιστή απόδειξη του 1976 από τους Kenneth Appel και Wolfgang Haken της τετράχρωμης εικασίας( βλ. υπ. 52). Οι δημιουργοί αυτής της απόδειξης ανακεφαλαίωσαν τουλάχιστον κάποιες από τις ενστάσεις και την υπεράσπισή τους ως εξής.

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

Αυτή η άποψη είναι λογική για τα θεωρήματα εκείνα των οποίων οι αποδείξεις είναι μετρίου μεγέθους και ιδιαιτέρως θεωρητικά. Όταν οι αποδείξεις είναι μακρές και χρειάζονται ιδιαίτερες πράξεις, μπορεί να λεχθεί οτι ακόμα και όταν ο έλεγχος με το χέρι είναι εφικτός, η πιθανότητα ανθρώπινου λάθους είναι αρκετά μεγαλύτερη από εκείνη του λάθους από το μηχάνημα( βλ. υπ. 53)(.

Αν και το γενικό ζήτημα της κατάστασης των τυπικών αποδείξεων που γεννιούνται από υπολογιστή παραμένει αμφισβητήσιμο, υπάρχουν σημάδια οτι στο επίπεδο που τίθενται τα στάνταρντ για συστήματα υπολογιστών κροτικής σημασίας για την ασφάλεια και την προστασία, η διαμάχη στην πράξη κερδίζεται από τους υποστηρικτές της τυπικής επαλήθευσης. Η ζήτηση για επαλήθευση στο Πορτοκαλί Βιβλίο αντιπροσώπευε μία νίκη για αυτή τη θέση, μολονότι αμφισβητήσιμη, καθώς υπάρχει κριτική και για το μοντέλο “ασφάλειας” που είναι θεμελιώδες στο Πορτοκαλί Βιβλίο και στις διαδικασίες πιστοποίησης σύμφωνα με τα κριτήρια του Πορτοκαλί Βιβλίου( βλ. υπ. 54). Ούτε προσέγγισε άμεσα το Πορτοκαλί Βιβλίο το ζήτημα της φύσεως της απόδειξης. Πιο πρόσφατα, ωστόσο, το Def Stan 00-55, που αντιπροσώπευε την επίσημη πολιτική του Υπουργείου Αμύνης του Ηνωμένου Βασιλείου, έχει πράξει κατ’ αυτόν τον τρόπο, σαφώς καταπιανόμενο με το ζήτημα της σχετικής κατάστασης των διαφορετικών μορφών μαθηματικών ισχυρισμών. Διαφοροποιείται μεταξύ της “Επίσημης Απόδειξης” και του “Αυστηρού Ισχυρισμού”:

Μία Επίσημη Απόδειξη είναι μια αυστηρά καλοφτιαγμένη σειρά από λογικές φόρμουλες τέτοιες που κάθε μία συνεπάγεται από φόρμουλες που νωρίτερα εμφανίζονταν στη σειρά είτε σαν παραδείγματα αξιωμάτων της λογικής θεωρίας…

Ένας Αυστηρός Ισχυρισμός είναι στο επίπεδο της μαθηματικής επιχειρηματολογίας στην επιστημονική βιβλιογραφία που θα γίνει αντικείμενο ανασκόπησης…( βλ. υπ. 55)

Σύμφωνα με το Υπουργείο, η επίσημη απόδειξη πρέπει να προτιμάται από τον αυστηρό ισχυρισμό:

Η δημιουργία (επίσημων) αποδείξεων θα…καταναλώσει αρκετό χρόνο από το ειδικευμένο προσωπικό. Έτσι το Στάνταρντ οραματίζεται επίσης ένα χαμηλότερο επίπεδο σχεδίου ασφαλείας˙ αυτό το επίπεδο είναι γνωστό ως Αυστηρός Ισχυρισμός. Ο Αυστηρός Ισχυρισμός δεν είναι Επίσημη Απόδειξη και δεν αποτελεί υποκατάστατο αυτής…( βλ. υπ. 56)

Παραμένει αμφίβολο σε πιο σημείο οι πρακτικές της βιομηχανίας προγραμμάτων υπολογιστών θα επηρεαστούν από το Def Stan 00-55 και από παρόμοια στάνταρντ για άλλους τομείς που πιθανόν ακολουθήσουν- μία διαδικασία για την απόδοση εξαιρέσεων των αυστηρών απαιτήσεων του 00-55 ενσωματώνεται στο έγγραφο. Επίσημες αποδείξεις των προγραμμάτων του “πραγματικού κόσμου” ή των σχεδίων φυσικών εξαρτημάτων υπολογιστών είναι ακόμα αρκετά σπάνιες. Εάν πράγματι γίνουν πιο συνήθεις, θα προέβλεπα οτι ένα επόμενο επίπεδο αμφισβήτησης και αντιδικίας θα δημιουργηθεί. Αυτό θα αφορά όχι τη γενική κατάσταση των επισήμων αποδείξεων που δημιουργούνται από υπολογιστές (αν και αυτό το ζήτημα σίγουρα θα επανέλθει), αλλά ένα ζήτημα που μέχρι στιγμής δεν έχει προκαλέσει καμία αντιδικία: την εσωτερική δομή των επισήμων αποδείξεων. Ακόμα κι αν όλοι συμφωνήσουν οτι οι αποδείξεις πρέπει να αποτελούνται από παραποιήσεις σε φόρμουλες σύμφωνα με “μηχανικούς” κανόνες της λογικής, δεν συνεπάγεται οτι όλοι θα συμφωνούν με το ποιοι θα πρέπει να είναι αυτοί οι κανόνες. Οι ιστορίες της μαθηματικής απόδειξης και της τυπικής λογικής αποκαλύπτουν το αντικείμενο για σημαντική διαφωνία.

Η πιο γνωστή διαφωνία αφορά το νόμο του εξαιρούμενου μέσου (ο οποίος ισχυρίζεται οτι είτε μία πρόταση είτε η άρνησή της πρέπει να είναι ορθή) και επομένως η δυνατότητα απόδειξης οτι ένα μαθηματικό αντικείμενο υφίσταται δείχνοντας την μη ύπαρξή του θα υποδήλωνε μία αντίφαση. Οι φορμαλιστές όπως ο Hilbert, δεν θεωρούσαν τέτοιες αποδείξεις προβληματικές˙ οι “κονστρακτιβιστές” (οπαδοί του κινήματος αφηρημένων κατασκευών) και οι υποστηρικτές του δόγματος της “διαισθητικής γνώσης”, αξίζει να αναφερθεί ο L. E. J. Brouwer, αρνήθηκαν να τις εφαρμόσουν, τουλάχιστον για διαισθητικά μαθηματικά σύνολα( βλ. υπ. 57).

Άλλα παραδείγματα είναι εκείνες που κάποιες φορές αποκαλούνται οι αρχές του Lewis, οι οποίες πήραν το όνομά τους από τον επιστήμονα της λογικής Clarence Irving Lewis( βλ. υπ. 58). Αυτές οι αρχές είναι οτι η αντίφαση συνεπάγεται κάθε αντίφαση και οτι μία ταυτολογία συνεπάγεται από κάθε πρόταση. Επακολουθούν από διαισθητικά ευχάριστους αξιωματισμούς της επίσημης λογικής, και όμως φάνηκαν να είναι αμφίβολες. Είναι λογικό, για παράδειγμα, να βγάλουμε το συμπέρασμα, όπως επιτρέπει η πρώτη αρχή του Lewis, οτι “Το φεγγάρι έχει φτιαχτεί από πράσινο τυρί”συνεπάγεται από το οτι “Ο Γιάννης είναι άντρας και ο Γιάννης δεν είναι άντρας;” Όπως γράφει ένα κείμενο: “Διαφορετικοί άνθρωποι αντιδρούν με διαφορετικούς τρόπους στις αρχές του Lewis. Για κάποιους είναι ευπρόσδεκτες ενώ για άλλους είναι περίεργες και ύποπτες. Για κάποιους είναι πιο αντικρούσιμο στη λογική να πούμε οτι (μια αντίφαση) συνεπάγεται όλες τις φόρμουλες από οτι είναι στην αριθμητική να πούμε οτι το χº πάντοτε ισούται με 1... Για άλλους, ωστόσο, οι αρχές του Lewis είναι αρκετά απορριπτέες διότι η προηγούμενη φόρμουλα μπορεί να ‘μην έχει καμία σχέση’ με την επόμενη φόρμουλα( βλ. υπ. 59). Οι κριτικοί πρέπει να αντιμετωπίσουν το πρόβλημα οτι οποιοδήποτε λογικό σύστημα που απέχει από τις αρχές του Lewis παρουσιάζεται να πρέπει να εγκαταλείψει τουλάχιστον ένα, πιο βασικό, “διαισθητικά φανερό”, λογικό αξίωμα.

Αυτοί οι αντιφατικοί κανόνες της λογικής μπορούν να βρεθούν σε συστήματα από τα οποία εξαρτάται η επίσημη απόδειξη προγραμμάτων και φυσικών εξαρτημάτων υπολογιστών. Ο νόμος του εξαιρουμένου μέσου χρησιμοποιείται ευρέως στην αυτοματοποιημένη απόδειξη θεωρήματος (για παράδειγμα, στο HOL σύστημα που χρησιμοποιήθηκε για την επίσημη απόδειξη του VIPΕR). Η πρώτη αρχή του Lewis – οτι η αντίφαση συνεπάγεται οποιαδήποτε πρόταση- μπορεί να βρεθεί σε σχεδόν όλα τα συστήματα αυτοματοποιημένης λογικής (π. χ. ανάμεσα στους βασικούς συμπερασματικούς κανόνες της σημαντικής Μεθόδου Ανάπτυξης της Βιέννης)( βλ. υπ. 60).

Μέχρι σήμερα, αυτοί οι κανόνες δεν έχουν προκαλέσει στην πληροφορική το είδος της αντίφασης που τους έχει καταλάβει στα μεταμαθηματικά και στην επίσημη λογική. Έχει υπάρξει κάποια πνευματική αψιμαχία μεταξύ των υποστηρικτών των αποδεικτών των “κλασσικών” θεωρημάτων, οι οποίοι εφαρμόζουν το νόμο του εξαιρουμένου μέσου, και των “κονστρακτιβιστών”, οι οποίοι δεν τον παραδέχονται( βλ. υπ. 61). Αυτή η αψιμαχία, μέχρι σήμερα, δεν έχει λάβει τη μορφή οχυρωμένης φιλοσοφικής διαμάχης, και απ’ όσο γνωρίζει ο συγγραφέας, καμία απόδειξη υπολογιστή δεν έχει απορριφθεί λόγω του οτι στηρίζεται στο εξαιρούμενο μέσο ή στις αρχές του Lewis. Πρακτικοί παράγοντες – η θέση των συστημάτων σε “λειτουργία”, η επιλογή λογικών κυκλωμάτων κατάλληλων σε συγκεκριμένα περιβάλλοντα- έχουν υπερακοντίσει ευρύτερα φιλοσοφικά ζητήματα. Στο μέλλον πάντως θα προκύψει το ζήτημα αυτό και αυτή η μεταφορά ενός θεωρητικού μαθηματικού προβλήματος σαν ένα πρόβλημα πλέον στο τεχνολογικό επίπεδο θα φάνταζε απίθανο σε παλαιότερες εποχες,αποτελει χαρακτηριστικό της εποχής μας όπου η εξέλιξη της τεχνολογίας όχι μόνο δεν ακολουθεί απαραίτητα την εξέλιξη της θεωρητικής έρευνας αλλά αντίθετα μπορεί και να την προκαθορίσει.

Μπορούμε, ωστόσο, να συμπεράνουμε μία κατάσταση πραγματισμού και ειρηνικής συνύπαρξης ανάμεσα σε διαφορετικά λογικά συστήματα θα συνεχιστεί; Η αίσθησή μου είναι οτι δεν μπορούμε˙ οτι αυτή η κατάσταση είναι προϊόν της πειραματικής ακαδημαϊκής φάσης της ανάπτυξης της απόδειξης της ορθότητας συστημάτων υπολογιστών. Καθώς επίσημες αποδείξεις λαμβάνουν μεγαλύτερη εμπορική και ρυθμιστική σημασία, μεγάλα συμφέροντα θα αναπτυχθούν προς υπεράσπιση, ή προς άσκηση κριτικής, συγκεκριμένων αποδείξεων. Κάποιες φορές, τουλάχιστον, αυτά τα συμφέροντα θα έρθουν σε σύγκρουση. Σε μία τέτοια περίπτωση, οι αξιοπιστίες των κανόνων της επίσημης λογικής αναπόφευκτα θα βρεθούν σε διαμάχη, και στα δικαστήρια.

Συμπέρασμα

Υπάρχει μία διαφορετική διαφορά μεταξύ της αριθμητικής κινητής υποδιαστολής των υπολογιστών και της απόδειξης των υπολογιστών. Στην πρώτη υπήρχε μία σταθερή, ομόφωνη ανθρώπινη αριθμητική έναντι της οποίας θα μπορούσε να κριθεί η ανθρώπινη αριθμητική. Η ανθρώπινη αριθμητική, ωστόσο, ήταν ανεπαρκής για να καθορίσει την καλύτερη μορφή αριθμητικής υπολογιστών. Ήταν πράγματι θέμα κρίσης το ποια ήταν καλύτερη, επίμαχης κρίσης πάνω σε αυτό. Η ανθρώπινη αριθμητική παρείχε μια πηγή, η οποία αντλείτο διαφορετικά από διαφορετικούς συμμετέχοντες, αντί για ένα μία σειρά κανόνες που θα μπορούσε απλά να εφαρμοστεί στην αριθμητική των υπολογιστών. Υπάρχει ακόμα αβέβαιη απόδειξη οτι κοινωνικά συμφέροντα, βασικά τα διαφορετικά συμφέροντα των εταιρειών Intel και Digital, επηρέασαν τις κριτικές που έγιναν. Αντίστοιχα, το αποτέλεσμα –“ολοκλήρωση” υπέρ του σχήματος της αριθμητικής των Kahan-Coonen-Stone- μπορεί να έχει επηρεαστεί από τυχαίους παράγοντες όπως η συχνότητα των συσκέψεων της αρμόδιας επιτροπής στο Silicon Valley, βάση της Intel και άλλων ημιαγωγών εταιρειών, και στη βάση του Kahan Berkeley.

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

Μία διαφωνία πάνω στη μαθηματική απόδειξη των συστημάτων υπολογιστών έχει ήδη φθάσει το επίπεδο της αντιδικίας: η αντίφαση που αφορά τον μικροεπεξεργαστή VIPER. Η πρόβλεψη αυτού του κεφαλαίου είναι οτι η υπόθεση VIPER δεν θα είναι μοναδική. Ούτε θα είναι αρκετή για να φθάσει σε συμφωνία πάνω στη γενική μορφή που θα λάβουν οι αποδείξεις- για παράδειγμα, μα απαιτηθεί να λάβουν τη μορφή διαδοχικών παραποιήσεων συμβόλων που θα συμβαίνουν σύμφωνα με τους κανόνες μετατροπής ενός λογικού συστήματος. Εάν η θέση που υιοθετείται σε αυτό το κεφάλαιο είναι ορθή, αυτό απλώς θα οδηγήσει τη διαφωνία “προς τα κάτω” από την κατάσταση των γενικών τύπων επιχειρημάτων στην ισχύ συγκεκριμένων βημάτων σε αυτά τα επιχειρήματα. Συγκεκριμένα, διαφωνία θα πρέπει να αναμένεται επάνω σε λογικά συστήματα τα οποία υποστηρίζουν επίσημες αποδείξεις.

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

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

Ευχαριστίες

Η έρευνα επάνω στην αριθμητική κινητής υποδιαστολής και στη VIPER υποστηρίχθηκε από το Συμβούλιο Οικονομικής και Κοινωνικής Έρευνας του Ηνωμένου Βασιλείου (ERSC) στα πλαίσια του Προγράμματος για τις Τεχνολογίες Πληροφορικής και Επικοινωνίας, (PICT), χορηγία Α35250006 και WA35250006. Η παρούσα εργασία επάνω στο θέμα του δεύτερου τμήματος της μελέτης υποστηρίζεται από μια επιπλέον χορηγία από το ESRC επάνω στις “Μελέτες επάνω στην Κοινωνιολογία της Απόδειξης” (R000234031)

Κεφάλαιο 8

H. M Collins, Artificial Experts: Social Knowledge and Intelligent Machines (MIT Press, 1990), κεφάλαιο 5.

E. Pelaéz, J. Fleck, και D. MacKenzie, “Κοινωνική έρευνα πάνω στα προγράμματα υπολογιστών”, εργασία που αναγνώστηκε στο Εθνικό Εργαστήρι του Προγράμματος στις Τεχνολογίες Πληροφορικής και Επικοινωνιών, Manchester, 1987, σελ. 5.

K. Mannheim, Ideology and Utopia (Routledge & Kegan Paul, 1936) Δείτε D. Bloor, “Wittegenstein and Manheim on the sociology of mathematics”, Μελέτες επάνω στην Ιστορία και τη Φιλοσοφία της Επιστήμης 4 (1973) : 173-191.

Αυτή η συνθήκη είναι γνωστή ως ”twos compliment arithmetic”, καθώς εάν βρίσκεται σε αυτήν τη μορφή “το πρόσημο αντιμετωπίζεται σαν να ήταν απλώς ένα ακόμη ψηφίο, οι αρνητικοί αριθμοί αντιπροσωπεύονται από τους συμπληρωματικούς τους αναφορικά με το 2” (Robert F. Shaw, “Arithmetic operation in a binary computer,” Επισκόπηση Επιστημονικών Εργαλείων 21 (1950), σελ. 687-688). (Η εργασία του Shaw, μαζί με άλλες σημαντικές εργασίες στον τομέα, ανατυπώθηκε στο Computer Arithmetic του Earl E. Schwartzlander, Jr. (Dowden, Hutchinson & Ross, 1980).)

Παρόμοια με άλλη αριθμητική υπολογιστών, επιτρέπονται μεταβλητές σε αυτή τη βασική μορφή (π. χ. ένα είδος 64-ψηφίων “διπλής ακριβείας”) . Χάριν ευκολίας, αυτό το ζήτημα αγνοείται στο κείμενο.

Ο εκθέτης συνήθως σώζεται όχι στη φυσική του μορφή η οποία θα έπρεπε να περιλαμβάνει ένα ψηφίο το οποίο θα παριστάνει το πρόσημό του, αλλά σε μία “διαφορετική” μορφή δίχως πρόσημο.

W. Kahan, “Mathematics written in sand,” Πρακτικά συνεδριάσεων της Αμερικάνικης Στατιστικής Ένωσης, 1983 τμήμα Στατιστικής Πληροφορικής, σελ. 12-26.

Imre Lakatos, Proofs and Refutations: The Logic of Mathematical Discovery (Cambridge University Press, 1976). Χρησιμοποιώντας ως πηγή τη δουλειά της Mary Douglas, o David Bloor έχει προτείνει οτι διαφορετικές κοινωνικές συνθήκες είναι δυνατόν να προκαλέσουν διαφορετικές τυπικές αντιδράσεις στις ανωμαλίες. Δυστυχώς, η αξιολόγηση αυτής της πρότασης για την εξεταζόμενη περίπτωση θα απαιτούσε στοιχεία τα οποία δεν κατέχω. Βλέπε D. Bloor, “Polyhedra and the abominations of Leviticus”, British Journal for the History of Science II (1978): 245-272; Μ. Douglas, Natural Symbols: Explorations in Cosmology (Barrie & Rockcliff, 1970).

Συνέντευξη με τον Καθηγητή W. Kahan, Berkeley, Οκτώβριος 19, 1989; Lakatos, Proofs and Refutations. Στην “ προς τα εμπρός ανάλυση λάθους”, ένα ανώτερο όριο υπολογίζεται για το συσσωρευμένο λάθος σε κάθε βήμα, και επομένως τελικά και για το λάθος στο τελικό αποτέλεσμα. Η προς τα πίσω ανάλυση, από την άλλη, “ξεκινά με τη λύση που έχει υπολογιστεί και λειτουργεί προς τα πίσω για να ξαναδημιουργήσει το πρόβλημα, του οποίου είναι ακριβής λύση. Βλέπε P. J. I. Wallis, Improving Floating Point Programming (Wiley, 1990), σελ. 12. Για κάποια σχόλια επάνω στην ιστορία της ανάλυσης του λάθους, βλέπε J. H. Wilkinson, “Modern error analysis, “ SIAM Review 13 (1971): 548-568.

O Kahan χρησιμοποιεί τον όρο αυτό στο “Doubled-Precision IEEE Standard 754 Floating Point Arithmetic” (κείμενο, 1987).

Lakatos, Proofs and Refutations, D. Bloor, Wittgenstein: A Social Theory of Knowledge (Mackmillan, 1983), σελ. 141-142.

Συνέντευξη του Kahan.

O Palmer επρόκειτο να παίξει αργότερα ένα σημαντικό ρόλο στην ανάπτυξη παράλληλων υπολογισμών στις ΗΠΑ όταν εκείνος και άλλοι εγκατέλειψαν την Intel το 1983 για να ιδρύσουν τη φίρμα Ncube.

Συνέντευξη του Kahan: J. Palmer, “The Intel standard for floating-point arithmetic,” στα Πρακτικά συνεδριάσεων του ΙΕΕΕ COMPSAC 1977, σελ. 107.

Επιστολή στο συγγραφέα από το Robert G. Stewart, 18 Οκτώβριος1990.

IEEE Standard for Binary Floating-Point Arithmetic: American National Standards Institute/Institute of Electrical and Electronics Engineering Standard 754,1985, 12 Αυγούστου, 1985.

Συνέντευξη του Kahan.

Η Intel εξέδωσε το i8087 το 1980 εις ανεμώνη του στάνταρντ. Για την αριθμητική του i8087 βλέπε J. F. Palmer και S. P. Morse, The 8087 Primer (Wiley, 1984), 7. Μία τρίτη πρόταση που εξετάστηκε σοβαρά έγινε από τον Robert Fraley και τον J. Stephen Walther, αλλά η κύρια διαφωνία φαίνεται οτι υπήρξε ανάμεσα στις προτάσεις του DEC και των Kahan-Coonen-Stone. Για μία σύγκριση των τριών προτάσεων βλέπε W. J. Cody. “Analysis of proposals for the floating-point standard,” Computer (March 1981): 63-66.

IEE Standard for Binary Floating-Point Arithmetic, σελ. 14. Το επιχείρημα για τα δύο μηδενικά είναι οτι διευκολύνουν την απομάκρυνση των ιδιαιτεροτήτων που θα μπορούσαν να δημιουργήσουν πρόβλημα στους υπολογισμούς οι οποίες είναι κοινές στη μελέτη (π. χ.) της ροής των υγρών. Με δύο μηδενικά, “οι ομοιότητες διατηρούνται ενώ διαφορετικά δεν διατηρούνταν” και παρέχονται δυνατότητες που δεν υπάρχουν στα συμβατικά μαθηματικά. Ένα παράδειγμα από τους πολύπλοκους αριθμούς αφορά την τετραγωνική ρίζα του –1, η οποία κατά συνθήκη μπορεί να έχει δύο αξίες: + i και – i. Τα μηδενικά επιτρέπουν την άρση αυτής της ασυνέχειας, η τετραγωνική ρίζα του –1- Οi είναι + i και η τετραγωνική ρίζα του –1-Οi είναι – i (συνέντευξη του Kahan).

Για τη gradual underflow βλέπε I. B. Goldberg, “27 bits are not enough for 8-Digit Accuracy,” Communications of the ACM 10 (1967): 105-108. Ο πρωτοπόρος των υπολογιστών Konrad Zuse ήταν ένας από τους πρώτους πρόμαχους, σύμφωνα με τον Cody (“Analysis of proposals for the floating-point standard,” σελ. 63).

Jeroma T. Coonen, “Underflow and the denormalized numbers,” Computer (Μάρτιος 1981), σελ. 75.

Cody, “Analysis of proposals for the floating –point standard,” σελ. 67.

Mary Payne and Dileep Bhandarkar, “VAX floating-point: A solid foundation for numerical computation,” Computer Architecture News 8, no 4 (1980), σελ. 28-29.

Bob Fraley και teve Walther, “Proposal to eliminate denormalized numbers,” ACM Signum Newletter (Οκτώβριος 1979), σελ. 22.

Cody, “Analysis of proposals for the floating-point standard,” σελ. 67

Εξάγω αυτά τα σημεία από τη συνέντευξή μου με τον Kahan.

Ομοίως

Mary H. Payne, “Floating point standardization,” Πρακτικά του COMPCON (Φθινόπωρο 1979), σελ. 169.

Επομένως η συμβατότητα με το στάνταρντ εξαπλώνεται στον τομέα των εξειδικευμένων ντίτζιταλ σήματος επεξεργαστών (DSP). Ένας ειδικός στον τομέα γράφει: “Το να μην είναι συμβατή με το ΙΕΕΕ προκαλεί τη δυσαρέσκεια των χρηστών που θέλουν να αντικαταστήσουν μια εφαρμογή που τρέχει σε έναν επεξεργαστή array με μια πλακέτα που περιλαμβάνει ένα τσιπ 32-bit floating-point DSP… Οι περισσότεροι array επεξεργαστές είναι συμβατοί με το ΙΕΕΕ.” (από το “DSP, 32-bit floating-point: The birth pangs of a new generation,” του Johan McLeod, Electronics (Απρίλιος 1989), σελ. 73.

W. Brian Arthur, “Competing Technologies and economic prediction,” Options (Απρίλιος 1984), σελ. 10.

Συνέντευξη με τον Chuck Purcell, Μινεάπολη, 4 Απριλίου, 1990.

E. W. Dijkstra, “The humble programmer,” Communications of the ACM 10 (1972), σελ. 864.

Ομοίως.

Trusted Computer System Evaluation Criteria, έγγραφο Υπουργείου Αμύνης ΗΠΑ. DOD 5200.28-STD, Δεκέμβριος 1985 (πρώτη έκδοση 1983).

Υπουργικό Συμβούλιο, Επιτροπή Συμβούλων για Εφαρμοσμένη Έρευνα και Ανάπτυξη, Πρόγραμμα: A Vital Key to UK Competitiveness (HMSO, 1986), παράρτημα Β; Ministry of Defense Directorate of Standardization, Προσωρινό Στάνταρντ Άμυνας 00-55: Η Προμήθεια Προγραμμάτων Υπολογιστών Σημαντικών για την Ασφάλεια στον Εφοδιασμό Άμυνας (Γλασκόβη, 5 Απριλίου 1991).

Pélaez, Fleck, êαι MacKenzie, “Social research on software,” σελ. 5

J. V. Grabiner, “Is mathematical truth time-dependent?” American Mathematical Monthly 81 (1974): 354-365.

Η αλυσίδα των συλλογισμών έχει σταδιακά αναπτυχθεί αρκετά. Βλέπε, π. χ., C. H. Pygott, “Verification of VIPER’s ALU [ Arithmetic/Logic Unit] ,” Tεχνική Αναφορά, Memo Τμήματος (Πρόχειρο), Royal Signals and Radar Establishment, 1991; Wai Wong, “Formal verification of VIPER’s ALU,” Εργαστήριο Υπολογιστών Cambridge, 15 Απριλίου 1993; J. Joyce, S. Rajan, και Z. Zhn, “A virtuoso performance becomes routine practice: A re-verification of the VIPER microprocessor using a combination of interactive theorem-proving and B[ inary] D[ ecision] D[ iagram] -based symbolic trajectory evaluation,” κείμενο από μελέτη που παρουσιάστηκε στο Λονδίνο το 1993. Δεν έχω δει το πρώτο από αυτά. Χρωστάω την γνώση μου ως προς αυτό στον Wong (“Formal Verification,” σελ. 4

Η υπόθεση ήταν Charter Technologies Limited εναντίον του Γραμματέα του Υπουργείου Αμύνης, Ανώτατο Δικαστήριο, Τμήμα Queen’s Bench, υπόθεση 691, 1991.

R. S. Boyer και J. S. Moore, “Proof checking the RSA public key encryption algorithm,” American Mathematical Monthly 91 (1984), σελ. 181.

J. Kershaw, πρόλογος στον Bishop Brock και στον Warren A. Hunt, Jr., Αναφορά στην Τυπική Προδιαγραφή και στη Μερική Επαλήθευση του Μικροεπεξεργαστή VIPER (τεχνική αναφορά 46, Η Λογική των Πράξεων, Ιnc., Austin, Texas, 1990).

M. Thomas, “VIPER lawsuit withdrawn” επικοινωνία μέσω e-mail, 5 Ιουνίου 1999.

Βλέπε την αναφορά του Hilbert το 1927 “The Foundations of Mathematics,” στο From Frege to Gödel: A Source Book in Mathematical Logιc, 1879-1931, ed. J. van Heijenoort (Harvard University Press, 1967). Μία διαφορά που θα μπορούσε να έχει σημασία, σε σχέση με τα επιχειρήματα του De Millo και άλλα που αναφέρονται παρακάτω, είναι οτι για τον Hilbert η σειρά από τις φόρμουλες που δημιουργούν μία απόδειξη “πρέπει να δίνεται ως τέτοια στη νοητική μας διαισθητικότητα” (ομοίως, σελ. 465)

Ο πλέον διάσημος αντίπαλος του φορμαλισμού, ο υποστηρικτής του δόγματος της διαισθητικής γνώσης L. E. J. Brouwer, έγραψε: “Το ερώτημα πού υπάρχει η μαθηματική ακρίβεια, απαντάται διαφορετικά από τις δύο πλευρές˙ ο υποστηρικτής του δόγματος της διαισθητικής γνώσης λέει: στην ανθρώπινη διάνοια, ο φορμαλιστής λέει: στο χαρτί” (από το “Intuitionism and Formalism,” μία Αγγλική μετάφραση της Εναρκτήριας Ομιλίας του Brouwer το 1912 στο Άμστερνταμ, στο Brouwer, Collected Works, τόμος 1, Philosophy and Foundations of Mathematics (North-Holland, 1975), σελ. 125.).

Για μια ενδιαφέρουσα συζήτηση πάνω στη σημαντικότητα της αναλογίας της μηχανής στο μαθηματικό πρόγραμμα του Hilbert, βλέπε Herbert Breger, “””Machines and mathematical styles of thought,” μελέτη που αναγνώστηκε στο συνέδριο επάνω στη Μαθηματικοποίηση των Τεχνικών και την Τεχνικοποίηση των Μαθηματικών , Zentrum fϋr interdisziplinäre Forschung, Universität Bielefeld, 1991.

R. A. De Millo, R. J. Lipton και A. J. Perlis, “Socialprocesses and proofs of theorems and programs,” Ανακοινώσεις της Ένωσης Μηχανημάτων Πληροφορικής 22 (1979): 271-280.

Ομοίως., σελ. 273-275. Η φράση “‘Social’ processes of proof” (“κοινωnικές διαδικασίες απόδειξης”) στην παραπάνω παραπομπή από τον Thomas πιθανότατα είναι μία αναφορά στο επιχείρημα αυτής της μελέτης.

Leslie Lamport των ειδικών της επαλήθευσης SRI International, όπως αναφέρθηκε στο Computer Software as Technology: An examination of Technological Development του Stuart S. Shapiro (διατριβή για Ph. D., Carnegie Mellon Universtiry, 1990), σελ. 132. Η διατριβή του Shapiro περιλαμβάνει μία χρήσιμη ανασκόπηση της διαμάχης γύρω από τη μελέτη των De Millo, Lipton και Perlis τη δεκαετία του 1970.

Edsger W. Dijkstra, “On a political pamphlet from the middle ages,” ACM SIGSOFT, Software Engineering Notes 3, μέρος 2 (Απρίλιος 1978), σελ. 14. Ο Dijkstra σχολίαζε μία παλαιότερη έκδοση της μελέτης των De Millo- Lipton- Perlis που εκδόθηκε στα Πρακτικά του Τέταρτου Συμποσίου ACM επάνω στις Αρχές των Γλωσσών Προγραμματισμού (1977).

Edsger W. Dijkstra, “Formal Techniques and sizeable programs,” μελέτη προετοιμασμένη για το Συμπόσιο επάνω στις Μαθηματικές Βάσεις της Πληροφορικής Επιστήμης, Gdansk, 1976, όπως επανεκτυπώθηκε στο Selected Writings on Computing: A Personal Perspective του Dijkstra (Springer, 1982) (βλέπε σελ. 212-213). Για μία ενδιαφέρουσα ανάλυση της γενικής θέσης του Dijkstra βλέπε Eloίna Pelaéz, A Gift from Pandora’s Boz: The Software Crisis, Διατριβή για Ph. D., University of Edinburgh, 1988.

Η πιο πρόσφατη εστίαση στη διαμάχη ήταν ένα ακόμα άρθρο που αρνείτο, σε διαφορετική βάση απ’ ότι οι De Millo, Lipton και Perlis, την αναλογία μεταξύ επαλήθευσης και μαθηματικών αποδείξεων: James H. Fetzer, “Program Verification: The very idea,” Πρακτικά του ACM 31 (1988), 1048-1063.

Kenneth Appel και Wolfgang Haken, όπως αναφέρεται στο “Why should I believe a computer?” των Philip J. Davis και Reuben Hersh, The Mathematical Experience (Harvester, 1981).

Ομοίως, σελ. 385-386.

Συμβούλιο Εθνικών Ερευνών, Επιτροπή για την Ασφάλεια των Συστημάτων, Computers at Risk: Safe Computing in the Information Age (National Academy Press, 1991).

Υπουργείο Αμύνης, Προσωρινό Στάνταρντ Αμύνης 00-55, Μέρος 2, Οδηγίες, σελ. 28. H Margaret Tierney μελετά την ιστορία του Def Stan 00-55 στο “The evolution of Def Stan 00-55 and 00-56: An intensification of the ‘formal methods debate’ in the UK,’’ επίσημο ντοκουμέντο 30, Πρόγραμμα για τις Τεχνολογίες Πληροφορικής και Επικοινωνίας, Εδιμβούργο, 1991.

Υπουργείο Αμύνης, Προσωρινό Στάνταρντ Αμύνης 00-55, Μέρος 2, Οδηγίες, σελ, 28.

From Frege to Gödel, ed. J, van Heijenoort. Κάποιοι από τους λόγους του Brouwer για το οτι αμφισβητεί ένα κανόνα ο οποίος όπως φαίνεται είναι προφανής μπορούν να βρεθούν στα ακόλουθα λόγια: “Τώρα αναλογιστείτε τον κανόνα tertii exclusi [ νόμος του εξαιρουμένου μέσου] : ισχυρίζεται οτι κάθε υπόθεση είναι είτε αληθινή είτε λανθασμένη˙ στα μαθηματικά αυτό σημαίνει οτι για κάθε πιθανή εμπέδωση ενός συστήματος σε ένα άλλο, ικανοποιώντας ορισμένους δεδομένους όρους, μπορούμε είτε να επιτύχουμε τέτοια εμπέδωση μέσω μιας δόμησης, είτε να φτάσουμε μέσω μιας δόμησης στη σύλληψη της διαδικασίας που θα μπορούσε να οδηγήσει στην εμπέδωση. Συνεπάγεται οτι το ερώτημα της ισχύος του κανόνα tertii exclusi είναι ισάξιο με το ερώτημα εάν είναι δυνατό να υπάρξουν μαθηματικά προβλήματα που δεν μπορούν να λυθούν. Δεν υπάρχει ίχνος απόδειξης για την ιδέα, η οποία έχει προωθηθεί κάποιες φορές οτι δεν υπάρχουν μαθηματικά προβλήματα που δεν μπορούν να λυθούν…στα μαθηματικά του άπειρου ο κανόνας tertii exclusi μέχρι στιγμής δεν είναι αξιόπιστος…Εφόσον αυτή η πρόταση είναι αναπόδεικτη, πρέπει να θεωρηθεί αβέβαιο το εάν προβλήματα σαν αυτό που ακολουθεί είναι δυνατόν να λυθούν: Υπάρχει στη δεκαδική επέκταση ενός [ pi] ψηφίου το οποίο συμβαίνει πιο συχνά από κάθε άλλο; …Και ομοίως παραμένει αβέβαιο εάν το πιο γενικό μαθηματικό πρόβλημα: Ο κανόνας tertii exclusi ισχύει στα μαθηματικά χωρίς εξαίρεση; επιλύεται…Στα μαθηματικά είναι αβέβαιο εάν ολόκληρη η λογική είναι αποδεκτή και είναι αβέβαιο εάν το πρόβλημα της αποδοχής της είναι δυνατό να αποφασισθεί.” “Brouwer, ”The Unreliability of the Logical Principles,” στα Collected Works, του Brouwer, τόμος 1, σελ. 109-111˙ οι εμφάσεις έχουν σβηστεί)

Εδώ χρησιμοποιώ σαν πηγή το Bittgenstein του Bloor, σελ. 124-136.

D. C. Makinson, Topics in Modern Logic (Methuen, 1973), σελ. 27-28.

Cliff B. Jones, Systematic Software Development using VDM, δεύτερη έκδοση (Prentice-Hall, 1990), σελ. 24./

“Εάν δεν έχουμε μια φιλοσοφική δέσμευση στη διαισθητικότητα, το να υιοθετούμε το κίνημα των αφηρημένων κατασκευών όταν απαιτείται μπορεί μόνο να κάνει ένα σύστημα απόδειξης πιο δύσχρηστο. Έχουμε δει οτι κάποια προγράμματα δεν μπορούν να εξαχθούν από τις προδιαγραφές τους σε μία εποικοδομητική λογική, αλλά μπορούν να εξαχθούν σε μία κλασσική λογική στην οποία έχουν επιβληθεί οι ελάχιστοι περιορισμοί.” ) Zohar Manna και Richard Waldinger, “constructive logic considered obstructive,” κείμενο χωρίς ημερομηνία, σελ 8)