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 Citation: Koletsos, G. (2015). Lambda calculus and proofs, Curry–Howard isomorphism [Chapter]. In Koletsos, G. 2015. Μαθηματική λογική [Undergraduate textbook]. Kallipos, Open Academic Editions. chapter 8. http://hdl.handle.net/11419/2307
Language: Greek
Is Part of: Μαθηματική λογική
Publication Origin: Kallipos, Open Academic Editions