Back to Search
Start Over
On the Semantic Expressiveness of Recursive Types
- Publication Year :
- 2020
-
Abstract
- Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-recursive. The relative advantages of iso- and equi-recursion are well- studied when it comes to their impact on type-inference. However, the relative semantic expressiveness of the two formulations remains unclear so far. This paper studies the semantic expressiveness of STLC with iso- and equi-recursive types, proving that these formulations are equally expressive. In fact, we prove that they are both as expressive as STLC with only term-level recursion. We phrase these equi-expressiveness results in terms of full abstraction of three canonical compilers between these three languages (STLC with iso-, with equi-recursive types and with term-level recursion). Our choice of languages allows us to study expressiveness when interacting over both a simply-typed and a recursively-typed interface. The three proofs all rely on a typed version of a proof technique called approximate backtranslation. Together, our results show that there is no difference in semantic expressiveness between STLCs with iso- and equi-recursive types. In this paper, we focus on a simply-typed setting but we believe our results scale to more powerful type systems like System F.
- Subjects :
- Phrase
Theoretical computer science
Interface (Java)
Computer science
Backtranslation
Coinductive Equi-recursive types
Fully-abstract compilation
Iso-recursive types
Lambda Calculus
Recursive types
cs.PL
02 engineering and technology
Type (model theory)
computer.software_genre
Mathematical proof
GeneralLiterature_MISCELLANEOUS
020204 information systems
0202 electrical engineering, electronic engineering, information engineering
Safety, Risk, Reliability and Quality
GeneralLiterature_REFERENCE(e.g.,dictionaries,encyclopedias,glossaries)
Abstraction (linguistics)
computer.programming_language
Recursion
020207 software engineering
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
ComputingMilieux_COMPUTERSANDSOCIETY
Compiler
Lambda calculus
computer
Software
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Accession number :
- edsair.doi.dedup.....e99a7186b935295dcc2cb5c5a935ca0f