| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Lutz Schröder |
| Herausgeber: |
Laurent Fribourg |
| Titel: |
Life without the Terminal Type |
| Buch / Sammlungs-Titel: |
Computer Science Logic |
| Band: |
2142 |
| Seite(n): |
429 – 442 |
| Serie / Reihe: |
Lecture Notes in Computer Science |
| Erscheinungsjahr: |
2001 |
| Verleger: |
Springer, Berlin |
| Abstract / Kurzbeschreibung: |
We introduce a method of extending arbitrary categories by a terminal object and apply this method in various type theoretic settings. In particular, we show that categories that are cartesian closed except for the lack of a terminal object have a universal full extension to a cartesian closed category, and we characterize categories for which the latter category is a topos. Both the basic construction and its correctness proof are extremely simple. This is quite surprising in view of the fact that the corresponding results for the simply typed lambda-calculus with surjective pairing, in particular concerning the decision problem for equality of terms in the presence of a terminal type, are comparatively involved.
|
| Internet: |
http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2142&spage=429 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/TermType.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~lschrode/papers/TermType.ps |
| Schlagworte: |
terminal type lambda calculus topos |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
22. 06. 2005 |
