Ξεκινάμε με τον Ζιράρ. Όχι γιατί ο Ζιράρ κι εγώ δε ξέρω τί, απλά, έκατσε εδώ και δυό-τρεις μέρες και βρήκα καλή αφορμή (έχω να γράψω ένα σχετικό ριβιού) να πιάσω επιτέλους σοβαρά το [Girard et al 1989]. Τον τύπο τον έχω αποφύγει ολ' αυτά τα χρόνια, κυρίως απο τεμπελιά, αλλα και κάτι λόγω δυσανεξίας στη γνωστή και γραφική πλέον γαλλιά –ξές, αυτός ο γλωσσικός εθνάρεσκος αυτοαποκλεισμός που θυμίζει ελληναριό: ιστοσελίδες αποκλειστικά στα γαλλικά, κιτσάτοι γαλλισμοί σε αγγλικά κείμενα, και άλλες τέτοιες καγκουριές.
Ε λοιπόν, παρά τις γαλλιές το βιβλίο διαβάζεται νεράκι. Αφενός γιατί δέ χάνεται στις λεπτομέρειες, κι αφετέρου λόγω γαλλιάς καλώς εννοούμενης: ο Ζιράρ τό 'χει με το μπλαμπλά, και δέν εχει πέσει και στη λούμπα της πολιτικής ορθότητας που μαστίζει το σινάφι απ' άκρη σ' άκρη. Γουστάρεις να τον διαβάζεις κι ας μή συμφωνείς. Ο συνδυασμός αυτών των δύο πάντως είναι επικίνδυνος: μπορεί κανείς να το ξεφυλλίσει σε μεγάλο βαθμό, παραλείποντας κάθε απόδειξη, και στο τέλος, χωρίς να έχει σκοντάψει συχνά, να έχει την αίσθηση οτι κάτι έκανε· στην πραγματικότητα, είναι πολύ πιθανό να έχει απλά αποκομίσει καναδυό τρία συνθήματα, που δέ θα μπορέσει να υποστηρίξει αν χρειαστεί. Αλλα εντάξει, αυτή ειναι η γνωστή ιδιοτροπία του καλογραμμένου μαθηματικού κειμένου, οτι διαβάζεται και σάν εφημερίδ' απο παιδί: μόνο τις γελοιογραφίες.
Τα δύο χάιλαϊτ του βιβλίου είναι μάλλον το σύστημα F (ή «σύστημα Ζιράρ-Ρέινολντς», αφού δέν πρόκειται μόνο για πατέντα του Ζάν-Ύβ) και η γραμμική λογική, καί τα δύο θέματα που είχε εισάξει ο Ζιράρ κάμποσα και κάποια χρόνια νωρίτερα. Το ισχυρά κανονικοποιήσιμο του συστήματος F είναι και ένα απ' τα ανδραγαθήματα του Ζιράρ, καθώς πρόκειται για απόδειξη της συνέπειας της ανάλυσης. Προσωπικά όμως ήθελα πάντα να δώ την προσέγγισή του στη δηλωτική σημασιολογία, και δή τους «χώρους συνάφειας» (coherence spaces), που τους χρησιμοποιεί αντί για τα πεδία Σκότ, και είναι βέβαια και το μοντέλο που χρησιμοποιεί για να σημασιοδοτήσει τη γραμμική λογική του.
Άς τα πάρουμε με τη σειρά. \(\newcommand{\denote}[1]{[\![ #1 ]\!]}\)
Ξεκινάει το Κεφάλαιο 1 πατώντας στον παππού Φρέγκε και τη θεμελιακή του διάκριση ανάμεσα σε νόημα (sense) και αναφορά (reference) ή, στα καθημάς, δήλωση (denotation). Στην εξίσωση \( 27 \times 37 = 999 \) οι όροι των δύο μελών δηλώνουν μέν, αναφέρονται στο ίδιο πράμα, εννοώντας το όμως, νοηματοδοτώντας το, διαφορετικά: αριστερά ως γινόμενο, δεξιά ως σταθερά. Πρόκειται όντως για ριζική διάκριση στη λογική –την οποία, φλασιά, πιάνει ωραία και ο Ντοβέκ στις «Μεταμορφώσεις του λογισμού» (αξιοδιάβαστο εκλαϊκευμένο, απ' τα ελάχιστα για το σινάφι μας, και σίγουρα, απ' όσο ξέρω, το μόνο στα ελληνικά· ήθελα εδώ και καιρό να γράψω γι' αυτό, κρατούμενο).
Μ' αυτήν τη διάκριση κατανού, και με βάση το γεγονός οτι το νόημα, όπως το καταλαβαίνουμε εδωπέρα, το προσδιορίζουμε συντακτικά, ενώ τη δήλωση σημασιολογικά, έχεις προφανώς οτι δύο όροι \(t_1\) και \(t_2\) με το ίδιο νόημα, παναπεί με την ίδια συντακτική διατύπωση, θα έχουν ασφαλώς και την ίδια δήλωση:
\[t_1 = t_2 \to \denote{t_1} = \denote{t_2} \ ,\]
ενώ το αντίστροφο δέν ισχύει πάντα, όπως δείχνει η πιό πάνω εξίσωση. Η παρατήρηση εδώ είναι βέβαια οτι άλλη ισότητα έχουμε για νοήματα (αυτή που προκύπτει απο την όποια λειτουργική σημασιολογία), άλλη για δηλώσεις (αυτήν που ορίζεται απ' την όποια δηλωτική σημασιολογία, στο όποιο μοντέλο δηλαδή), άλλο αν τις γράφω εδώ το ίδιο.
Συνεχίζει με άλλη μία καλή διάκριση, αυτήν τη φορά μέσα στο πεδίο της σημασιολογίας, ανάμεσα στη σχολή Τάρσκι και τη σχολή Χάιτινγκ. Η μέν ερμηνεύει τους τελεστές ξερά, «ταυτολογικά», αποσκοπώντας στην αλήθεια: \(A \to B\) να σημαίνει «άν η \(A\) αληθεύει, τότε αληθεύει και η \(B\)»· η δέ τους ερμηνεύει συναρτησιακά, αποσκοπώντας στην αποδειξιμότητα: \(A \to B\) να σημαίνει «υπάρχει συνάρτηση \(f\) που απεικονίζει αποδείξεις \(p\) της \(A\) σε αποδείξεις \(f(p)\) της \(B\)» (ο Ζιράρ λέει απλά «Χάιτινγκ», αλλα βέβαια μιλάει για τη γνωστή ερμηνεία BHK, που πλέον αποδίδεται αποκοινού σε Μπράουερ, Χάιτινγκ και Κολμογκόροφ).
Σημειώνει πως η ερμηνεία αλα Τάρσκι, άν και απλοϊκή, ευνόησε την άνθηση της μοντελοθεωρίας, ενώ η ερμηνεία αλα Χάιτινγκ, άν και βαθύτερη, απαιτεί με τη μία να δουλέψουμε κατασκευαστικά. Και κλείνει το κεφάλαιο προοικονομώντας τη σύνδεση της BHK με την αντιστοιχία Κάρι-Χάουαρντ.
Στα Κεφάλαια 2 και 3 στήνει την αντιστοιχία Κάρι-Χάουαρντ, την αντιστοιχία δηλαδή μεταξύ συμπερασμών στο σύστημα της φυσικής απαγωγής του Γκέντσεν (αλα Πράβιτς), και όρων του έντυπου λαμδαλογισμού. Το κάνει αρκετά φιλότιμα και παιδαγωγικά (για το τμήμα \( \{\land, \to, \forall\}\) της γλώσσας), ενώ το ρεζουμέ είναι το εξής (για το ευανάγνωστο, γράφω καί \(t : A\) καί \(t^A\) για έναν όρο \(t\) τύπου \(A\)).
Ε λοιπόν, παρά τις γαλλιές το βιβλίο διαβάζεται νεράκι. Αφενός γιατί δέ χάνεται στις λεπτομέρειες, κι αφετέρου λόγω γαλλιάς καλώς εννοούμενης: ο Ζιράρ τό 'χει με το μπλαμπλά, και δέν εχει πέσει και στη λούμπα της πολιτικής ορθότητας που μαστίζει το σινάφι απ' άκρη σ' άκρη. Γουστάρεις να τον διαβάζεις κι ας μή συμφωνείς. Ο συνδυασμός αυτών των δύο πάντως είναι επικίνδυνος: μπορεί κανείς να το ξεφυλλίσει σε μεγάλο βαθμό, παραλείποντας κάθε απόδειξη, και στο τέλος, χωρίς να έχει σκοντάψει συχνά, να έχει την αίσθηση οτι κάτι έκανε· στην πραγματικότητα, είναι πολύ πιθανό να έχει απλά αποκομίσει καναδυό τρία συνθήματα, που δέ θα μπορέσει να υποστηρίξει αν χρειαστεί. Αλλα εντάξει, αυτή ειναι η γνωστή ιδιοτροπία του καλογραμμένου μαθηματικού κειμένου, οτι διαβάζεται και σάν εφημερίδ' απο παιδί: μόνο τις γελοιογραφίες.
Τα δύο χάιλαϊτ του βιβλίου είναι μάλλον το σύστημα F (ή «σύστημα Ζιράρ-Ρέινολντς», αφού δέν πρόκειται μόνο για πατέντα του Ζάν-Ύβ) και η γραμμική λογική, καί τα δύο θέματα που είχε εισάξει ο Ζιράρ κάμποσα και κάποια χρόνια νωρίτερα. Το ισχυρά κανονικοποιήσιμο του συστήματος F είναι και ένα απ' τα ανδραγαθήματα του Ζιράρ, καθώς πρόκειται για απόδειξη της συνέπειας της ανάλυσης. Προσωπικά όμως ήθελα πάντα να δώ την προσέγγισή του στη δηλωτική σημασιολογία, και δή τους «χώρους συνάφειας» (coherence spaces), που τους χρησιμοποιεί αντί για τα πεδία Σκότ, και είναι βέβαια και το μοντέλο που χρησιμοποιεί για να σημασιοδοτήσει τη γραμμική λογική του.
Άς τα πάρουμε με τη σειρά. \(\newcommand{\denote}[1]{[\![ #1 ]\!]}\)
Νόημα και αναφορά
Ξεκινάει το Κεφάλαιο 1 πατώντας στον παππού Φρέγκε και τη θεμελιακή του διάκριση ανάμεσα σε νόημα (sense) και αναφορά (reference) ή, στα καθημάς, δήλωση (denotation). Στην εξίσωση \( 27 \times 37 = 999 \) οι όροι των δύο μελών δηλώνουν μέν, αναφέρονται στο ίδιο πράμα, εννοώντας το όμως, νοηματοδοτώντας το, διαφορετικά: αριστερά ως γινόμενο, δεξιά ως σταθερά. Πρόκειται όντως για ριζική διάκριση στη λογική –την οποία, φλασιά, πιάνει ωραία και ο Ντοβέκ στις «Μεταμορφώσεις του λογισμού» (αξιοδιάβαστο εκλαϊκευμένο, απ' τα ελάχιστα για το σινάφι μας, και σίγουρα, απ' όσο ξέρω, το μόνο στα ελληνικά· ήθελα εδώ και καιρό να γράψω γι' αυτό, κρατούμενο).
Μ' αυτήν τη διάκριση κατανού, και με βάση το γεγονός οτι το νόημα, όπως το καταλαβαίνουμε εδωπέρα, το προσδιορίζουμε συντακτικά, ενώ τη δήλωση σημασιολογικά, έχεις προφανώς οτι δύο όροι \(t_1\) και \(t_2\) με το ίδιο νόημα, παναπεί με την ίδια συντακτική διατύπωση, θα έχουν ασφαλώς και την ίδια δήλωση:
\[t_1 = t_2 \to \denote{t_1} = \denote{t_2} \ ,\]
ενώ το αντίστροφο δέν ισχύει πάντα, όπως δείχνει η πιό πάνω εξίσωση. Η παρατήρηση εδώ είναι βέβαια οτι άλλη ισότητα έχουμε για νοήματα (αυτή που προκύπτει απο την όποια λειτουργική σημασιολογία), άλλη για δηλώσεις (αυτήν που ορίζεται απ' την όποια δηλωτική σημασιολογία, στο όποιο μοντέλο δηλαδή), άλλο αν τις γράφω εδώ το ίδιο.
Ερμηνεία των λογικών τελεστών
Συνεχίζει με άλλη μία καλή διάκριση, αυτήν τη φορά μέσα στο πεδίο της σημασιολογίας, ανάμεσα στη σχολή Τάρσκι και τη σχολή Χάιτινγκ. Η μέν ερμηνεύει τους τελεστές ξερά, «ταυτολογικά», αποσκοπώντας στην αλήθεια: \(A \to B\) να σημαίνει «άν η \(A\) αληθεύει, τότε αληθεύει και η \(B\)»· η δέ τους ερμηνεύει συναρτησιακά, αποσκοπώντας στην αποδειξιμότητα: \(A \to B\) να σημαίνει «υπάρχει συνάρτηση \(f\) που απεικονίζει αποδείξεις \(p\) της \(A\) σε αποδείξεις \(f(p)\) της \(B\)» (ο Ζιράρ λέει απλά «Χάιτινγκ», αλλα βέβαια μιλάει για τη γνωστή ερμηνεία BHK, που πλέον αποδίδεται αποκοινού σε Μπράουερ, Χάιτινγκ και Κολμογκόροφ).
Σημειώνει πως η ερμηνεία αλα Τάρσκι, άν και απλοϊκή, ευνόησε την άνθηση της μοντελοθεωρίας, ενώ η ερμηνεία αλα Χάιτινγκ, άν και βαθύτερη, απαιτεί με τη μία να δουλέψουμε κατασκευαστικά. Και κλείνει το κεφάλαιο προοικονομώντας τη σύνδεση της BHK με την αντιστοιχία Κάρι-Χάουαρντ.
Φυσική απαγωγή και έντυπος λογισμός λάμδα
Στα Κεφάλαια 2 και 3 στήνει την αντιστοιχία Κάρι-Χάουαρντ, την αντιστοιχία δηλαδή μεταξύ συμπερασμών στο σύστημα της φυσικής απαγωγής του Γκέντσεν (αλα Πράβιτς), και όρων του έντυπου λαμδαλογισμού. Το κάνει αρκετά φιλότιμα και παιδαγωγικά (για το τμήμα \( \{\land, \to, \forall\}\) της γλώσσας), ενώ το ρεζουμέ είναι το εξής (για το ευανάγνωστο, γράφω καί \(t : A\) καί \(t^A\) για έναν όρο \(t\) τύπου \(A\)).
Σε μία υπόθεση αντιστοιχεί μία μεταβλητή:
\[\frac{}{A} \qquad \qquad x^A : A \ .\]
Σε μία εισαγωγή σύζευξης αντιστοιχεί ένα ζεύγος:
\[\frac{A \quad B}{A \land B} \qquad \qquad \langle t_1^A, t_2^B\rangle : A \times B \ ,\]
ενώ σε απαλοιφή σύζευξης αντιστοιχεί προβολή
\[\frac{A \land B}{A} \qquad \qquad \pi^1 t^{A \times B} : A\]
\[\frac{A \land B}{B} \qquad \qquad \pi^2 t^{A \times B} : B \ .\]
Απο δώ παίρνουμε τις εξισώσεις
\[ \pi^1 \langle t_1, t_2 \rangle = t_1 \\ \pi^2 \langle t_1, t_2 \rangle = t_2 \\ \langle \pi^1 t, \pi^2 t \rangle = t \ .\]
Σε μία εισαγωγή συνεπαγωγής αντιστοιχεί μιά λαμδαφαίρεση:
\[\frac{\begin{array}{c} \left[A\right] \\ \vdots \\ B \end{array}}{A \to B} \qquad \qquad \lambda x^A.t^B : A \to B \ ,\]
ενώ σε μιά απαλοιφή συνεπαγωγής (μόντους πόνενς) αντιστοιχεί μιά εφαρμογή:
\[\frac{A \quad A \to B}{B} \qquad \qquad t^{A \to B} s^A : B \ .\]
Απο δώ παίρνουμε επιπλέον άλλες δύο εξισώσεις:
\[ (\lambda x. t) s = t [s / x] \\ \lambda x. t x = t \ ,\]
οπου στην τελευταία δέν επιτρέπεται η \( x \) νά 'ν' ελεύθερη στον \(t\). Η πρότελευταία είναι η γνωστή βήτα μετατροπή ενώ η τελευταία λέγεται ήτα μετατροπή. Τέλος, εντελώς παρόμοια με την περίπτωση του τελεστή συνεπαγωγής, σε μία εισαγωγή καθολικής ποσόδειξης αντιστοιχεί μιά λαμδαφαίρεση:
Προαναγγέλεται εδώ το θεώρημα κανονικοποίησης: το σύστημα αναγωγής που προκύπτει απο τις παραπάνω εξισώσεις (θεωρώντας τες ώς κανόνες αναγωγής, απο τ' αριστερά προς τα δεξιά) είναι συνεπές και αποφασίσιμο.
Πιό συγκεκριμένα, λέμε έναν όρο ανάγωγο (ή κανονικό) άν δέν περιέχει αναγώγιμα (ρέντεξ στ' αγγλικά), δηλαδή υποόρους της μορφής \( \pi^1 \langle t_1, t_2 \rangle\), \(\pi^2 \langle t_1, t_2 \rangle\) ή \( (\lambda x. t) s \), ενώ το σύστημα αναγωγής είναι ο ανακλαστικομεταβατικός κλεισμός των κανόνων
\[ \pi^1 \langle t_1, t_2 \rangle \mapsto t_1 \qquad \pi^2 \langle t_1, t_2 \rangle \mapsto t_2 \qquad (\lambda x. t) s \mapsto t [s / x] \ .\]
Γράφει \( t \leadsto s \) άν ο όρος \(t\), μετατροπή τη μετατροπή, ανάγεται στον όρο \(s\).
(συνεχίζεται)
\[\frac{B}{\forall_x B} \qquad \qquad \lambda x. t^B : \lambda_x B \ ,\]
ενώ σε μιά απαλοιφή καθολικής ποσόδειξης αντιστοιχεί μιά εφαρμογή:
\[\frac{s \quad \forall_x B}{B[s/x]} \qquad \qquad t^{\forall_x B} s : B[s/x] \ ,\]
οπου η \(x\) δέν επιτρέπεται νά 'ν' ελεύθερη στον \(t\). Απο δώ παίρνουμε εντελώς παρόμοιες εξισώσεις μ' αυτές της συνεπαγωγής.
Οι εξισώσεις ώς κανόνες αναγωγής
Προαναγγέλεται εδώ το θεώρημα κανονικοποίησης: το σύστημα αναγωγής που προκύπτει απο τις παραπάνω εξισώσεις (θεωρώντας τες ώς κανόνες αναγωγής, απο τ' αριστερά προς τα δεξιά) είναι συνεπές και αποφασίσιμο.
Πιό συγκεκριμένα, λέμε έναν όρο ανάγωγο (ή κανονικό) άν δέν περιέχει αναγώγιμα (ρέντεξ στ' αγγλικά), δηλαδή υποόρους της μορφής \( \pi^1 \langle t_1, t_2 \rangle\), \(\pi^2 \langle t_1, t_2 \rangle\) ή \( (\lambda x. t) s \), ενώ το σύστημα αναγωγής είναι ο ανακλαστικομεταβατικός κλεισμός των κανόνων
\[ \pi^1 \langle t_1, t_2 \rangle \mapsto t_1 \qquad \pi^2 \langle t_1, t_2 \rangle \mapsto t_2 \qquad (\lambda x. t) s \mapsto t [s / x] \ .\]
Γράφει \( t \leadsto s \) άν ο όρος \(t\), μετατροπή τη μετατροπή, ανάγεται στον όρο \(s\).
(συνεχίζεται)
