Among all the reduction strategies for the untyped λ-calculus, the so called lazy β-evaluation is of particular interest due to its large applicability to functional programming languages (e.g. Haskell [Bird, R., “Introduction to Functional Programming using Haskell,” Series in Computer Science (2nd edition), Prentice Hall, (1998)]). This strategy reduces only redexes not inside a lambda abstraction. The lazy strongly β- normalizing terms are the λ-terms that don't have infinite lazy β-reduction sequences. This paper presents a logical characterization of lazy strongly β-normalizing terms using intersection types. This characterization, besides being interesting by itself, allows an interesting connection between call-by-name and call-by-value λ-calculus. In fact, it turns out that the class of lazy strongly β-normalizing terms coincides with that of call-by-value potentially valuable terms. This last class is of particular interest since it is a key notion for characterizing solvability in the call-by-value setting.

Lazy strong normalization

PAOLINI, LUCA LUIGI;RONCHI DELLA ROCCA, Simonetta
2005-01-01

Abstract

Among all the reduction strategies for the untyped λ-calculus, the so called lazy β-evaluation is of particular interest due to its large applicability to functional programming languages (e.g. Haskell [Bird, R., “Introduction to Functional Programming using Haskell,” Series in Computer Science (2nd edition), Prentice Hall, (1998)]). This strategy reduces only redexes not inside a lambda abstraction. The lazy strongly β- normalizing terms are the λ-terms that don't have infinite lazy β-reduction sequences. This paper presents a logical characterization of lazy strongly β-normalizing terms using intersection types. This characterization, besides being interesting by itself, allows an interesting connection between call-by-name and call-by-value λ-calculus. In fact, it turns out that the class of lazy strongly β-normalizing terms coincides with that of call-by-value potentially valuable terms. This last class is of particular interest since it is a key notion for characterizing solvability in the call-by-value setting.
2005
ntersection Types and Related Systems (ITRS'04)
Turku, Finland
13 July 2004
136C
103
116
http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4GK8BG8-6&_user=525216&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_version=1&_urlVersion=0&_userid=525216&md5=ad8450b9d695c7eefce89c5ca2a0f597
λ-calculus; lazy evaluation; lazy strong normalization
L. PAOLINI; E. PIMENTEL; S. RONCHI DELLA ROCCA
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/8398
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 0
social impact