datalog — συγκεντρωτικός οδηγός — DedSec Project

Datalog

Η Datalog παράγει σχέσεις από γεγονότα και κανόνες. Το δείγμα αφορά τον μηχανισμό Soufflé και όχι τη σύνταξη της Prolog.

Αναπαραγώγιμο πείραμα

Αποθήκευσε ως paths.dl:

.decl edge(src:symbol, dst:symbol)
.decl reachable(src:symbol, dst:symbol)
.output reachable
edge("a","b").
edge("b","c").
reachable(x,y) :- edge(x,y).
reachable(x,z) :- edge(x,y), reachable(y,z).

Με εγκατεστημένη τη Soufflé, εκτέλεσε souffle -D- paths.dl. Αναμένουμε (a,b), (b,c), (a,c), χωρίς σταθερή σειρά. Ο πρώτος κανόνας βρίσκει άμεσες ακμές και ο δεύτερος επεκτείνει γνωστές διαδρομές. Οι σχέσεις είναι σύνολα, άρα διπλά γεγονότα δεν δημιουργούν διπλές γραμμές.

Διάγνωση και επέκταση

Πρόσθεσε edge("c","a"). και παρατήρησε την αυτοπροσβασιμότητα λόγω κύκλου. Άλλαξε έναν τύπο symbol σε number για να ελέγξεις τη διάγνωση τύπων. Επανέφερε τον τύπο.

Άσκηση: βρες κόμβους με δύο διαφορετικούς εξερχόμενους γείτονες και δοκίμασε κόμβο χωρίς ακμές. Εξήγησε γιατί η αναδρομική προσπελασιμότητα δεν είναι μία απλή SQL join.

Αντιμετώπιση σφαλμάτων: άγνωστη οδηγία μπορεί να σημαίνει διαφορετική διάλεκτο· κενή έξοδος μπορεί να σημαίνει απουσία .output. Έλεγξε τον φάκελο εργασίας και την έκδοση Soufflé.

Τεκμηρίωση: https://souffle-lang.org/datalog-language

Εργαστήριο εξάσκησης: Datalog

Ξεκίνα από το κύριο μάθημα Datalog, το οποίο χρησιμοποιεί το αρχείο paths.dl με τις δηλώσεις .decl edge και .decl reachable. Η εντολή δοκιμής είναι souffle -D- paths.dl σε συμβατή εγκατάσταση. Δεν χρησιμοποιούμε το παλιό παράδειγμα parent("Ada","Grace"), επειδή δεν υπάρχει στο τρέχον βασικό μάθημα.

Αναδρομικό κλείσιμο γράφου

Οι αρχικές ακμές είναι a→b και b→c. Βρες πριν από την εκτέλεση ολόκληρη τη σχέση προσβασιμότητας. Πρέπει να περιέχει ακριβώς (a,b), (b,c) και (a,c), ανεξάρτητα από τη σειρά εκτύπωσης. Ο άμεσος κανόνας δίνει δύο ζεύγη και ο αναδρομικός το τρίτο. Πρόσθεσε edge("c","a")., σχηματίζοντας κύκλο. Τώρα καθένας από τους τρεις κόμβους φτάνει σε όλους, ακόμη και στον εαυτό του: προκύπτουν εννέα διαφορετικά ζεύγη. Διπλό γεγονός ακμής δεν δημιουργεί διπλή έξοδο, γιατί οι σχέσεις είναι σύνολα.

Σχέση ακριβώς δύο ακμών

Διατήρησε τις αρχικές δηλώσεις και πρόσθεσε:

.decl two_hops(src:symbol, dst:symbol)
.output two_hops
two_hops(x,z) :- edge(x,y), edge(y,z).

Χωρίς κύκλο, το μόνο ζεύγος είναι (a,c). Αν προσθέσεις ακμή c→d, προστίθεται το (b,d), όχι όμως το (a,d), που απαιτεί τρία βήματα. Εξήγησε πώς διαφέρει η συγκεκριμένη σύνθεση δύο ακμών από το πλήρες αναδρομικό κλείσιμο. Με κύκλο, μπορεί να εμφανιστεί ζεύγος ίδιου κόμβου.

Ελεγχόμενα σφάλματα

Σε προσωρινό αντίγραφο, χρησιμοποίησε αριθμό σε όρισμα που έχει δηλωθεί ως symbol. Κατάγραψε το πραγματικό διαγνωστικό τύπου από τον Soufflé. Έπειτα αφαίρεσε .output two_hops: το ότι δεν εμφανίζεται μία σχέση στην έξοδο δεν σημαίνει απαραίτητα ότι παύει να υπολογίζεται. Επανέφερε το σωστό αρχείο ανάμεσα στα πειράματα.

Παραδοτέα: τρία αρχικά ζεύγη, εννέα με κύκλο, αποτέλεσμα δύο βημάτων με τέταρτο κόμβο, έκδοση Soufflé και ένα πραγματικό σφάλμα. Χωρίς runtime δήλωσε στατική ανάλυση μόνο.

Datalog — Διαδρομή ουσιαστικής εξάσκησης

Πώς παράγονται νέα facts

Η θετική Datalog δεν εκτελεί «βήματα» σαν ένα τυπικό imperative loop. Οι κανόνες εξάγουν πλειάδες από υπάρχοντα γεγονότα και επαναλαμβάνονται έως ότου δεν προκύπτει τίποτα νέο. Η παρακάτω σημειογραφία είναι λογικό ψευδοπρόγραμμα· ο πραγματικός engine (όπως Soufflé) ενδέχεται να απαιτεί δηλώσεις σχέσεων και διαφορετική σύνταξη εξόδου.

edge(a,b).
edge(b,c).
edge(c,d).
reach(X,Y) :- edge(X,Y).
reach(X,Z) :- reach(X,Y), edge(Y,Z).

Στον πρώτο γύρο τα reach αντιστοιχούν στα τρία edges. Στη συνέχεια εμφανίζονται reach(a,c) και reach(b,d), και αργότερα reach(a,d). Το σταθερό σημείο έρχεται όταν κανένας κανόνας δεν παράγει νέα ζεύγη. Μην ερμηνεύεις τη σειρά εκτύπωσης μιας μη ταξινομημένης σχέσης ως εγγυημένη σειρά διάσχισης.

Κύκλος ως ελεγχόμενο πείραμα

Πρόσθεσε edge(d,a). Πλέον υπάρχει κλειστή διαδρομή από a προς a και μία σωστή reachability σχέση μπορεί να περιέχει reach(a,a). Σε πεπερασμένη θετική Datalog χωρίς function symbols ο αριθμός διαφορετικών συνδυασμών σταθερών είναι περιορισμένος, οπότε το σύνολο συμπερασμάτων σταθεροποιείται. Αυτό δεν ισοδυναμεί με τον τρόπο που μία αφελής recursive Prolog διαδικασία αναζητεί λύσεις.

Δεν είναι απλό SQL self-join

Ένα self-join του edge υπολογίζει διαδρομές ακριβώς δύο ακμών· το αναδρομικό reach καλύπτει αυθαίρετο πεπερασμένο μήκος. Για shortest-path χρειάζονται πρόσθετες τιμές και κατάλληλη σημασιολογία aggregation. Το γεγονός reach(a,d) από μόνο του δεν αποδεικνύει το μικρότερο μήκος.

Έλεγχος απομονωμένων κόμβων

Πρόσθεσε μια σταθερά e χωρίς εισερχόμενες ή εξερχόμενες ακμές και επιβεβαίωσε ότι δεν κατασκευάζεται αυθαίρετη διαδρομή μέσω αυτής. Χρησιμοποίησε toy engine για να καταγράψεις το πλήθος των νέων πλειάδων ανά γύρο. Εξήγησε πώς υπολογίζεται το ελάχιστο σταθερό σημείο, με πραγματική καταγραφή outputs και version. Τα παραδείγματα εδώ δεν παρουσιάζονται ως ήδη εκτελεσμένα.