Change search
ReferencesLink to record
Permanent link

Direct link
Subsets, quotients and partial functions in Martin-Löf's Type Theory
Stockholm University, Faculty of Science, Department of Mathematics.
2003 In: Types for Proofs and Programs: TYPES 2002, Selected Papers, LNCS 2646, Springer , 2003, 78-94 p.Chapter in book (Other academic) Published
Place, publisher, year, edition, pages
Springer , 2003. 78-94 p.
URN: urn:nbn:se:su:diva-23755ISBN: 3-540-14031-XOAI: diva2:194363
Part of urn:nbn:se:su:diva-475Available from: 2005-04-26 Created: 2005-04-26Bibliographically approved
In thesis
1. Partiality and Choice: Foundational Contributions
Open this publication in new window or tab >>Partiality and Choice: Foundational Contributions
2005 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The subject of the thesis is foundational aspects of partial functions (Papers 1, 2 & 4) and some choice principles (Papers 3 & 4) in the context of constructive mathematics.

Paper 1 studies the inversion functions of commutative rings. The foundational problem of having them only partially defined is overcome by extending them to total functions. This cannot be done constructively unless the rings themselves are extended at the same time. We study such extensions, called wheels. It is investigated how identities for wheels relate to identities for commutative rings.

Paper 2 studies the foundations of partial functions in Martin-Löf's type theory according to the view of subsets as propositional functions, in particular in connection with equivalence relations that the functions are supposed to preserve. The first and second isomorphism theorems of algebra are verified, showing that our approach is flexible enough for some natural mathematical proofs to be carried out.

Paper 3 shows that the difference between the principles of intensional and extensional choice can be described as the principle of excluded middle plus a certain mild extensionality principle, which follows from the principle that functions are identical if they are identical at every point.

Paper 4 studies a constructive calculus of indefinite and definite descriptions. It has the property that it can be interpreted straightforwardly in type theory with all terms referring to individuals. In this respect it differs from other constructive calculi of descriptions, which are known to be conservative extensions of description-free calculi but for which descriptions cannot be interpreted as referring to individuals in general.

The appendix includes a predicative version of Birkhoff's theorem. It states that if a class of algebras is closed under homomorphic images, subalgebras and products and contains a set-indexed family of algebras that satisfies the same identities as the class, then the class can be axiomatized by a set of equations.

Place, publisher, year, edition, pages
Stockholm: Matematiska institutionen, 2005. 132 p.
National Category
urn:nbn:se:su:diva-475 (URN)91-7155-020-8 (ISBN)
Public defence
2005-06-02, sal 14, hus 5, Kräftriket, Stockholm, 10:00
Available from: 2005-04-26 Created: 2005-04-26Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Mathematics

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 20 hits
ReferencesLink to record
Permanent link

Direct link