Open AccessAn Extensional Characterization of Lambda-Lifting and Lambda-Dropping
Author(s) -
Olivier Danvy
Publication year - 1998
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v5i2.21961
Subject(s) - lambda , correctness , extensional definition , mathematics , church encoding , characterization (materials science) , type (biology) , block (permutation group theory) , arithmetic , algebra over a field , algorithm , calculus (dental) , discrete mathematics , lambda calculus , combinatorics , pure mathematics , typed lambda calculus , simply typed lambda calculus , physics , medicine , paleontology , ecology , dentistry , biology , optics , tectonics
Lambda-lifting and lambda-dropping respectively transform a block-structured functional program into recursive equations and vice versa. Lambda-lifting is known since the early 80's, whereas lambda-dropping is more recent. Both are split into an analysis and a transformation. Published work, however, has only concentrated on the analysis part. We focus here on the transformation part and more precisely on its formal correctness, which is an open problem. One of our two main theorems suggests us to define extensional versions of lambda-lifting and lambda-dropping, which we visualize both using ML and using type-directed partial evaluation. See revised version BRICS-RS-99-21.