The elimination of nesting in SPCF

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

3 Citations (SciVal)


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.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications
Subtitle of host publicationProceedings of 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005
EditorsP. Urzyczyn
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Number of pages12
ISBN (Print)9783540255932
Publication statusPublished - 2005
Event7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005 - Nara, Japan
Duration: 21 Apr 200523 Apr 2005

Publication series

NameLecture Notes in Computer Science


Conference7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005

ASJC Scopus subject areas

  • Computer Science (miscellaneous)


Dive into the research topics of 'The elimination of nesting in SPCF'. Together they form a unique fingerprint.

Cite this