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, Berlin, pp. 70-84. ISBN 9783642229435

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

Abstract

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 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:04 Jan 2019 03:24
Related URLs:
URI:https://strathprints.strath.ac.uk/id/eprint/53101
Export data:
CORE (COnnecting REpositories)