Λάμβδα λογισμός και αποδείξεις, ισομoρφισμός Curry-Howard

 
Το τεκμήριο παρέχεται από τον φορέα :

Αποθετήριο :
Αποθετήριο «Κάλλιπος»
δείτε την πρωτότυπη σελίδα τεκμηρίου
στον ιστότοπο του αποθετηρίου του φορέα για περισσότερες πληροφορίες και για να δείτε όλα τα ψηφιακά αρχεία του τεκμηρίου*
κοινοποιήστε το τεκμήριο



Λάμβδα λογισμός και αποδείξεις, ισομoρφισμός Curry-Howard (EL)
Lambda calculus and proofs, Curry–Howard isomorphism (EN)

Κολέτσος, Γεώργιος (EL)
Koletsos, Georgios (EN)

Ξύστρα, Αικατερίνη (EL)
Τουλάτου, Δήμητρα (EL)
Δημητρακόπουλος, Κωνσταντίνος (EL)
Κάλλιπος (EL)
Toulatou, Dimitra (EN)
Kallipos (EN)
Ksystra, Aikaterini (EN)
Dimitrakopoulos, Konstantinos (EN)

Εισαγωγή στο λ-λογισμό. Η έννοια της αναγωγής και της κανονικοποίησης. Τα προγράμματα ως λ-όροι. Αναπαραστασιμότητα των συναρτήσεων. Στοιχειώδης προγραμματισμός. Ο λ-λογισμός ως πλαίσιο υπολογισμού ανάλογο των μηχανών Turing. Προγραμματισμός με τύπους, ο λ-λογισμός με τύπους. Το σύστημα των απλών τύπων, το σύστημα T του Gödel και το σύστημα F του Girard. Εκφραστικότητα των συστημάτων με τύπους. Αναδρομικές συναρτήσεις με απόδειξη τερματισμού. Περιγραφή του ισομορφισμού Curry-Howard. Οι φόρμουλες της λογικής ως τύποι της πληροφορικής και οι αποδείξεις μιας φόρμουλας ως προγράμματα αυτού του τύπου. Απόδειξη της ισοδυναμίας, η οποία διατηρεί ισομορφικά την κανονικοποίηση των προγραμμάτων και αντίστοιχα των αποδείξεων. (EL)

learningMaterial
bookChapter

ΛΟΓΙΚΗ ΠΛΗΡΟΤΗΤΑ ΑΝΑΠΟΚΡΙΣΙΜΟΤΗΤΑ ΘΕΩΡΙΑ ΑΠΟΔΕΙΞΕΩΝ ΙΣΟΜΟΡΦΙΣΜΟΣ ΑΠΟΔΕΙΞΕΩΝ ΠΡΟΓΡΑΜΜΑΤΩΝ (EL)
Logic Completeness Undecidability Proof Theory Curry-howard Isomorphism (EN)

Σύνδεσμος Ελληνικών Ακαδημαϊκων Βιβλιοθηκών (EL)
Hellenic Academic Libraries Link (EN)


Σύνδεσμος Ελληνικών Ακαδημαϊκών Βιβλιοθηκών (EL)
Hellenic Academic Libraries Link (EN)

2015



*Η εύρυθμη και αδιάλειπτη λειτουργία των διαδικτυακών διευθύνσεων των συλλογών (ψηφιακό αρχείο, καρτέλα τεκμηρίου στο αποθετήριο) είναι αποκλειστική ευθύνη των αντίστοιχων Φορέων περιεχομένου.