A categorical semantics for inductive-inductive definitions
Altenkirch, Thorsten and Morris, Peter and Nordvall Forsberg, Fredrik and Setzer, Anton (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.
| Author(s): | Altenkirch, Thorsten, Morris, Peter, Nordvall Forsberg, Fredrik  ORCID: https://orcid.org/0000-0001-6157-9288 and Setzer, Anton | 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: | 24 Jan 2020 04:36 |
| Related URLs: | |
| URI: | https://strathprints.strath.ac.uk/id/eprint/53101 |
| Export data: |
CORE (COnnecting REpositories)
CORE (COnnecting REpositories)