Σύστημα Μωντ

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
 Το λήμμα παραθέτει τις πηγές του αόριστα, χωρίς παραπομπές. Βοηθήστε συνδέοντας το κείμενο με τις πηγές χρησιμοποιώντας παραπομπές, ώστε να είναι επαληθεύσιμο.
Η σήμανση τοποθετήθηκε στις 07/02/2020.

Το σύστημα Μωντ (Maude) είναι μια υλοποίηση της λογικής επαναγραφής που αναπτύχθηκε στο SRI International. Η προσέγγισή του γενικά μοιάζει με την υλοποίηση OBJ3 της εξισωτικής λογικής (equational logic) από τον Τζόζεφ Γκωγκέν, αλλά βασίζεται στη λογική επαναγραφής αντί για την εξισωτικής λογικής με διατεταγμένους τύπους (order-sorted equational logic), με έμφαση στον ισχυρό μεταπρογραμματισμό που βασίζεται στην ανάκλαση.

Μωντ - τα βασικά[Επεξεργασία | επεξεργασία κώδικα]

Οι μονάδες (modules) του Μωντ (θεωρίες επαναγραφής, rewrite theories) αποτελούνται από μια γλώσσα όρων και ένα σύνολο από ισότητες και κανόνες επαναγραφής. Οι όροι σε μια θεωρία επαναγραφής κατασκευάζονται με τη χρήση τελεστών ("operators"), που είναι συναρτήσεις που δέχονται 0 ή περισσότερα ορίσματα ενός τύπου (sort) και επιστρέφουν έναν όρο ενός συγκεκριμένου τύπου. Οι τελεστές που δέχονται 0 ορίσματα θεωρούνται σταθερές και η γλώσσα των όρων κατασκευάζεται από αυτές τις απλές δομές.

ΣΗΜΕΙΩΣΗ: Τα παρακάτω προγράμματα μπορούν να εκτελεστούν αν δοθεί στο Μωντ η επιλογή -no-prelude η οποία δεν επιτρέπει στο Μωντ να περιλαμβάνει τις βασικές του ενότητες (όπως την ενότητα NAT του Μωντ που θα προκαλούσε σύγκρουση).

Παράδειγμα 1[Επεξεργασία | επεξεργασία κώδικα]

 fmod NAT is
   sort Nat .

   op 0 : -> Nat [ctor] .
   op s : Nat -> Nat [ctor] .
 endfm

Αυτή η θεωρία επαναγραφής ορίζει όλους τους φυσικούς αριθμούς. Αρχικά εισάγεται ο τύπος, λέγοντας ότι υπάρχει ένα τέτοιο και ονομάζεται ΝΑΤ (συντομογραφία για τους ακέραιους αριθμούς, αγγλ. όρος "natural numbers"), και ακολουθεί η προδιαγραφή που περιγράφει πώς κατασκευάζονται. Ο τελεστής s στο Παράδειγμα 1 είναι η συνάρτηση "επόμενο" ("successor") που αναπαριστά τον επόμενο φυσικό αριθμό στην ακολουθία των φυσικών αριθμών, δηλ. s(N) := N + 1. Ο s(0) εννοείται ότι αναπαριστά το φυσικό αριθμό 1, ακολουθούν όμοια και οι υπόλοιποι. Ο 0 είναι μια σταθερά, δε δέχεται παραμέτρους εισόδου αλλά επιστρέφει έναν Νατ (Nat).

Παράδειγμα 2[Επεξεργασία | επεξεργασία κώδικα]

fmod NAT is
  sort Nat .

  op 0 : -> Nat [ctor] .
  op s : Nat -> Nat [ctor] .
  op _+_ : Nat Nat -> Nat .

  vars N M : Nat .

  eq 0 + N = N .
  eq s(N) + M = s (N + M) .

endfm

Στο Παράδειγμα 2 εισάγεται το σύμβολο + που αναπαριστά την πρόσθεση φυσικών αριθμών. Ο ορισμός του είναι παρόμοιος με τον προηγούμενο, με τύπους εισόδου και εξόδου, αλλά υπάρχει μια διαφορά, ο τελεστής του έχει κάτω παύλες σε κάθε πλευρά. Το Μωντ επιτρέπει στο χρήστη να ορίζει αν ένας τελεστής είναι ανάμεσα στα ορίσματά του (infix), πριν από αυτά (prefix, η προκαθορισμένη συμπεριφορά) ή μετά από αυτά (infix), και αυτό γίνεται με τη χρήση της κάτω παύλας ως θέσης που αντιστοιχεί σε μια παράμετρο εισόδου. Επομένως, ο τελεστής + δέχεται είσοδο και στις δύο πλευρές του, με αποτέλεσμα να ανήκει στην πρώτη κατηγορία (infix). Αντίθετα ο προηγούμενος τελεστής s δεχόταν την είσοδο μετά από αυτόν (prefix). 

op + : Nat Nat -> Nat .
*** είναι το ίδιο με

op +__ : Nat Nat -> Nat . *** δύο κάτω παύλες

Τα τρία αστέρια είναι τα σχόλια μέχρι το τέλος της γραμμής στο Μωντ και λέει στο συντακτικό αναλυτή του Μωντ να αγνοήσει το υπόλοιπο της γραμμής (σαν να μην ανήκει στο πρόγραμμα), με τη χρήση παρενθέσεων προκύπτουν σχόλια σε ενότητα: 

*** το Maude αγνοεί την υπόλοιπη γραμμή
*** (
το Maude
αγνοεί την
υπόλοιπη ενότητα
)

Η εκτεταμένη μονάδα Nat επίσης περιέχει δύο μεταβλητές και δύο σύνολα από ισότητες. 

vars N M : Nat .

eq 0 + N = N .
eq s(N) + M = s (N + M) .

Όταν το Μωντ "εκτελεί", επαναγράφει τους όρους σύμφωνα με τις προδιαγραφές. Αυτό γίνεται με την εντολή: 

reduce in <κάποια μονάδα> : <κάποιος όρος> .

ή με τη συντομογραφία: 

red <κάποιος όρος> .

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

reduce in NAT : s(0) + s(0) .
rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
result Nat: s(s(0))

Χρησιμοποιώντας τις δύο εξισώσεις της θεωρίας επαναγραφής NAT, το Μωντ μπόρεσε να ανάγει τον αρχικό όρο στον επιθυμητό όρο, την αναπαράσταση του αριθμού δύο, δηλ. το μεθεπόμενο αριθμό του 0. Σε αυτό το σημείο δε μπορεί να εφαρμοστεί καμία άλλη εξίσωση και το Μωντ παύει να εκτελείται. Το Μωντ επαναγράφει τους όρους σύμφωνα με τις εξισώσεις όταν υπάρχει ένα ταίριασμα (match) ανάμεσα στους κλειστούς όρους (closed terms) που πρόκειται να επαναγραφούν (ή αναχθούν) και στο αριστερό μέλος (left hand side) μιας από τις εξισώσεις. Σε αυτό το περιβάλλον ένα ταίριασμα είναι μια αντικατάσταση των μεταβλητών στο αριστερό μέλος μιας εξίσωσης, που την αφήνει ίδια με τον όρο που επαναγράφεται/ανάγεται.

Αυτό φαίνεται από το αριστερό μέλος των εξισώσεων καθώς εκτελείται το Μωντ, ανάγοντας/επαναγράφοντας τον όρο. Η παρακάτω: 

eq s(N) + M = s (N + M) .

μπορεί να εφαρμοστεί στον όρο: 

s(0) + s(0)

επειδή η αντικατάσταση: 

N => 0
M => s(0)

s(N) + M [[N => 0, M => s(0)]] == s(0) + s(0)

τους κάνει ίδιους και μπορεί να γίνει αναγωγή/επαναγραφή με χρήση αυτής της εξίσωσης. Όταν αυτή η εξίσωση έχει εφαρμοστεί στον όρο, μένει ο όρος: 

s (0 + s(0))

Στον όρο αυτό ταιριάζει μια αντικατάσταση για την οποία είναι κατάλληλη η πρώτη εξίσωση, με τμήμα του όρου να ταιριάζει με την πρώτη εξίσωση: 

eq 0 + N = N .

Η αντικατάσταση είναι: 

N => s(0)

s (0 + N) [[N => s(0)]] == s (0 + s(0))

0 + s(0) - ταιριάζει με την πρώτη εξίσωση και επαναγράφεται

Όπως φαίνεται, η δεύτερη αντικατάσταση και το βήμα επαναγραφής επαναγράφουν τον εσωτερικό όρο (ο συνολικός όρος δεν ταιριάζει με καμία από τις εξισώσεις αλλά ο εσωτερικός όρος ταιριάζει). Στη συνέχεια προκύπτει ο όρος s(s(0)), ο οποίος αντιστοιχεί στην πρόσθεση 1 + 1.

Πρέπει να τονιστεί ότι οι παραπάνω αναγωγές/επαναγραφές προϋποθέτουν:

  • Η αναγωγή/επαναγραφή να τερματίζει
  • Η αναγωγή/επαναγραφή να συμβάλλουν (confluent, η εφαρμογή των εξισώσεων πρέπει να έχει τον ίδιο όρο ως αποτέλεσμα, ανεξάρτητα από τη σειρά με την οποία εφαρμόζονται)

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

Κανόνες επαναγραφής[Επεξεργασία | επεξεργασία κώδικα]

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

Η ενότητα NAT των ακέραιων αριθμών και της πρόσθεσης, που ήδη παρουσιάστηκε, θεωρείται συναρτησιακή μονάδα (functional module) ή θεωρία επαναγραφής (rewrite theory), γιατί δεν περιέχει κανόνες επαναγραφής. Για αυτόν το λόγο, αυτές οι ενότητες συνήθως περιέχονται ανάμεσα στις λέξεις fmod και endfm (αντί για τις mod και endm). Μια συναρτησιακή μονάδα και οι εξισώσεις της πρέπει να συμβάλλουν και να τερματίζουν γιατί αποτελούν το τμήμα της θεωρίας επαναγραφής που πρέπει πάντα να υπολογίζει το ίδιο αποτέλεσμα, κάτι που θα φανεί και στη συνέχεια, από την περιγραφή της λειτουργίας των κανόνων επαναγραφής.

Παράδειγμα 3[Επεξεργασία | επεξεργασία κώδικα]

mod PERSON is

including NAT . *** η προηγούμενη μονάδα

sort Person .
sort State .

op married : -> State [ctor] .
op divorced : -> State [ctor] .
op single : -> State [ctor] .
op engaged : -> State [ctor] .
op dead : -> State [ctor] .

op person : State Nat -> Person [ctor] .

var N : Nat .
var S : State .

rl [birthday] :

person (S, N) => person (S, N + s(0)) .

rl [get-engaged] :

person (single, N) => person (engaged, N) .

rl [get-married] :

person (engaged, N) => person (married, N) .

rl [get-divorced] :

person (married, N) => person (divorced, N) .

rl [las-vegas] :

person (S, N) => person (married, N) .

rl [die] :

person (S, N) => person (dead, N) .

endm

Αυτή η ενότητα εισάγει δύο νέους τύπους και ένα σύνολο από κανόνες επαναγραφής. Περιέχεται επίσης η προηγούμενη μονάδα, για να φανεί η διαφορά μεταξύ εξισώσεων και κανόνων επαναγραφής. Οι κανόνες επαναγραφής μπορούν να θεωρηθούν ως ένα σύνολο από επιτρεπτές αλλαγές κατάστασης και, ενώ οι εξισώσεις διατηρούν την ίδια σημασία και στα δύο μέλη του συμβόλου της ισότητας, οι κανόνες επαναγραφής δεν έχουν αυτήν την ιδιότητα (οι κανόνες επαναγραφής χρησιμοποιούν το σύμβολο => αντί του συμβόλου της ισότητας). Στο παραπάνω παράδειγμα, ένα πρόσωπο, όταν παντρεύεται, δεν αλλάζει αλλά κάτι έχει αλλάξει, τουλάχιστον η οικογενειακή κατάσταση. Αυτό φαίνεται από έναν κανόνα επαναγραφής και όχι μια εξίσωση. Οι κανόνες επαναγραφής δε χρειάζεται να συμβάλλουν και να τερματίζουν, επομένως είναι σημαντικό ποιοι κανόνες επιλέγονται για να επαναγραφεί ένας όρος. Οι κανόνες εφαρμόζονται "τυχαία" από το σύστημα Μωντ, δεν είναι δηλαδή σίγουρο αν κάποιος κανόνας εφαρμόζεται πριν από κάποιον άλλο, κλπ. Αν μια εξίσωση μπορεί να εφαρμοστεί σε έναν όρο, πάντα θα εφαρμόζεται πριν από κάποιον κανόνα επαναγραφής.

Ένα μικρό παράδειγμα:

Παράδειγμα 4[Επεξεργασία | επεξεργασία κώδικα]

rewrite [3] in PERSON : person (single, 0) .

rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second)

result Person: person (married, s(0))

Σε αυτό το παράδειγμα δίνεται η εντολή στο Μωντ να επαναγράψει τον όρο που δίνεται σύμφωνα με τη θεωρία επαναγραφής και να σταματήσει μετά από 3 βήματα επαναγραφής (ένα άνω όριο μπορεί να χρειάζεται επειδή οι κανόνες επαναγραφής δεν είναι απαραίτητο ότι τερματίζουν ή συμβάλλουν), ώστε να φανεί η τελική κατάσταση μετά από την εφαρμογή 3 τυχαία επιλεγμένων κανόνων. Το αποτέλεσμα είναι περίεργο ως έννοια (η ηλικία είναι 1) και εμφανίζει 4 βήματα επαναγραφής (επειδή τα βήματα επαναγραφής από την εφαρμογή εξισώσεων δεν υπολογίζονται, μιας και δεν αλλάζουν τον όρο αν οι εξισώσεις είναι σωστές). Σε αυτό το παράδειγμα χρησιμοποιείται μια από τις εξισώσεις της μονάδας NAT για την αναγωγή του όρου 0 + s(0) σε s(0), στην οποία οφείλεται το 4ο βήμα αναγωγής.

Για να διορθωθεί το παράδειγμα, κάποιοι κανόνες επαναγραφής μπορούν να τροποποιηθούν και να γίνουν κανόνες επαναγραφής υπό συνθήκη (conditional), που σημαίνει ότι πρέπει να ικανοποιούν κάποια επιπλέον κριτήρια (εκτός του ταιριάσματος του αριστερού τους μέλους) για να εφαρμοστούν. 

crl [las-vegas] :

person (S, N) => person (married, N) if (S =/= married) /\ (S =/= dead) .

crl [die] :

person (S, N) => person (dead, N) if (S =/= dead) .

Είναι λογικό ότι ένας άνθρωπος δε μπορεί να πεθάνει αν είναι ήδη νεκρός (dead) και δε μπορεί να παντρευτεί αν είναι ήδη παντρεμένος (married). Το σύμβολο (/\) συμβολίζει το λογικό ΚΑΙ (AND) και σημαίνει ότι πρέπει να ικανοποιούνται και τα δύο επιπλέον κριτήρια για την εφαρμογή του όρου. Οι εξισώσεις μπορούν επίσης να γραφούν υπό συνθήκη με παρόμοιο τρόπο.

Λόγοι χρήσης της Λογικής Επαναγραφής και του Μωντ[Επεξεργασία | επεξεργασία κώδικα]

Το Μωντ στοχεύει στην επίλυση διαφορετικών προβλημάτων από αυτά που χειρίζονται οι συνηθισμένες προστακτικές γλώσσες, όπως η C, η Java ή η Perl. Είναι ένα εργαλείο τυπικής συλλογιστικής που βεβαιώνει το χρήστη ότι κάποιες ιδιότητες είναι σωστές ή δείχνει γιατί αυτές δεν ισχύουν. Το Μωντ επιτρέπει να βρεθεί τυπικά τι σημαίνει μια ιδέα σε αφηρημένο επίπεδο (χωρίς να χρειάζονται λεπτομέρειες της υλοποίησής της), περιγράφοντας τι θεωρείται ισοδύναμο στη θεωρία (εξισώσεις) και πώς μπορεί να αλλάξει (κανόνες επαναγραφής). Αυτό αποδεικνύεται πολύ χρήσιμο στον έλεγχο της ορθότητας πρωτοκόλλων ασφαλείας και σημαντικού κώδικα. Το σύστημα Μωντ έχει αποδείξει σφάλματα σε πρωτόκολλα κρυπτογραφίας, απλά περιγράφοντας τις δυνατότητες του συστήματος (όπως η θεωρία επαναγραφής PERSON), και αναζητώντας μη επιθυμητές καταστάσεις (καταστάσεις ή όρους που δεν είναι επιθυμητό να μπορούν να εμφανιστούν), αποδεικνύονται τα σφάλματα του πρωτοκόλλου. Τα σφάλματα αυτά μπορούν να είναι δύσκολα στην ανίχνευση γιατί συμβολίζουν καταστάσεις εκτός του κλασικού τρόπου λειτουργίας και ο προγραμματιστής μπορεί εύκολα να μην τα έχει υπόψη του.

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

Ακολουθεί άλλο ένα μικρό παράδειγμα της μονάδας PERSON. 

search [1] in PERSON : person (single, 1) =>1 person (married, 2) .

No solution.

Εδώ οι φυσικοί αριθμοί ακολουθούν τον κλασικό συμβολισμό (έχει φορτωθεί η βασική μονάδα prelude.maude του Μωντ με την εντολή "in prelude", ή το 1 μπορεί να αντικατασταθεί από το s(0) και το 2 από το s(s(0)) αν δεν πρόκειται να φορτωθούν οι βασικές ενότητες του Μωντ), γενικά το Μωντ έχει ενσωματωμένη υποστήριξη για συνηθισμένες δομές όπως οι ακέραιοι ή οι αριθμοί κινητής υποδιαστολής. Οι φυσικοί αριθμοί εξακολουθούν να είναι μέλη του ενσωματωμένου τύπου Nat. Δηλώνεται ότι πρόκειται να γίνει αναζήτηση για μια μετάβαση που χρησιμοποιεί έναν κανόνα επαναγραφής (=>1), ο οποίος να επαναγράφει τον πρώτο όρο στον δεύτερο. Το αποτέλεσμα είναι προφανές. Αν επιτραπεί στο Μωντ να χρησιμοποιήσει παραπάνω από ένα βήμα, προκύπτει διαφορετικό αποτέλεσμα: 

search [1] in PERSON : person (single, 1) =>+ person (married, 2) .

Solution 1 (state 7)
states: 8 rewrites: 14 in 0ms cpu (0ms real) (~ rewrites/second)

Η ενσωματωμένη εντολή show path δείχνει ποιες εφαρμογές κανόνων οδηγούν στον τελικό όρο. Το σύμβολο (=>+) σημαίνει μια ή περισσότερες εφαρμογές όρων. 

show path 7 .
state 0, Person: person (single, 1)
===[[rl person(S, N) => person(S, N + 1) [label 'birthday]] .]
===>
state 1, Person: person (single, 2)
===[[crl person(S, N) => person(married, N) if S =/= married = true /\ S =/= dead = true [label las-vegas]] .]
===>
state 7, Person: person (married, 2)

Το επιθυμητό αποτέλεσμα προκύπτει από την εφαρμογή του κανόνα "birthday" και μετά του κανόνα "las-vegas". Η προσέγγιση αυτή δεν ενδείκνυται πάντα γιατί όλες οι θεωρίες επαναγραφής ή οι μονάδες με πολλές πιθανές εφαρμογές κανόνων παράγουν ένα τεράστιο δέντρο πιθανών καταστάσεων που δε μπορεί να χειριστεί από την εντολή search. Μπορεί επίσης να ελεγχθεί ποιος κανόνας μπορεί να χρησιμοποιηθεί σε κάθε βήμα, μέσω μεταπρογραμματισμού λόγω της ανακλαστικής ιδιότητας της λογικής επαναγραφής.

Το Μωντ είναι ελεύθερο λογισμικό και υπάρχει αρκετό εκπαιδευτικό υλικό διαθέσιμο.

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

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

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

Ανακτήθηκε από "https://el.wikipedia.org/w/index.php?title=Σύστημα_Μωντ&oldid=10222009"