Η Ρητη Αντικατασταση Στον Λ-λογισμο

Abstract

Σκοπός αυτής της διπλωματικής εργασίας είναι η μελέτη του μεγάλου προβλήματος της "ρητής αντικατάστασης" (Explicit Substitution) στον λάμδα λογισμό. Η αντικατάσταση μιας μεταβλητής από μια άλλη, που τη συναντάμε στη β-αναγωγή , δεν είναι μια απλή διαδικασία. Από πίσω της κρύβονται τεράστιες υπολογιστικές διεργασίες οι οποίες προσδιορίζονται απ’ τους περιορισμούς που θέτει η ίδια η αντικατάσταση. Στον λ-λογισμό αυτό το πρόβλημα δεν ενδιαφέρει. Ο λ-λογισμός είναι ένα μαθηματικό μοντέλο που περιγράφει κάθε τι που είναι υπολογίσιμο και όχι ένα μοντέλο για μια πρακτική υλοποίηση ενός αλγορίθμου. Παρ’ όλα αυτά οι συναρτησιακές γλώσσες, που ολοένα και περισσότερη απήχηση φαίνεται να έχουν, στηρίζονται σ’ αυτόν. Άρα λοιπόν είναι χρήσιμο να υπάρχει ένα αποδοτικό μοντέλο που να προκύπτει απ’ τον λάμδα λογισμό και το οποίο να περιγράφει ακριβώς ποιο είναι το αποτέλεσμα της β-αναγωγής με όσο το δυνατόν πιο κομψό και αποδοτικό τρόπο.