A categorical semantics for inductive-inductive definitions
Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik and Setzer, Anton; Corradini, Andrea and Klin, Bartek and Cîrstea, Corina, eds. (2011) A categorical semantics for inductive-inductive definitions. In: Algebra and Coalgebra in Computer Science. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, GBR, pp. 70-84. ISBN 9783642229435
Full text not available in this repository.Request a copy from the Strathclyde authorAbstract
Induction-induction is a principle for defining data types in Martin-Löf Type Theory. An inductive-inductive definition consists of a set A, together with an A-indexed family B : A → Set, where both A and B are inductively defined in such a way that the constructors for A can refer to B and vice versa. In addition, the constructors for B can refer to the constructors for A. We extend the usual initial algebra semantics for ordinary inductive data types to the inductive-inductive setting by considering dialgebras instead of ordinary algebras. This gives a new and compact formalisation of inductive-inductive definitions, which we prove is equivalent to the usual formulation with elimination rules.
Creators(s): |
Altenkirch, Thorsten, Morris, Peter, Nordvall Forsberg, Fredrik ![]() | Item type: | Book Section |
---|---|
ID code: | 53101 |
Keywords: | data type, dialgebras, elimination rules, formalisation, initial algebras, 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 13:38 |
Last modified: | 01 Jan 2021 06:52 |
Related URLs: | |
URI: | https://strathprints.strath.ac.uk/id/eprint/53101 |
Export data: |