TY - GEN

T1 - The elimination of nesting in SPCF

AU - Laird, J.

PY - 2005

Y1 - 2005

N2 - We use a fully abstract denotational model to show that nested function calls and recursive definitions can be eliminated from SPCF (a typed functional language with simple non-local control operators) without losing expressiveness. We describe -via simple typing rules - an affine fragment of SPCF in which function nesting and recursion (other than iteration) are not permitted. We prove that this affine fragment is fully expressive in the sense that every term of SPCF is observationally equivalent to an affine term. Our proof is based on the observation of Longley - already used to prove universality and full abstraction results for models of SPCF that every type of SPCF is a retract of a first-order type. We describe retractions of this kind which are definable in the affine fragment. This allows us to transform an arbitrary SPCF term into an affine one by mapping it to a first-order term, obtaining an (affine) normal form, and then projecting back to the original type. In the case of finitary SPCF, the retraction is based on a simple induction, which yields bounds for the size of the resulting term. In the infinitary case, it is based on an analysis of the relationship between SPCF definable functions and strategies for computing them sequentially.

AB - We use a fully abstract denotational model to show that nested function calls and recursive definitions can be eliminated from SPCF (a typed functional language with simple non-local control operators) without losing expressiveness. We describe -via simple typing rules - an affine fragment of SPCF in which function nesting and recursion (other than iteration) are not permitted. We prove that this affine fragment is fully expressive in the sense that every term of SPCF is observationally equivalent to an affine term. Our proof is based on the observation of Longley - already used to prove universality and full abstraction results for models of SPCF that every type of SPCF is a retract of a first-order type. We describe retractions of this kind which are definable in the affine fragment. This allows us to transform an arbitrary SPCF term into an affine one by mapping it to a first-order term, obtaining an (affine) normal form, and then projecting back to the original type. In the case of finitary SPCF, the retraction is based on a simple induction, which yields bounds for the size of the resulting term. In the infinitary case, it is based on an analysis of the relationship between SPCF definable functions and strategies for computing them sequentially.

UR - http://www.scopus.com/inward/record.url?scp=24944444236&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1007/11417170_18

U2 - 10.1007/11417170_18

DO - 10.1007/11417170_18

M3 - Chapter in a published conference proceeding

AN - SCOPUS:24944444236

SN - 9783540255932

T3 - Lecture Notes in Computer Science

SP - 234

EP - 245

BT - Typed Lambda Calculi and Applications

A2 - Urzyczyn, P.

PB - Springer Verlag

CY - Berlin, Germany

T2 - 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005

Y2 - 21 April 2005 through 23 April 2005

ER -