Book chapter
Efficient Mendler-Style Lambda-Encodings in Cedille
Interactive Theorem Proving, pp.235-252
Lecture Notes in Computer Science, Springer International Publishing
07/04/2018
DOI: 10.1007/978-3-319-94821-8_14
Abstract
It is common to model inductive datatypes as least fixed points of functors. We show that within the Cedille type theory we can relax functoriality constraints and generically derive an induction principle for Mendler-style lambda-encoded inductive datatypes, which arise as least fixed points of covariant schemes where the morphism lifting is defined only on identities. Additionally, we implement a destructor for these lambda-encodings that runs in constant-time. As a result, we can define lambda-encoded natural numbers with an induction principle and a constant-time predecessor function so that the normal form of a numeral requires only linear space. The paper also includes several more advanced examples.
Details
- Title: Subtitle
- Efficient Mendler-Style Lambda-Encodings in Cedille
- Creators
- Denis Firsov - Department of Computer Science, The University of Iowa, Iowa City, USARichard Blair - Department of Computer Science, The University of Iowa, Iowa City, USAAaron Stump - Department of Computer Science, The University of Iowa, Iowa City, USA
- Resource Type
- Book chapter
- Publication Details
- Interactive Theorem Proving, pp.235-252
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-94821-8_14
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Publisher
- Springer International Publishing; Cham
- Language
- English
- Date published
- 07/04/2018
- Academic Unit
- Computer Science
- Record Identifier
- 9984002419302771
Metrics
26 Record Views