Λογισμός λάμδα
From Wikipedia, the free encyclopedia
Στη μαθηματική λογική, την πληροφορική και την υπολογιστική γλωσσολογία, λογισμός λάμδα ή λ-λογισμός (αγγλ. lambda calculus ή λ-calculus), είναι ένα τυπικό σύστημα (formal system) σχεδιασμένο για τη διερεύνηση ορισμών, εφαρμογών συναρτήσεων και αναδρομής συναρτήσεων. Δημιουργήθηκε από τους Αλόνζο Τσερτς και Στίβεν Κλέινι τη δεκαετία 1930. Ο Τσερτς χρησιμοποίησε το λογισμό λάμδα για να δώσει αρνητική απάντηση στο πρόβλημα απόφασης (Entscheidungsproblem) του Ντάβιντ Χίλμπερτ. Ο λογισμός λάμδα μπορεί να χρησιμοποιηθεί για να ορίσει τι είναι μια υπολογίσιμη συνάρτηση. Η ερώτηση αν δύο όροι του λογισμού λάμδα είναι ισοδύναμοι (πρόβλημα λέξης, word problem) δε μπορεί να απαντηθεί με ένα γενικό αλγόριθμο. Αυτό ήταν το πρώτο πρόβλημα, πριν ακόμα το πρόβλημα τερματισμού (halting problem) για το οποίο μπορούσε να αποδειχθεί η μη αποφασισιμότητα.
Αυτό το λήμμα ή η ενότητα χρειάζεται ειδικές γνώσεις. Αν γνωρίζετε καλά το θέμα, βελτιώστε το. Δείτε τη σελίδα συζήτησης για λεπτομέρειες. |
Ο λογισμός λάμδα είναι η μικρότερη δυνατή καθολική γλώσσα προγραμματισμού. Αποτελείται από ένα μοναδικό κανόνα μετασχηματισμού (αντικατάσταση μεταβλητών) και ένα μοναδικό τρόπο ορισμού συνάρτησης. Ο λογισμός λάμδα είναι καθολικός με την έννοια ότι οποιαδήποτε υπολογίσιμη συνάρτηση μπορεί να εκφραστεί και να υπολογιστεί χρησιμοποιώντας αυτό το σύστημα. Έτσι, είναι ισοδύναμος με τη μηχανή Τούρινγκ. Παρόλα αυτά, ο λογισμός λάμδα είναι τυποποίηση της υπολογισιμότητας που δίνει έμφαση στη χρήση κανόνων μετασχηματισμού, και δεν ενδιαφέρεται για τη μηχανή που τους υλοποιεί —σχετίζεται περισσότερο με το λογισμικό παρά με το υλικό— και ως τέτοια έχει αποτελέσει τη βάση του λεγόμενου συναρτησιακού προγραμματισμού.