Inductive-inductive definitions

Nordvall Forsberg, Fredrik and Setzer, Anton; Dawar, Anuj and Veith, Helmut, eds. (2010) Inductive-inductive definitions. In: Computer Science Logic. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, CZE, pp. 454-468. ISBN 9783642152047

Full text not available in this repository.Request a copy from the Strathclyde author

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.

Creators(s): Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288 and Setzer, Anton; Dawar, Anuj and Veith, Helmut
Item type:Book Section
ID code:53108
Keywords:axiomatisation, data type, inductive definitions, theorem provers, theoretical model, type theory, Electronic computers. Computer science, Computer Science(all)
Subjects:Science > Mathematics > Electronic computers. Computer science
Department:Faculty of Science > Computer and Information Sciences
Depositing user: Pure Administrator
Date deposited:27 May 2015 14:14
Last modified:16 Dec 2020 04:06
Related URLs:
URI:https://strathprints.strath.ac.uk/id/eprint/53108
Export data:
CORE (COnnecting REpositories)