Λογισμός λάμδα

Στη μαθηματική λογική και στην επιστήμη υπολογιστών, λογισμός λάμδα ή λ-λογισμός (αγγλ. lambda calculus ή λ-calculus), είναι ένα τυπικό σύστημα σχεδιασμένο για την διερεύνηση ορισμών, εφαρμογών συναρτήσεων και αναδρομής συναρτήσεων. Δημιουργήθηκε από τους Αλόνζο Τσερτς και Στέφεν Κλέινι τη δεκαετία 1930. Ο Τσερτς χρησιμοποίησε το λογισμό λάμδα για να δώσει αρνητική απάντηση στο πρόβλημα απόφασης (Entscheidungsproblem) του Χίλμπερτ. Ο λογισμός λάμδα μπορεί να χρησιμοποιηθεί για να ορίσει τι είναι μια υπολογίσιμη συνάρτηση. Η ερώτηση αν δυο όροι του λογισμού λάμδα είναι ισοδύναμοι (πρόβλημα λέξης, word problem) δεν μπορεί να απαντηθεί με ένα γενικό αλγόριθμο. Αυτό ήταν το πρώτο πρόβλημα, πριν ακόμα το πρόβλημα τερματισμού (halting problem) για το οποίο μπορούσε να αποδειχθεί η μη αποφασισιμότητα.

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