Adobe PDF
(279.37 kB)
| Title Details: | |
|
Lambda calculus and proofs, Curry–Howard isomorphism |
|
| Authors: |
Koletsos, Georgios |
| Reviewer: |
Dimitrakopoulos, Konstantinos |
| Subject: | HUMANITIES AND ARTS > LOGIC AND PHILOSOPHY OF LOGIC HUMANITIES AND ARTS > LOGIC AND PHILOSOPHY OF LOGIC > LOGIC AND PHILOSOPHY OF LOGIC, MISCELLANEOUS > DEDUCTIVE LOGIC MATHEMATICS AND COMPUTER SCIENCE > MATHEMATICS > MATHEMATICAL LOGIC AND FOUNDATIONS MATHEMATICS AND COMPUTER SCIENCE > COMPUTER SCIENCE MATHEMATICS AND COMPUTER SCIENCE > COMPUTER SCIENCE |
| Keywords: |
Logic Completeness Undecidability Proof Theory Curry-howard Isomorphism
|
| Description: | |
| Abstract: |
Εισαγωγή στο λ-λογισμό. Η έννοια της αναγωγής και της κανονικοποίησης. Τα προγράμματα ως λ-όροι. Αναπαραστασιμότητα των συναρτήσεων. Στοιχειώδης προγραμματισμός. Ο λ-λογισμός ως πλαίσιο υπολογισμού ανάλογο των μηχανών Turing.Προγραμματισμός με τύπους, ο λ-λογισμός με τύπους. Το σύστημα των απλών τύπων, το σύστημα T του Gödel και το σύστημα F του Girard. Εκφραστικότητα των συστημάτων με τύπους. Αναδρομικές συναρτήσεις με απόδειξη τερματισμού.Περιγραφή του ισομορφισμού Curry-Howard. Οι φόρμουλες της λογικής ως τύποι της πληροφορικής και οι αποδείξεις μιας φόρμουλας ως προγράμματα αυτού του τύπου. Απόδειξη της ισοδυναμίας, η οποία διατηρεί ισομορφικά την κανονικοποίηση των προγραμμάτων και αντίστοιχα των αποδείξεων.
|
| Linguistic Editors: |
Toulatou, Dimitra |
| Technical Editors: |
Ksystra, Aikaterini |
| Type: |
Chapter |
| Creation Date: | 2015 |
| Item Details: | |
| License: |
http://creativecommons.org/licenses/by-nc-nd/3.0/gr |
| Handle | http://hdl.handle.net/11419/2307 |
| Bibliographic Reference: | Koletsos, G. (2015). Lambda calculus and proofs, Curry–Howard isomorphism [Chapter]. In Koletsos, G. 2015. Μαθηματική λογική [Undergraduate textbook]. Kallipos, Open Academic Editions. https://hdl.handle.net/11419/2307 |
| Language: |
Greek |
| Is Part of: |
Μαθηματική λογική |
| Publication Origin: |
Kallipos, Open Academic Editions |