On the expressiveness of affine programs with non-local control

the elimination of nesting in SPCF

Research output: Contribution to journalArticle

3 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)511-531
Number of pages21
JournalFundamenta Informaticae
Volume77
Issue number4
Publication statusPublished - 2007

Fingerprint

Expressiveness
Elimination
Affine transforms
Semantics
Term
First-order
Denotational Semantics
Order Type
Retract
Retraction
Natural number
Normal Form
Fragment
Flexibility
Transform
Iteration
Computing
Arbitrary
Operator

Cite this

On the expressiveness of affine programs with non-local control : the elimination of nesting in SPCF. / Laird, James D.

In: Fundamenta Informaticae, Vol. 77, No. 4, 2007, p. 511-531.

Research output: Contribution to journalArticle

@article{6314553cd39d4b88a4ee71a3bf4257bb,
title = "On the expressiveness of affine programs with non-local control: the elimination of nesting in SPCF",
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.",
author = "Laird, {James D.}",
year = "2007",
language = "English",
volume = "77",
pages = "511--531",
journal = "Fundamenta Informaticae",
issn = "0169-2968",
publisher = "IOS Press",
number = "4",

}

TY - JOUR

T1 - On the expressiveness of affine programs with non-local control

T2 - the elimination of nesting in SPCF

AU - Laird, James D.

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

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

M3 - Article

VL - 77

SP - 511

EP - 531

JO - Fundamenta Informaticae

JF - Fundamenta Informaticae

SN - 0169-2968

IS - 4

ER -