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.2018.27
URN: urn:nbn:de:0030-drops-91972
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9197/
Go to the corresponding LIPIcs Volume Portal

Parys, Pawel

Homogeneity Without Loss of Generality

pdf-format:
LIPIcs-FSCD-2018-27.pdf (0.5 MB)

Abstract

We consider higher-order recursion schemes as generators of infinite trees. A sort (simple type) is called homogeneous when all arguments of higher order are taken before any arguments of lower order. We prove that every scheme can be converted into an equivalent one (i.e, generating the same tree) that is homogeneous, that is, uses only homogeneous sorts. Then, we prove the same for safe schemes: every safe scheme can be converted into an equivalent safe homogeneous scheme. Furthermore, we compare two definition of safe schemes: the original definition of Damm, and the modern one. Finally, we prove a lemma which illustrates usefulness of the homogeneity assumption. The results are known, but we prove them in a novel way: by directly manipulating considered schemes.

BibTeX - Entry

@InProceedings{parys:LIPIcs:2018:9197,
  author =	{Pawel Parys},
  title =	{{Homogeneity Without Loss of Generality}},
  booktitle =	{3rd International Conference on Formal Structures for  Computation and Deduction (FSCD 2018)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{H{\'e}l{\`e}ne Kirchner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9197},
  URN =		{urn:nbn:de:0030-drops-91972},
  doi =		{10.4230/LIPIcs.FSCD.2018.27},
  annote =	{Keywords: higher-order recursion schemes, lambda-calculus, homogeneous types, safe schemes}
}

Keywords: higher-order recursion schemes, lambda-calculus, homogeneous types, safe schemes
Collection: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Issue Date: 2018
Date of publication: 04.07.2018

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