|
|
Lambda Calculus and type theory (Lamtyp)- Dozent/in
- Dr. Wolfgang Degen
- Angaben
- Vorlesung
2 SWS, benoteter Schein, ECTS-Studium, ECTS-Credits: 2,5
nur Fachstudium
Zeit und Ort: n.V.; Bemerkung zu Zeit und Ort: Zeit und Ort werden noch bekannt gegeben
Vorbesprechung: 19.10.2009, 16:00 - 17:00 Uhr, Raum 0.141
- Voraussetzungen / Organisatorisches
- The lecture will be held either in German or in English, according to the wishes of the students
- Inhalt
- A Lambda-calculus is a theory about function abstraction lambda x. F[x] and function application M(N). The calculus is type free if the expressions M and N have the same type (equivalently: no type). The type free Lambda-calculus is the first model of computation: Every general recursive funtion is Lambda-calculable.
The proof theory and model theory of the type free Lambda-calculus is very rich and interesting. In a Lambda-calculus with types, in the expression M(N) the term M must have a higher type than N. The recursive functions calculable in a Lambda-calculus with types are a proper subset of all recursive functions. A good example is Gödel's system T of all primitive recursive functionals of finite types. T can be used for an informative consistency proof of first-order arithmetic. Type theory e.g. in the sense of Russell can be considered as a certain extension of a Lambda-calculus with types.
- Empfohlene Literatur
- K. Schütte: Proof Theory. Springer 1977.
J.W. Degen: Complete Infinitary Type Logics. Studia Logica 1999.
H. Barendregt: The Lambda Calculus. Its Syntax and Semantics. North Holland, 1984.
H. Barendregt: Lambda Calculi with Types. Oxford 1992.
Hindley and Seldin: Lambda-Calculus and Combinators. Cambridge 2008
- ECTS-Informationen:
- Credits: 2,5
- Zusätzliche Informationen
- Erwartete Teilnehmerzahl: 10
- Institution: Lehrstuhl für Informatik 10 (Systemsimulation)
|
 |
|
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|