Inductive-inductive definitions

Fredrik Nordvall Forsberg; Anton Setzer

doi:10.1007/978-3-642-15205-4_35

Inductive-inductive definitions

Fredrik Nordvall Forsberg, Anton Setzer

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

18 Citations (Scopus)

Abstract

We present a principle for introducing new types in type theory which generalises strictly positive indexed inductive data types. In this new principle a set A is defined inductively simultaneously with an A-indexed set B, which is also defined inductively. Compared to indexed inductive definitions, the novelty is that the index set A is generated inductively simultaneously with B. In other words, we mutually define two inductive sets, of which one depends on the other.
Instances of this principle have previously been used in order to formalise type theory inside type theory. However the consistency of the framework used (the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. We give an axiomatisation of the new principle in such a way that the resulting type theory is consistent, which we prove by constructing a set-theoretic model.

Original language	English
Title of host publication	Computer Science Logic
Subtitle of host publication	24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings
Editors	Anuj Dawar, Helmut Veith
Place of Publication	Berlin
Pages	454-468
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-15205-4_35
Publication status	Published - 11 Aug 2010
Event	24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL - Brno, Czech Republic Duration: 23 Aug 2010 → 27 Aug 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	6247
ISSN (Print)	0302-9743

Conference

Conference	24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL
Country/Territory	Czech Republic
City	Brno
Period	23/08/10 → 27/08/10

Keywords

axiomatisation
data type
inductive definitions
theorem provers
theoretical model
type theory

Access to Document

10.1007/978-3-642-15205-4_35

Cite this

Nordvall Forsberg, F., & Setzer, A. (2010). Inductive-inductive definitions. In A. Dawar, & H. Veith (Eds.), Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings (pp. 454-468). (Lecture Notes in Computer Science; Vol. 6247).. https://doi.org/10.1007/978-3-642-15205-4_35

@inproceedings{d367a8219e0f43e2853f86fa845a6782,

title = "Inductive-inductive definitions",

abstract = "We present a principle for introducing new types in type theory which generalises strictly positive indexed inductive data types. In this new principle a set A is defined inductively simultaneously with an A-indexed set B, which is also defined inductively. Compared to indexed inductive definitions, the novelty is that the index set A is generated inductively simultaneously with B. In other words, we mutually define two inductive sets, of which one depends on the other.Instances of this principle have previously been used in order to formalise type theory inside type theory. However the consistency of the framework used (the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. We give an axiomatisation of the new principle in such a way that the resulting type theory is consistent, which we prove by constructing a set-theoretic model.",

keywords = "axiomatisation, data type, inductive definitions, theorem provers, theoretical model, type theory",

author = "{Nordvall Forsberg}, Fredrik and Anton Setzer",

year = "2010",

month = aug,

day = "11",

doi = "10.1007/978-3-642-15205-4_35",

language = "English",

isbn = "9783642152047",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "454--468",

editor = "Anuj Dawar and Helmut Veith",

booktitle = "Computer Science Logic",

note = "24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL ; Conference date: 23-08-2010 Through 27-08-2010",

}

Nordvall Forsberg, F & Setzer, A 2010, Inductive-inductive definitions. in A Dawar & H Veith (eds), Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6247, Berlin, pp. 454-468, 24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL, Brno, Czech Republic, 23/08/10. https://doi.org/10.1007/978-3-642-15205-4_35

Inductive-inductive definitions. / Nordvall Forsberg, Fredrik; Setzer, Anton.
Computer Science Logic: 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. ed. / Anuj Dawar; Helmut Veith. Berlin, 2010. p. 454-468 (Lecture Notes in Computer Science; Vol. 6247).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Inductive-inductive definitions

AU - Nordvall Forsberg, Fredrik

AU - Setzer, Anton

PY - 2010/8/11

Y1 - 2010/8/11

N2 - We present a principle for introducing new types in type theory which generalises strictly positive indexed inductive data types. In this new principle a set A is defined inductively simultaneously with an A-indexed set B, which is also defined inductively. Compared to indexed inductive definitions, the novelty is that the index set A is generated inductively simultaneously with B. In other words, we mutually define two inductive sets, of which one depends on the other.Instances of this principle have previously been used in order to formalise type theory inside type theory. However the consistency of the framework used (the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. We give an axiomatisation of the new principle in such a way that the resulting type theory is consistent, which we prove by constructing a set-theoretic model.

AB - We present a principle for introducing new types in type theory which generalises strictly positive indexed inductive data types. In this new principle a set A is defined inductively simultaneously with an A-indexed set B, which is also defined inductively. Compared to indexed inductive definitions, the novelty is that the index set A is generated inductively simultaneously with B. In other words, we mutually define two inductive sets, of which one depends on the other.Instances of this principle have previously been used in order to formalise type theory inside type theory. However the consistency of the framework used (the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. We give an axiomatisation of the new principle in such a way that the resulting type theory is consistent, which we prove by constructing a set-theoretic model.

KW - axiomatisation

KW - data type

KW - inductive definitions

KW - theorem provers

KW - theoretical model

KW - type theory

UR - http://link.springer.com/

UR - http://mfcsl2010.fi.muni.cz/

U2 - 10.1007/978-3-642-15205-4_35

DO - 10.1007/978-3-642-15205-4_35

M3 - Conference contribution book

SN - 9783642152047

T3 - Lecture Notes in Computer Science

SP - 454

EP - 468

BT - Computer Science Logic

A2 - Dawar, Anuj

A2 - Veith, Helmut

CY - Berlin

T2 - 24th International Workshop on Computer Science Logic, CSL 2010, and 19th Annual Conference of the EACSL

Y2 - 23 August 2010 through 27 August 2010

ER -

Inductive-inductive definitions

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this