# Denotational aspects of untyped normalization by evaluation

Andrzej Filinski; Henning Korsholm Rohde

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 39, Issue: 3, page 423-453
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topFilinski, Andrzej, and Rohde, Henning Korsholm. "Denotational aspects of untyped normalization by evaluation." RAIRO - Theoretical Informatics and Applications 39.3 (2010): 423-453. <http://eudml.org/doc/92775>.

@article{Filinski2010,

abstract = {
We show that the standard normalization-by-evaluation construction for the
simply-typed λβη-calculus
has a natural counterpart for the untyped
λβ-calculus, with the central type-indexed logical relation
replaced by a “recursively defined” invariant relation, in
the style of Pitts. In fact, the construction can be seen as
generalizing a computational-adequacy argument for an untyped,
call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms, so the
normalization function is necessarily partial. We establish its
correctness in the senses of soundness (the output term, if
any, is in normal form and β-equivalent to the input term);
identification (β-equivalent terms are mapped to the
same result); and completeness (the function is defined for
all terms that do have normal forms). We also show how the semantic
construction enables a simple yet formal correctness proof for the
normalization algorithm, expressed as a functional program in an
ML-like, call-by-value language. Finally, we generalize the construction to produce an
infinitary variant of normal forms, namely Böhm trees.
We show that the three-part characterization of correctness,
as well as the proofs, extend naturally to this generalization.
},

author = {Filinski, Andrzej, Rohde, Henning Korsholm},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Normalization by evaluation; untyped λ-calculus;
denotational semantics; functional programming; Böhm trees;
computational adequacy.; untyped -calculus; denotational semantics; computational adequacy; normalization-by-evaluation construction},

language = {eng},

month = {3},

number = {3},

pages = {423-453},

publisher = {EDP Sciences},

title = {Denotational aspects of untyped normalization by evaluation},

url = {http://eudml.org/doc/92775},

volume = {39},

year = {2010},

}

TY - JOUR

AU - Filinski, Andrzej

AU - Rohde, Henning Korsholm

TI - Denotational aspects of untyped normalization by evaluation

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 39

IS - 3

SP - 423

EP - 453

AB -
We show that the standard normalization-by-evaluation construction for the
simply-typed λβη-calculus
has a natural counterpart for the untyped
λβ-calculus, with the central type-indexed logical relation
replaced by a “recursively defined” invariant relation, in
the style of Pitts. In fact, the construction can be seen as
generalizing a computational-adequacy argument for an untyped,
call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms, so the
normalization function is necessarily partial. We establish its
correctness in the senses of soundness (the output term, if
any, is in normal form and β-equivalent to the input term);
identification (β-equivalent terms are mapped to the
same result); and completeness (the function is defined for
all terms that do have normal forms). We also show how the semantic
construction enables a simple yet formal correctness proof for the
normalization algorithm, expressed as a functional program in an
ML-like, call-by-value language. Finally, we generalize the construction to produce an
infinitary variant of normal forms, namely Böhm trees.
We show that the three-part characterization of correctness,
as well as the proofs, extend naturally to this generalization.

LA - eng

KW - Normalization by evaluation; untyped λ-calculus;
denotational semantics; functional programming; Böhm trees;
computational adequacy.; untyped -calculus; denotational semantics; computational adequacy; normalization-by-evaluation construction

UR - http://eudml.org/doc/92775

ER -

## References

top- K. Aehlig and F. Joachimski, Operational aspects of untyped normalization by evaluation. Math. Structures Comput. Sci.14 (2004) 587–611. Zbl1090.68018
- H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition (1984). Zbl0551.03007
- U. Berger and H. Schwichtenberg, An inverse of the evaluation functional for typed λ-calculus, in Proc. of the Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands (July 1991) 203–211.
- T. Coquand and P. Dybjer, Intuitionistic model constructions and normalization proofs. Math. Structures Comput. Sci.7 (1997) 75–94. Zbl0883.03009
- A. Filinski, A semantic account of type-directed partial evaluation, in International Conference on Principles and Practice of Declarative Programming, edited by G. Nadathur, Springer-Verlag, Paris, France. Lect. Notes Comput. Sci.1702 (1999) 378–395 Zbl0953.68034
- A. Filinski and H.K. Rohde, A denotational account of untyped normalization by evaluation, in 7th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2004), edited by I. Walukiewicz, Springer-Verlag, Barcelona, Spain Lect. Notes Comput. Sci.2987 (2004) 167–181. Zbl1126.68335
- A. Filinski and H.K. Rohde, Denotational aspects of untyped normalization by evaluation (extended version, with detailed proofs). BRICS Report RS-05-4, University of Aarhus, Denmark (February 2005). Available from . URIhttp://www.brics.dk/RS/05/4/
- B. Grégoire and X. Leroy, A compiled implementation of strong reduction, in Proc. of the Seventh ACM SIGPLAN International Conference on Functional Programming, edited by S. Peyton Jones, ACM Press, Pittsburgh, Pennsylvania, SIGPLAN Notices 37 (2002) 235–246. Zbl1322.68053
- R. Milner, M. Tofte, R. Harper and D. MacQueen, The Definition of Standard ML. The MIT Press, revised edition (1997).
- J.C. Mitchell, Foundations for Programming Languages. The MIT Press (1996).
- A.M. Pitts, Computational adequacy via “mixed” inductive definitions, in Mathematical Foundations of Programming Semantics. Springer-Verlag. Lect. Notes Comput. Sci.802 (1993) 72–82.
- A.M. Pitts, Relational properties of domains. Inform. Comput.127 (1996) 66–90. Zbl0868.68037
- G.D. Plotkin, LCF considered as a programming language. Theor. Comput. Sci.5 (1977) 223–255.
- M.R. Shinwell, A.M. Pitts and M.J. Gabbay, FreshML: Programming with binders made simple, in Eighth ACM SIGPLAN International Conference on Functional Programming, ACM Press, Uppsala, Sweden (2003) 263–274. Zbl1315.68058

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.