On the Expressiveness of Affine Programs with Non-local Control: The Elimination of Nesting in SPCF

Issue title: Typed Lambda Calculi and Applications 2005, Selected Papers

Article type: Research Article

Authors: Laird, James D.

Affiliations: Department of Informatics, University of Sussex, United Kingdom. E-mail: jiml@sussex.ac.uk

Abstract: We use a denotational semantics to show that every term in SPCF (a typed functional language with simple non-local control operators) is contextually equivalent to one which is typable in an affine typing system. Nested function calls and recursive definitions are not affinely typable, and so our result entails that they can be eliminated from SPCF without losing expressiveness. Our proof is based on the observation of Longley that every type of SPCF is a retract of a first-order type. We describe retractions of this kind in bistable biorder models of SPCF 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. We show the flexibility of our approach by considering two variants of SPCF, a finitary, call-byname version and a call-by-value version over the natural numbers. In the infinitary case, (in which we establish in addition that all instances of recursive definition may be replaced with iteration) our proof is based on an analysis of the relationship between SPCF definable functions and strategies for computing them sequentially.

Journal: Fundamenta Informaticae, vol. 77, no. 4, pp. 511-531, 2007