The Optimal Implementation of Functional Programming LanguagesCambridge University Press, 3.12.1998 - 392 sivua All traditional implementation techniques for functional languages fail to avoid useless repetition of work. They are not "optimal" in their implementation of sharing, often causing a catastrophic, exponential explosion in reduction time. Optimal reduction is an innovative graph reduction technique for functional expressions, introduced by Lamping in 1990, that solves the sharing problem. This work, the first on the subject, is a comprehensive account by two of its leading exponents. Practical implementation aspects are fully covered as are the mathematical underpinnings of the subject. The relationship to the pioneering work of Lévy and to Girard's more recent "Geometry of Interaction" are explored; optimal reduction is thereby revealed as a prime example of how a beautiful mathematical theory can lead to practical benefit. The book is essentially self-contained, requiring no more than basic familiarity with functional languages. It will be welcomed by graduate students and research workers in lambda calculus, functional programming or linear logic. |
Sisältö
III | 1 |
V | 4 |
VI | 8 |
VII | 14 |
IX | 15 |
X | 19 |
XI | 20 |
XII | 29 |
LXVIII | 208 |
LXIX | 209 |
LXX | 212 |
LXXI | 215 |
LXXIII | 216 |
LXXIV | 217 |
LXXV | 220 |
LXXVI | 221 |
XIII | 33 |
XIV | 35 |
XV | 38 |
XVI | 39 |
XVII | 41 |
XVIII | 43 |
XIX | 46 |
XX | 50 |
XXI | 52 |
XXII | 60 |
XXIII | 63 |
XXIV | 66 |
XXV | 71 |
XXVI | 73 |
XXVII | 75 |
XXVIII | 76 |
XXIX | 80 |
XXX | 81 |
XXXI | 83 |
XXXII | 86 |
XXXIII | 88 |
XXXIV | 89 |
XXXV | 91 |
XXXVI | 96 |
XXXVII | 98 |
XXXVIII | 101 |
XXXIX | 105 |
XL | 108 |
XLI | 119 |
XLII | 122 |
XLIII | 124 |
XLIV | 126 |
XLV | 129 |
XLVI | 138 |
XLVII | 141 |
XLIX | 142 |
L | 144 |
LI | 148 |
LII | 150 |
LIII | 154 |
LIV | 159 |
LV | 168 |
LVI | 178 |
LVIII | 179 |
LIX | 181 |
LX | 184 |
LXI | 185 |
LXII | 189 |
LXIII | 191 |
LXIV | 196 |
LXV | 199 |
LXVI | 200 |
LXVII | 206 |
LXXVII | 222 |
LXXVIII | 223 |
LXXIX | 224 |
LXXX | 225 |
LXXXI | 227 |
LXXXII | 229 |
LXXXIII | 231 |
LXXXIV | 233 |
LXXXV | 235 |
LXXXVI | 239 |
LXXXVII | 240 |
LXXXVIII | 243 |
LXXXIX | 244 |
XC | 247 |
XCI | 248 |
XCII | 250 |
XCIII | 257 |
XCIV | 262 |
XCV | 265 |
XCVI | 268 |
XCVII | 269 |
XCVIII | 272 |
XCIX | 273 |
C | 277 |
CI | 279 |
CII | 281 |
CV | 284 |
CVI | 288 |
CVII | 291 |
CVIII | 296 |
CIX | 302 |
CXI | 303 |
CXIII | 305 |
CXIV | 313 |
CXVI | 316 |
CXVII | 328 |
CXVIII | 329 |
CXIX | 331 |
CXX | 334 |
CXXI | 342 |
CXXII | 343 |
CXXIII | 344 |
CXXIV | 351 |
CXXV | 352 |
CXXVII | 355 |
CXXVIII | 361 |
CXXIX | 365 |
CXXX | 370 |
CXXXI | 371 |
CXXXII | 376 |
| 383 | |
| 390 | |
Yleiset termit ja lausekkeet
A-calculus A-node A-term abstract syntax tree access path ancestor application argument arity auxiliary ports binding loop binding port brackets Caml Light church integer computation consistent paths control nodes corresponding critical pair croissant cycle deadlock-free defined definition duplication example expanded proper path family red fan inter fan-in fan-out function garbage collection graph reduction graph rewriting implementation induction hypothesis initial instance interaction internal labeled lambda calculus leftmost-outermost legal path Lemma let us note lifting sequence Linear Logic LSeq M₁ normal form occurrence optimal reduction pair prerequisite chain principal port proof proof net proper node Proposition prove quicksort read-back representation residual rewriting rules rules in Figure sharing graph sharing nodes ẞ-redex ẞ-reduction ẞ-rule strongly normalizing subterm syntax tree term Theorem traversed unique unshared graph v-cycle v-node virtual redex λι λο λχ
Suositut otteet
Sivu 387 - In Automata, Languages and Programming. 24th International Colloquium, volume 1256 of Lecture Notes in Computer Science, pages 177-187.
Sivu 388 - Press, 1980. [LM96] Julia L. Lawall and Harry G. Mairson. Optimality and inefficiency: What isn'ta cost model of the lambda calculus? In 1996 ACM International Conference on Functional Programming, 1996.
Sivu 386 - S. Abramsky and G. McCusker. Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions (extended abstract). In Proceedings of 1996 Workshop on Linear Logic, volume 3 of Electronic notes in Theoretical Computer Science. Elsevier, 1996.
Viitteet tähän teokseen
The Parametric Lambda Calculus: A Metamodel for Computation Simona Ronchi Della Rocca,Luca Paolini Rajoitettu esikatselu - 2004 |
Typed Lambda Calculi and Applications: 5th International Conference, TLCA ... Samson Abramsky Esikatselu ei käytettävissä - 2001 |

