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

Agda

Συνήθης χρήση: Τυπικές αποδείξεις και εξαρτημένοι τύποι.

Προτεινόμενη επέκταση αρχείου: .agda.

Εκτέλεση / περιβάλλον: Έλεγχος τύπων με agda (δεν είναι αυτόνομο εκτελέσιμο).

Αρχικό παράδειγμα

module Hello where
open import Agda.Builtin.Nat
answer : Nat
answer = 42

Πώς διαβάζεται

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

Συνηθισμένο λάθος

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

Agda — Αναλυτικός οδηγός εξάσκησης

Μικρή αφετηρία πηγαίου κώδικα

module Hello where
open import Agda.Builtin.Nat
answer : Nat
answer = 42

Περιβάλλον: Typecheck with agda (not a standalone executable example).. Κράτησε αντίγραφο του αρχικού κώδικα και σημείωσε έκδοση εργαλείου. Ξεχώρισε αν η εκτέλεση επιστρέφει τιμή, εμφανίζει κείμενο ή αλλάζει state. Για τις πρώτες δοκιμές χρησιμοποίησε απομονωμένο περιβάλλον, όχι πραγματικούς λογαριασμούς ή δεδομένα.

Ανάλυση του ιδιαίτερου μηχανισμού

Όρισε συνάρτηση σε length-indexed vector που αποκλείει out-of-bounds index. Δοκίμασε να αφαιρέσεις case constructor από απόδειξη.

Διάγνωση κρίσιμου ορίου

Ένα hole είναι ημιτελής απόδειξη. Universe levels και termination εξαρτώνται από έκδοση Agda.

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

Μια ελάχιστη απόδειξη

Στην Agda μπορείς να εκφράσεις μία μαθηματική πρόταση ως τύπο και μία απόδειξή της ως τιμή. Στο Identity.agda το ίδιο το pattern matching καθορίζει πότε επιτρέπεται ο κατασκευαστής refl.

module Identity where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

same : {A : Set} (x : A) → x ≡ x
same x = refl

Το refl δεν αποδεικνύει αυθαίρετα ότι x ≡ y. Επιτρέπεται όταν οι όροι είναι οριστικά ίσοι σύμφωνα με τον type checker. Προσπάθησε να κατασκευάσεις απόδειξη ότι δύο διαφορετικοί φυσικοί αριθμοί είναι ίσοι με refl και διάβασε το diagnostic που δημιουργείται.

Άσκηση συμμετρίας

Γράψε συνάρτηση symmetry με τύπο {A : Set} {x y : A} → x ≡ y → y ≡ x. Η απόδειξη ολοκληρώνεται με matching στην περίπτωση refl, επειδή τότε οι δύο πλευρές ανάγονται στην ίδια έκφραση. Εξήγησε γιατί αυτό είναι πραγματική ανάλυση μορφής μάρτυρα και όχι ένα cast που παρακάμπτει τον έλεγχο.

Προϋποθέσεις μέσα στον τύπο

Σύγκρινε List A με Vec A n. Για μια συνάρτηση head με input Vec A (suc n), η κενή περίπτωση αποκλείεται ήδη από τον τύπο. Αυτό μεταφέρει μία προϋπόθεση από τον runtime έλεγχο στο όριο εισόδου της συνάρτησης. Δεν σημαίνει, ωστόσο, ότι κάθε πρόγραμμα που περνά type checking έχει και την επιθυμητή επιχειρησιακή συμπεριφορά, αν η προδιαγραφή είναι ανεπαρκής.

Τι δεν θεωρείται απόδειξη

Ένα postulate προσθέτει υπόθεση, δεν τη θεμελιώνει. Ένα hole δείχνει ότι η απόδειξη δεν έχει ολοκληρωθεί. Άφησε προσωρινά έναν στόχο ανοιχτό, παρατήρησε τον interaction mode και στη συνέχεια κλείσε τον χωρίς νέα αξιώματα.

Αποδοχή

Κράτησε αντίγραφο που περνά τον checker και εσκεμμένα λανθασμένο αντίγραφο που αποτυγχάνει. Κατάγραψε έκδοση Agda, flags και ακριβή έξοδο. Το υλικό εδώ είναι σχεδιασμένο για δική σου εκτέλεση, όχι βεβαίωση ότι τα παραδείγματα δοκιμάστηκαν στο audit.