The power of closed reduction strategies

S. Alves; M. Fernández; M. Florido; I. Mackie

The power of closed reduction strategies

S. Alves
, M. Fernández
, M. Florido
, I. Mackie

École Polytechnique

Ipatimup Diagnósticos
King's College London

Research output: Contribution to journal › Conference article › peer-review

Abstract

Closed reduction strategies in the λ-calculus restrict the reduction rules: the idea is that reductions can only take place when certain terms are closed (i.e. do not contain free variables). This has lead to various applications, such as an α-conversion free calculus of explicit substitutions, and an efficient abstract machine. The main contribution of this paper is a new application of this strategy to a linear version of Gödel's System T. We show that a linear System T with closed reduction offers a huge increase in expressive power over the usual linear systems, which are 'closed by construction' rather than 'closed at reduction'.

Original language	English
Pages (from-to)	20-33
Number of pages	14
Journal	Electronic Notes in Theoretical Computer Science
Publication status	Published - 1 Dec 2006
Event	6th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2006, as part of the Federated Logic Conference, FLoC 2006 - Seattle, WA, United States Duration: 11 Aug 2006 → 11 Aug 2006

Cite this

@article{0c49aef5bdb143b4bf1f414d045e4194,

title = "The power of closed reduction strategies",

abstract = "Closed reduction strategies in the λ-calculus restrict the reduction rules: the idea is that reductions can only take place when certain terms are closed (i.e. do not contain free variables). This has lead to various applications, such as an α-conversion free calculus of explicit substitutions, and an efficient abstract machine. The main contribution of this paper is a new application of this strategy to a linear version of G{\"o}del's System T. We show that a linear System T with closed reduction offers a huge increase in expressive power over the usual linear systems, which are 'closed by construction' rather than 'closed at reduction'.",

author = "S. Alves and M. Fern{\'a}ndez and M. Florido and I. Mackie",

year = "2006",

month = dec,

day = "1",

language = "English",

pages = "20--33",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

note = "6th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2006, as part of the Federated Logic Conference, FLoC 2006 ; Conference date: 11-08-2006 Through 11-08-2006",

}

TY - JOUR

T1 - The power of closed reduction strategies

AU - Alves, S.

AU - Fernández, M.

AU - Florido, M.

AU - Mackie, I.

PY - 2006/12/1

Y1 - 2006/12/1

N2 - Closed reduction strategies in the λ-calculus restrict the reduction rules: the idea is that reductions can only take place when certain terms are closed (i.e. do not contain free variables). This has lead to various applications, such as an α-conversion free calculus of explicit substitutions, and an efficient abstract machine. The main contribution of this paper is a new application of this strategy to a linear version of Gödel's System T. We show that a linear System T with closed reduction offers a huge increase in expressive power over the usual linear systems, which are 'closed by construction' rather than 'closed at reduction'.

AB - Closed reduction strategies in the λ-calculus restrict the reduction rules: the idea is that reductions can only take place when certain terms are closed (i.e. do not contain free variables). This has lead to various applications, such as an α-conversion free calculus of explicit substitutions, and an efficient abstract machine. The main contribution of this paper is a new application of this strategy to a linear version of Gödel's System T. We show that a linear System T with closed reduction offers a huge increase in expressive power over the usual linear systems, which are 'closed by construction' rather than 'closed at reduction'.

UR - https://www.scopus.com/pages/publications/84890259664

M3 - Conference article

AN - SCOPUS:84890259664

SN - 1571-0661

SP - 20

EP - 33

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - 6th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2006, as part of the Federated Logic Conference, FLoC 2006

Y2 - 11 August 2006 through 11 August 2006

ER -

The power of closed reduction strategies

Abstract

Other files and links

Fingerprint

Cite this