Linearity and Recursion in a Typed Lambda-Calculus

摘要

We show that the full PCF language can be encoded in E_(rec), a syntactically linear A-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for E_(rec), exploiting its linearity.