Data types, infinity and equality in system AF 2

Autor:	Christophe Raffalli
Rok vydání:	2006
Předmět:	Algebra Normalization (statistics) Pure mathematics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer Science::Logic in Computer Science Coinduction Uniqueness Equivalence (formal languages) Programming method Data type Mathematics
Zdroj:	Computer Science Logic ISBN: 3540582770 CSL
DOI:	10.1007/bfb0049337
Popis:	This work presents an extension of system AF2 to allow the use of infinite data types. We extend the logic with inductive and coinductive types, and show that the “programming method” is still correct. We prove propositions about the normalization of typed terms. Moreover, since we only use the pure λ-calculus to represent data types, we prove uniqueness of the representation of data up to Bohm tree equivalence. We also study the problem of equality on infinite structures and we introduce a new approach, different from the coinduction scheme, and which suits our system better.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::f1f1634481d7b386acc866075bc3f6fb https://doi.org/10.1007/bfb0049337 Zobrazit plný text záznamu