Inductive-inductive definitions

Research output: ThesisDoctoral Thesis

Abstract

The principle of inductive-inductive definitions is a principle for defining data types in Martin-Löf Type Theory. It allows the definition of a set A, simultaneously defined with a family B ∶ A → Set indexed over A. Such forms of definitions have been used by several authors in order to for example define the syntax of Type Theory in Type Theory itself. This thesis gives a theoretical justification for their use. We start by giving a finite axiomatisation of a type theory with inductive-inductive definitions in the style of Dybjer and Setzer’s axiomatisation of inductive-recursive definitions. We then give a categorical characterisation of inductive-inductive definitions as initial objects in a certain category. This is presented using a general framework for elimination rules based on the concept of a Category with Families. To show consistency of inductive-inductive definitions, a set-theoretical model is constructed. Furthermore, we give a translation of our theory with a simplified form of the elimination rule into the already existing theory of indexed inductive definitions. This translation does notseem possible for the general elimination rule. Extensions to the theory are investigated, such as a combined theory of inductive-inductive-recursive definitions, more general forms of indexing and arbitrarily high (finite) towers of inductive-inductive definitions.Even so, not all uses of inductive-inductive definitions in the literature (in particular the syntax of Type Theory) are covered by the theories presented. Finally, two larger, novel case studies of the use of inductive-inductive definitions are presented: Conway’s Surreal numbers and a formalisation of positive inductive-recursive definitions.
Original languageEnglish
QualificationPhD
Awarding Institution
  • Swansea University
Supervisors/Advisors
  • Setzer, Anton, Supervisor, External person
Award date22 Jan 2014
Publication statusPublished - 2013

Fingerprint

Inductive Definitions
Towers
Type Theory
Elimination
Axiomatization
Formalization
Justification
Categorical
Indexing
Theoretical Model

Keywords

  • logic
  • Martin-Löf type theory
  • inductive-inductive definitions
  • type theory

Cite this

@phdthesis{a88e933ddf7b4927bd7a1cd21527e79c,
title = "Inductive-inductive definitions",
abstract = "The principle of inductive-inductive definitions is a principle for defining data types in Martin-L{\"o}f Type Theory. It allows the definition of a set A, simultaneously defined with a family B ∶ A → Set indexed over A. Such forms of definitions have been used by several authors in order to for example define the syntax of Type Theory in Type Theory itself. This thesis gives a theoretical justification for their use. We start by giving a finite axiomatisation of a type theory with inductive-inductive definitions in the style of Dybjer and Setzer’s axiomatisation of inductive-recursive definitions. We then give a categorical characterisation of inductive-inductive definitions as initial objects in a certain category. This is presented using a general framework for elimination rules based on the concept of a Category with Families. To show consistency of inductive-inductive definitions, a set-theoretical model is constructed. Furthermore, we give a translation of our theory with a simplified form of the elimination rule into the already existing theory of indexed inductive definitions. This translation does notseem possible for the general elimination rule. Extensions to the theory are investigated, such as a combined theory of inductive-inductive-recursive definitions, more general forms of indexing and arbitrarily high (finite) towers of inductive-inductive definitions.Even so, not all uses of inductive-inductive definitions in the literature (in particular the syntax of Type Theory) are covered by the theories presented. Finally, two larger, novel case studies of the use of inductive-inductive definitions are presented: Conway’s Surreal numbers and a formalisation of positive inductive-recursive definitions.",
keywords = "logic, Martin-L{\"o}f type theory, inductive-inductive definitions, type theory",
author = "{Nordvall Forsberg}, Fredrik",
year = "2013",
language = "English",
school = "Swansea University",

}

Nordvall Forsberg, F 2013, 'Inductive-inductive definitions', PhD, Swansea University.

Inductive-inductive definitions. / Nordvall Forsberg, Fredrik.

2013.

Research output: ThesisDoctoral Thesis

TY - THES

T1 - Inductive-inductive definitions

AU - Nordvall Forsberg, Fredrik

PY - 2013

Y1 - 2013

N2 - The principle of inductive-inductive definitions is a principle for defining data types in Martin-Löf Type Theory. It allows the definition of a set A, simultaneously defined with a family B ∶ A → Set indexed over A. Such forms of definitions have been used by several authors in order to for example define the syntax of Type Theory in Type Theory itself. This thesis gives a theoretical justification for their use. We start by giving a finite axiomatisation of a type theory with inductive-inductive definitions in the style of Dybjer and Setzer’s axiomatisation of inductive-recursive definitions. We then give a categorical characterisation of inductive-inductive definitions as initial objects in a certain category. This is presented using a general framework for elimination rules based on the concept of a Category with Families. To show consistency of inductive-inductive definitions, a set-theoretical model is constructed. Furthermore, we give a translation of our theory with a simplified form of the elimination rule into the already existing theory of indexed inductive definitions. This translation does notseem possible for the general elimination rule. Extensions to the theory are investigated, such as a combined theory of inductive-inductive-recursive definitions, more general forms of indexing and arbitrarily high (finite) towers of inductive-inductive definitions.Even so, not all uses of inductive-inductive definitions in the literature (in particular the syntax of Type Theory) are covered by the theories presented. Finally, two larger, novel case studies of the use of inductive-inductive definitions are presented: Conway’s Surreal numbers and a formalisation of positive inductive-recursive definitions.

AB - The principle of inductive-inductive definitions is a principle for defining data types in Martin-Löf Type Theory. It allows the definition of a set A, simultaneously defined with a family B ∶ A → Set indexed over A. Such forms of definitions have been used by several authors in order to for example define the syntax of Type Theory in Type Theory itself. This thesis gives a theoretical justification for their use. We start by giving a finite axiomatisation of a type theory with inductive-inductive definitions in the style of Dybjer and Setzer’s axiomatisation of inductive-recursive definitions. We then give a categorical characterisation of inductive-inductive definitions as initial objects in a certain category. This is presented using a general framework for elimination rules based on the concept of a Category with Families. To show consistency of inductive-inductive definitions, a set-theoretical model is constructed. Furthermore, we give a translation of our theory with a simplified form of the elimination rule into the already existing theory of indexed inductive definitions. This translation does notseem possible for the general elimination rule. Extensions to the theory are investigated, such as a combined theory of inductive-inductive-recursive definitions, more general forms of indexing and arbitrarily high (finite) towers of inductive-inductive definitions.Even so, not all uses of inductive-inductive definitions in the literature (in particular the syntax of Type Theory) are covered by the theories presented. Finally, two larger, novel case studies of the use of inductive-inductive definitions are presented: Conway’s Surreal numbers and a formalisation of positive inductive-recursive definitions.

KW - logic

KW - Martin-Löf type theory

KW - inductive-inductive definitions

KW - type theory

M3 - Doctoral Thesis

ER -