Course-of-Value Induction in Cedille

Denis Firsov; Larry Diehl; Christopher Jenkins; Aaron Stump

doi:10.48550/arxiv.1811.11961

Back

Preprint

Open access

Course-of-Value Induction in Cedille

Denis Firsov, Larry Diehl, Christopher Jenkins and Aaron Stump

ArXiv.org

11/28/2018

DOI: 10.48550/arxiv.1811.11961

Files and links (1)

url

https://doi.org/10.48550/arXiv.1811.11961View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

Abstract

In the categorical setting, histomorphisms model a course-of-value recursion scheme that allows functions to be defined using arbitrary previously computed values. In this paper, we use the Calculus of Dependent Lambda Eliminations (CDLE) to derive a lambda-encoding of inductive datatypes that admits course-of-value induction. Similar to course-of-value recursion, course-of-value induction gives access to inductive hypotheses at arbitrary depth of the inductive arguments of a function. We show that the derived course-of-value datatypes are well-behaved by proving Lambek's lemma and characterizing the computational behavior of the induction principle. Our work is formalized in the Cedille programming language and also includes several examples of course-of-value functions.

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Course-of-Value Induction in Cedille
Creators: Denis Firsov
Larry Diehl
Christopher Jenkins
Aaron Stump
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.1811.11961
ISSN: 2331-8422
Language: English
Date posted: 11/28/2018
Academic Unit: Computer Science
Record Identifier: 9984410847702771

Metrics

1 Record Views