The theory of recursive functions where the domain of a function is inductively defined at the same time as the function is called induction-recursion. This theory has been introduced in Martin-Lèof type theory by Dybjer and further explored in a series of papers by Dybjer and Setzer. Important data types like universes closed under dependent type operators are instances of this theory. In this thesis we study the class of data types arising from inductive-recursive definitions, taking the seminal work of Dybjer and Setzer as our starting point. We show how the theories of inductive and indexed inductive types arise as sub-theories of induction-recursion, by revealing the role played by a notion of of size within the theory of induction-recursion. We then expand the expressive power of induction-recursion, showing how to extend the theory of induction-recursion in two different ways: in one direction we investigate the changes needed to obtain a more flexible semantics which gives rise to a more comprehensive elimination principle for inductive-recursive types. In another direction we generalize the theory of induction-recursion to a fibrational setting. In both extensions we provide a finite axiomatization of the theories introduced, we show applications and examples of these theories not previously covered by induction-recursion, and we justify the existence of data types built within these theories.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:658934 |
| Date | January 2015 |
| Creators | Malatesta, Lorenzo |
| Publisher | University of Strathclyde |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://oleg.lib.strath.ac.uk:80/R/?func=dbin-jump-full&object_id=24982 |
Page generated in 0.0023 seconds