dc.contributor.advisor 
SchroederHeister, Peter (Prof. Dr.) 

dc.contributor.author 
Spahn, Stephan Alexander 

dc.date.accessioned 
20181107T10:42:08Z 

dc.date.available 
20181107T10:42:08Z 

dc.date.issued 
20181107 

dc.identifier.other 
512681562 
de_DE 
dc.identifier.uri 
http://hdl.handle.net/10900/84681 

dc.identifier.uri 
http://nbnresolving.de/urn:nbn:de:bsz:21dspace846815 
de_DE 
dc.identifier.uri 
http://dx.doi.org/10.15496/publikation26071 

dc.description.abstract 
\emph{Inductionrecursion} is a definitional principle in MartinL{\"o}f Type Theory defining families $(\U , \T: \U\to D) : \Fam{D}$ where $D: \Setone$ is an arbitrary fixed (large) set (which in motivating examples is chosen to be $D=\Set$), and $\U : \Set$ is defined by induction while $\T$ is simultaneously defined by recursion on $\U$; the qualifier ``simultaneously'' means here that $\U$ may depend on values of the function $\T : \U \to D$. Two equivalent\footnote{These axiomatizations are equivalent if the underlying logical framework is chosen appropriately.} axiomatizations of this situation were proposed by DybjerSetzer in \cite{dybjer99}\cite{dybjer03}. In both cases a (large) set of \emph{codes} $\DS\; D\; D$ (respectively $\DS'$) for inductiverecursive definitions is defined such that each code $c : \DS\; D\; D$ decodes to an endofunctor $\sem{c} : \Fam{D}\to \Fam{D}$ between categories of families whose initial algebra is the family defined by this code $c$. The authors proved the consistency of their axiomatizations be giving a settheoretic model.
These axiomatizations $\DS$ and $\DS'$ are however not the only reasonable axiomatizations of inductionrecursion. There are at least two ways to come to this conclusion: the more practical one is motivated by the observation that while in the reference theory of inductive definitions it is always possible to compose (in a semantically sound way) two inductive definitions to a single new one, this seems hardly to be the case for the preexisting axiomatizations of InductionRecursion. The second, more conceptual observation about the existing axiomatizations of inductionrecursion is that it does not contain constructors for dependent products (or powers\footnote{There is a close relationship between dependent products, and powers of codes.}) of codes but only for dependent sums of codes. Indeed, we show that these two observations are related by characterizing compositionality of DybjerSetzer inductionrecursion in terms of the existence of powers of codes by sets.
Departing from this characterization, we define and explore two new axiomatizations of inductionrecursion satisfying the mentioned characterization and for which we prove compositionality. In the first one, this is achieved by restricting to a subsystem\footnote{By ``subsystem'' we mean here that there is a semanticspreserving translation from $\UF$ to $\DS$.} $\UF$ of $\DS$ of \emph{uniform codes} for which powers of codes exist. Consistency of this system is established by a semanticspreserving embedding into the system $\DS$.
The second axiomatization $\IR$ of \emph{polynomial codes} (so called since they are based on the idea of iterating polynomials\footnote{Polynomials are also called \emph{containers} and are a formalization for inductive definitions.}) defines a system into which $\DS$ can be embedded and which contains a constructor for dependent products (and in particular powers) of codes. While for $\UF$ the existence of a model can be obtained by embedding it into $\DS$ for which DybjerSetzer themselves devised a (settheoretic) model, we cannot argue in this way for a model of $\IR$ and instead we provide a new model for the latter having almost the same settheoretical assumptions concerning large cardinals: while DybjerSetzer inductionrecursion can be modeled in ZFC supplemented by a Mahlo cardinal and a $0$inaccessible, we need ZFC plus a Mahlo cardinal and a $1$inaccessible.
Since the system $\IR$ does not simply arise by adding a constructor for dependent products of codes to $\DS$ caeteris paribus, but additionally requires redefining all other constructors, the question about constructors generating the image of the inclusion $\DS\hookrightarrow \IR$ imposes itself; we approach this question by defining an intermediary system lying between $\DS$ and $\IR$ and give a translation of this intermediary system into $\DS$. This intermediary system does not only arise by removal of the constructor for dependent products of codes since this did not yet enable us to define a desired translation to $\DS$, but by introduction of an additional uniformity constraint realized by an annotation of codes by binary trees.
A common feature of both new systems $\UF$ and $\IR$ is that they admit a more flexible relation between codes and their subcodes than this is the case for $\DS$: sub$\DS$codes of a given $\DS$code do all have the same type while sub$\UF$, and sub$\IR$codes are not constrained in this way. This latter feature reveals a more abstract way of arriving at the conclusion that DybjerSetzer inductionrecursion is not the most general formulation of inductionrecursion: like inductive definitions can be characterized by a set of operations on sets\footnote{Theses operations are called ``stictly positive operations'' (see \cite{dybjer1996Wtypes}).}, inductiverecursive definitions are also determined by a set of operations on families (namely those represented by the set of functors defined by codes) and DybjerSetzer's systems did not take into account operations that change the (large) set $D$ indexing families while the new systems $\UF$ and $\IR$ do so.
In line with the idea of considering inductionrecursion as contributing to the pursue of the project of formalizing the meta theory of type theory in type theory itself \cite[p.1]{Dybjer96internaltype}, we return to DybjerSetzer's original formalization $\DS$ and provide a \emph{relationallyparametric} model for it that we articulate as a categorieswithfamilies model in the category of reflexive graphs; categorieswithfamilies were proposed in loc.cit. as a formalization of type theory inside type theory that is additionally well adapted to category theoretic reasoning. Relational parametricity is an established and important proof technique to establish metatheoretic properties of type theories. 
en 
dc.language.iso 
en 
de_DE 
dc.publisher 
Universität Tübingen 
de_DE 
dc.rights 
ubtpodok 
de_DE 
dc.rights.uri 
http://tobiaslib.unituebingen.de/doku/lic_mit_pod.php?la=de 
de_DE 
dc.rights.uri 
http://tobiaslib.unituebingen.de/doku/lic_mit_pod.php?la=en 
en 
dc.subject.classification 
Typentheorie , Kategorientheorie , Konstruktive Mathematik , Kompositionalität , Semantik , Intuitionistische Mathematik 
de_DE 
dc.subject.ddc 
004 
de_DE 
dc.subject.ddc 
100 
de_DE 
dc.subject.ddc 
510 
de_DE 
dc.subject.other 
type theory 
en 
dc.subject.other 
category theory 
en 
dc.subject.other 
semantics 
en 
dc.subject.other 
compositionality 
en 
dc.subject.other 
intuitionistic mathematics 
en 
dc.subject.other 
constructive mathematics 
en 
dc.subject.other 
predicativity 
en 
dc.title 
Axiomatizations of Compositional InductiveRecursive Definitions 
en 
dc.type 
PhDThesis 
de_DE 
dcterms.dateAccepted 
20181025 

utue.publikation.fachbereich 
Informatik 
de_DE 
utue.publikation.fakultaet 
7 MathematischNaturwissenschaftliche Fakultät 
de_DE 