License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.23
URN: urn:nbn:de:0030-drops-123451
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12345/
Go to the corresponding LIPIcs Volume Portal

Kaposi, Ambrus ; von Raumer, Jakob

A Syntax for Mutual Inductive Families

pdf-format:
LIPIcs-FSCD-2020-23.pdf (0.5 MB)

Abstract

Inductive families of types are a feature of most languages based on dependent types. They are usually described either by syntactic schemes or by encodings of strictly positive functors such as combinator languages or containers. The former approaches are informal and give only external signatures, the latter approaches suffer from encoding overheads and do not directly represent mutual types.
In this paper we propose a direct method for describing signatures for mutual inductive families using a domain-specific type theory. A signature is a context (roughly speaking, a list of types) in this small type theory. Algebras, displayed algebras and sections are defined by models of this type theory: the standard model, the logical predicate and a logical relation interpretation, respectively. We reduce the existence of initial algebras for these signatures to the existence of the syntax of our domain-specific type theory. As this theory is very simple, its normal syntax can be encoded using indexed W-types. To the best of our knowledge, this is the first formalisation of the folklore fact that mutual inductive types can be reduced to indexed W-types.
The contents of this paper were formalised in the proof assistant Agda.

BibTeX - Entry

@InProceedings{kaposi_et_al:LIPIcs:2020:12345,
  author =	{Ambrus Kaposi and Jakob von Raumer},
  title =	{{A Syntax for Mutual Inductive Families}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12345},
  URN =		{urn:nbn:de:0030-drops-123451},
  doi =		{10.4230/LIPIcs.FSCD.2020.23},
  annote =	{Keywords: type theory, inductive types, mutual inductive types, W-types, Agda}
}

Keywords: type theory, inductive types, mutual inductive types, W-types, Agda
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020
Supplementary Material: All of the results were formalised in the proof assistant Agda, the source code is available online at https://bitbucket.org/javra/inductive-families/src/master/agda.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI