Μετάβαση στο περιεχόμενο
Topos Uranos
Ελληνικά

Ο αλγόριθμος των κανονικών μορφών και οι εφαρμογές του

Περίληψη

Το μάθημα για τις κανονικές μορφές απέδειξε ότι κάθε τύπος είναι ισοδύναμος με μια διαζευκτική και με μια συζευκτική κανονική μορφή· αυτό το μάθημα διδάσκει πώς να τις υπολογίζουμε χωρίς τον πίνακα και πώς να τις χρησιμοποιούμε. Ο υπολογισμός είναι ένας αλγόριθμος επανεγγραφής σε τρεις φάσεις: απαλείφονται η διπλή συνεπαγωγή, η αποκλειστική διάζευξη, η κοινή άρνηση και η συνεπαγωγή· οι αρνήσεις μεταφέρονται ως τις μεταβλητές με τους νόμους του Ντε Μόργκαν και τη διπλή άρνηση· και γίνεται επιμερισμός, της σύζευξης ως προς τη διάζευξη για τη διαζευκτική μορφή και της διάζευξης ως προς τη σύζευξη για τη συζευκτική. Αποδεικνύονται η ορθότητά του, που είναι συνέπεια της σημασιολογικής αντικατάστασης, και ο τερματισμός του, με ένα αριθμητικό μέτρο που μειώνεται σε κάθε βήμα κάθε φάσης· και αποδεικνύεται επίσης το όριό του: η συζευκτική μορφή μιας διάζευξης nn συζεύξεων δύο μεταβλητών έχει αναγκαστικά 2n2^n φράσεις. Έπειτα οι κανονικές μορφές λαμβάνονται από τον πίνακα αληθείας μιας συσκευής της οποίας το εσωτερικό δεν φαίνεται, απλοποιούνται με συγχώνευση γειτονικών γραμμών και μετατρέπονται σε κυκλώματα διακοπτών σε σειρά και παράλληλα. Το πρόβλημα μιας συσκευής με τέσσερις διακόπτες λύνεται πλήρως, με τον πίνακά του, τις δύο μορφές του και τα κυκλώματά του· το πρόβλημα με πέντε μένει ως πρόκληση.

Μαθησιακοί στόχοι

  1. Εφαρμογή του αλγορίθμου επανεγγραφής για την εύρεση μιας διαζευκτικής και μιας συζευκτικής κανονικής μορφής ενός τύπου, επιλέγοντας την απαλοιφή της διπλής συνεπαγωγής που ταιριάζει ανάλογα με τη θέση όπου εμφανίζεται.
  2. Απόδειξη ότι ο αλγόριθμος είναι ορθός, μέσω της σημασιολογικής αντικατάστασης, και ότι τερματίζει, με μέτρα που μειώνονται σε κάθε βήμα· και εξήγηση του γιατί η συζευκτική μορφή μπορεί να είναι εκθετικά μακρύτερη από τον αρχικό τύπο.
  3. Κατασκευή των κανονικών μορφών ενός μαύρου κουτιού από τον πίνακα αληθείας του και απλοποίησή τους με συγχώνευση γειτονικών γραμμών.
  4. Αναπαράσταση κυκλωμάτων διακοπτών σε σειρά και παράλληλα με τύπους, και σχεδίαση και απλοποίηση κυκλωμάτων που ικανοποιούν μια προδιαγραφή δοσμένη σε φυσική γλώσσα.

Το μάθημα για τις κανονικές μορφές έδωσε δύο αποδείξεις της ύπαρξής τους. Η πρώτη περνά από τον πίνακα αληθείας, που έχει 2n2^n γραμμές για nn μεταβλητές· η δεύτερη διατρέχει τον τύπο από τις μεταβλητές ακολουθώντας τον μοναδικό κανόνα σχηματισμού του. Καμία από τις δύο δεν λέει πώς να προχωρήσουμε μπροστά σε έναν τύπο γραμμένο με συνεπαγωγές, διπλές συνεπαγωγές και εμφωλευμένες αρνήσεις, που είναι ο τρόπος με τον οποίο συνήθως παρουσιάζονται οι τύποι. Αν αυτό ισχύει, λείπει μια διαδικασία που να δουλεύει πάνω στην ίδια τη γραφή, που να μπορεί να εκτελεστεί χωρίς σκέψη, για την οποία να είναι βέβαιο ότι τερματίζει και ότι δίνει έναν ισοδύναμο τύπο. Αυτό είναι ένας αλγόριθμος, και η μελέτη του είναι το πρώτο αντικείμενο αυτού του μαθήματος· το δεύτερο είναι ό,τι γίνεται με αυτόν: η περιγραφή με τύπους της συμπεριφοράς μιας συσκευής και η κατασκευή ενός κυκλώματος που την αναπαράγει.

Γραφές και αντικατάσταση

Υπενθυμίζεται ότι οι τύποι του κύκλου μαθημάτων είναι συμβολοσειρές κύκλων και δίσκων, και ότι οι ¬\neg, ∨\vee, ∧\wedge, →\rightarrow, ↔\leftrightarrow και ⊻\veebar είναι συντομογραφίες που ορίζονται με βάση την κοινή άρνηση (μάθημα για τη γλώσσα της προτασιακής λογικής). Όταν γράφουμε ((p∨q)→(¬q∧p))((p \vee q) \rightarrow (\neg q \wedge p)) δεν γράφουμε τη συμβολοσειρά, αλλά μια γραφή της: ένα δένδρο του οποίου τα φύλλα είναι μεταβλητές και οι κόμβοι είναι οι σύνδεσμοι ¬\neg, ∧\wedge, ∨\vee, →\rightarrow, ↔\leftrightarrow, ⊻\veebar και ↓\downarrow, ο καθένας με τις συνιστώσες του. Κάθε γραφή δηλώνει έναν μόνο τύπο, εκείνον που προκύπτει από την ανάπτυξη των συντομογραφιών της· και ένας ίδιος τύπος μπορεί να έχει πολλές γραφές: το μάθημα για τις κανονικές μορφές παρατήρησε ότι οι ¬¬φ\neg\neg\varphi και (φ∨φ)(\varphi \vee \varphi) είναι η ίδια συμβολοσειρά. Ο αλγόριθμος διαβάζει τη γραφή, όχι τη συμβολοσειρά· γι' αυτό είναι χρήσιμο να τις διακρίνουμε. Επειδή η διάκριση έχει σημασία μόνο για να ξέρουμε πού δρα κάθε βήμα, θα χρησιμοποιούμε τα γράμματα φ\varphi, ψ\psi, χ\chi για γραφές και για τους τύπους που δηλώνουν, και θα γράφουμε φ≡ψ\varphi \eqsem \psi όταν οι δηλούμενοι τύποι είναι σημασιολογικά ισοδύναμοι. Μια επιμέρους γραφή μιας γραφής είναι το υποδένδρο που έχει ρίζα έναν από τους κόμβους της.

Ένα βήμα του αλγορίθμου αντικαθιστά μια επιμέρους γραφή με μια άλλη. Το εργαλείο που εγγυάται ότι αυτή η αλλαγή δεν μεταβάλλει τη σημασία είναι το θεώρημα σημασιολογικής αντικατάστασης του μαθήματος για τη σημασιολογική συνέπεια και ισοδυναμία· όμως εκείνο το θεώρημα αντικαθιστά μία εμφάνιση στη συμβολοσειρά, και μια επιμέρους γραφή μπορεί να αντιστοιχεί σε πολλές εμφανίσεις στη συμβολοσειρά, επειδή κάθε συντομογραφία αντιγράφει τις συνιστώσες της: στην (φ∨ψ)=((φ↓ψ)↓(φ↓ψ))(\varphi \vee \psi) = ((\varphi \downarrow \psi) \downarrow (\varphi \downarrow \psi)), η συνιστώσα φ\varphi εμφανίζεται δύο φορές. Το επόμενο λήμμα προσαρμόζει την αντικατάσταση στις γραφές.

ΛήμμαΑντικατάσταση σε μια γραφή

Έστω χ\chi μια γραφή, θ\theta μία από τις επιμέρους γραφές της και θ′\theta' μια γραφή με θ≡θ′\theta \eqsem \theta'. Αν η χ′\chi' προκύπτει από την αντικατάσταση αυτής της επιμέρους γραφής της χ\chi με την θ′\theta', τότε χ≡χ′\chi \eqsem \chi'.

Απόδειξη

  1. χ′=θ′≡θ=χ\chi' = \theta' \eqsem \theta = \chi

    Με επαγωγή στο βάθος του κόμβου όπου έχει ρίζα η θ\theta, δηλαδή στο πλήθος των συνδέσμων της χ\chi που βρίσκονται πάνω από αυτόν. Αν το βάθος είναι 00, η επιμέρους γραφή είναι ολόκληρη η γραφή.

  2. χ=c(χ1,χ2),χ′=c(χ1′,χ2),χ1′≡χ1\dato{hi}{\chi = c(\chi_1, \chi_2), \qquad \chi' = c(\resaltar{\chi_1'}, \chi_2), \qquad \chi_1' \eqsem \chi_1}

    Αν είναι μεγαλύτερο από 00, η ρίζα της χ\chi είναι ένας σύνδεσμος cc με συνιστώσες χ1\chi_1 (και χ2\chi_2, αν ο cc είναι διμελής), και η θ\theta έχει ρίζα μέσα σε μία από αυτές, ας πούμε την χ1\chi_1, σε μικρότερο βάθος. Από την επαγωγική υπόθεση, η αλλαγή μέσα στην χ1\chi_1 δίνει μια ισοδύναμη γραφή.

  3. v(χ′)=Fc(v(χ1′),v(χ2))=Fc(v(χ1),v(χ2))=v(χ)v(\chi') = F_c\left( v(\chi_1'), v(\chi_2) \right) = F_c\left( v(\chi_1), v(\chi_2) \right) = v(\chi)

    Από το θεώρημα των τιμών των παράγωγων συνδέσμων (μάθημα για τη σημασιολογία της προτασιακής λογικής) και από τον όρο της κοινής άρνησης, η τιμή της c(χ1,χ2)c(\chi_1, \chi_2) σε μια αποτίμηση είναι συνάρτηση των τιμών των χ1\chi_1 και χ2\chi_2, και αυτές δεν αλλάζουν. Επομένως οι χ\chi και χ′\chi' έχουν την ίδια τιμή σε κάθε αποτίμηση.

Εδώ FcF_c είναι η συνάρτηση αληθείας του συνδέσμου: F¬(a)=1−aF_\neg(a) = 1 - a, F∧(a,b)=abF_\wedge(a, b) = ab, και ούτω καθεξής για τους υπόλοιπους. Το ίδιο αποτέλεσμα προκύπτει από το θεώρημα σημασιολογικής αντικατάστασης εφαρμόζοντάς το μία φορά για κάθε αντίγραφο της θ\theta στη συμβολοσειρά και αλυσιδώνοντας τις ισοδυναμίες με τη μεταβατικότητα· η απόδειξη μέσω της γραφής είναι συντομότερη επειδή μετρά τους γραμμένους συνδέσμους και όχι τα αντίγραφα.