Απόδειξη Ορθότητας Του Μετασχηματισμού Διακλαδιζόμενων Διαστάσεων Στο Coq

Abstract

Σκοπός της διπλωματικής είναι η κωδικοποίηση της απόδειξης ορθότητας του μετασχηματισμού που προτείνεται από τους Π. Ροντογιάννη και W. W. Wadge, από προγράμματα συναρτησιακών γλωσσών ανώτερης τάξης σε σημασιολογικά ισοδύναμα πολυδιάστατα προγράμματα νοηματικού προγραμματισμού που έχουν μόνο συναρτήσεις μηδενικής τάξης, δηλαδή κανένα όρισμα. Ο αλγόριθμος αυτός καταργεί τις συναρτήσεις του πηγαίου προγράμματος κατά αυστηρό και συστηματικό τρόπο με την εισαγωγή κατάλληλων τελεστών χειρισμού των περιβαλλόντων που προκύπτουν σε κάθε στάδιο του μετασχηματισμού. Ο μετασχηματισμός πραγματοποιείται σε M βήματα και σε κάθε στάδιο ο βαθμός του προγράμματος μειώνεται κατά 1. Το αποτέλεσμα είναι ένα M-διάστατο πρόγραμμα νοηματικού προγραμματισμού μηδενικής τάξης. Η μεθοδολογία που αναπτύχθηκε δίνει τις κατευθυντήριες γραμμές για ανάπτυξη νέων τεχνικών υλοποίησης συναρτησιακών γλωσσών προγραμματισμού.